2021-01-21 06:24 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000765Frama-CPlug-in > wppublic2011-03-25 15:522013-03-09 23:42
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
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 Files
  • c file icon toto.c (137 bytes) 2011-03-25 15:52 - 
    void f (int c) {
  int x;

  //@ ensures x == 10;
  {
    x = 0;
    if (c) {
      x ++;
      goto L;
    }
    x += 10;
  }
L: x++;
}
    c file icon toto.c (137 bytes) 2011-03-25 15:52 +

-Relationships
+Relationships

-Notes

~0001640

Anne (reporter)

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 (reporter)

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 (reporter)

2011-04-11 15:49

 @Loïc: I transfer this task to you as you asked for.

~0002649

patrick (developer)

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
+Notes

-Issue History
Date Modified Username Field Change
2011-03-25 15:52 Anne New Issue
2011-03-25 15:52 Anne Status new => assigned
2011-03-25 15:52 Anne Assigned To => dargaye
2011-03-25 15:52 Anne File Added: toto.c
2011-03-25 15:52 Anne Assigned To dargaye => Anne
2011-03-25 15:55 Anne Note Added: 0001640
2011-03-25 15:55 Anne Assigned To Anne => patrick
2011-03-25 15:55 Anne Assigned To patrick => Anne
2011-04-11 15:48 Anne Note Added: 0001716
2011-04-11 15:48 Anne Assigned To Anne => correnson
2011-04-11 15:49 Anne Note Added: 0001718
2012-01-31 16:16 patrick Note Added: 0002649
+Issue History