Frama-C Bug Tracking System - Frama-C
View Issue Details
0000765Frama-CPlug-in > wppublic2011-03-25 15:522013-03-09 23:42
Anne 
correnson 
normalminorhave not tried
assignedopen 
 
 
0000765: Post-state of statement spec
When there is a [goto] going out of a block, the post-condition should be check at the normal exit of the block (ie. the program point after the '}'). But there is a problem when the [goto] precisely jump to that point... The CFG for WP should be able to find only the edge coming from the block exit !
$ frama-c -wp toto.c -wp-print Goal store_f_default_for_stmt_2_stmt_post_1: forall c:int. is_in_format(sint32_format, c) -> ( tag_Then:( (c <> 0) -> (let x= 1 in (x = 10))) and tag_Else:( (c = 0) -> (let x= 10 in (x = 10))))
No tags attached.
c toto.c (137) 2011-03-25 15:52
https://bts.frama-c.com/file_download.php?file_id=186&type=bug
Issue History
2011-03-25 15:52AnneNew Issue
2011-03-25 15:52AnneStatusnew => assigned
2011-03-25 15:52AnneAssigned To => dargaye
2011-03-25 15:52AnneFile Added: toto.c
2011-03-25 15:52AnneAssigned Todargaye => Anne
2011-03-25 15:55AnneNote Added: 0001640
2011-03-25 15:55AnneAssigned ToAnne => patrick
2011-03-25 15:55AnneAssigned Topatrick => Anne
2011-04-11 15:48AnneNote Added: 0001716
2011-04-11 15:48AnneAssigned ToAnne => correnson
2011-04-11 15:49AnneNote Added: 0001718
2012-01-31 16:16patrickNote Added: 0002649

Notes
(0001640)
Anne   
2011-03-25 15:55   
It is not easy to fix because it seems that we want another behavior for the post-condition of a loop since the end of the block is never reached directly, but always through [break] statements.
(0001716)
Anne   
2011-04-11 15:48   
The previous note is not true if we imagine that the break label is in the loop statement as if the loop were in a block. BTW the block also includes the initial part of the [for] loop. When fixing this bug, one should also consider the conclusion of the "commit" mailing list discussion (the 6 of April 2011) about the [assigns] property of a statement.
(0001718)
Anne   
2011-04-11 15:49   
@Loïc: I transfer this task to you as you asked for.
(0002649)
patrick   
2012-01-31 16:16   
There is another similar example raising an exception: void g(int c) { int r; r=0; //@ assigns \nothing; if(c) { goto stop; } stop: ; r=1; } frama-c -wp file.c ... [wp] failure: Merging different assigns goals [kernel] The full backtrace is: Raised at file "src/wp/register.ml", line 615, characters 27-29