Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

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 
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 file icon toto.c [^] (137 bytes) 2011-03-25 15:52 [Show Content]

- 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

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker