Frama-C Bug Tracking System - Frama-C
View Issue Details
0000765Frama-CPlug-in > wppublic2011-03-25 15:522013-03-09 23:42
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000765: Post-state of statement spec
DescriptionWhen 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 !
Additional Information$ 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))))
TagsNo tags attached.
Attached Filesc toto.c (137) 2011-03-25 15:52
https://bts.frama-c.com/file_download.php?file_id=186&type=bug

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

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