View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0000765 | Frama-C | Plug-in > wp | public | 2011-03-25 15:52 | 2013-03-09 23:42 | ||||||||
Reporter | Anne | ||||||||||||
Assigned To | correnson | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||||||
Status | assigned | Resolution | open | ||||||||||
Product Version | |||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0000765: Post-state of statement spec | ||||||||||||
Description | 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 ! | ||||||||||||
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)))) | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
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. |
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. |
Anne (reporter) 2011-04-11 15:49 |
@Loïc: I transfer this task to you as you asked for. |
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 |
![]() |
|||
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 |