Post-state of statement spec
ID0000765: This issue was created automatically from Mantis Issue 765. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000765 | Frama-C | Plug-in > wp | public | 2011-03-25 | 2013-03-09 |
| Reporter | Anne | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
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))))