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)))) ## Attachments - [toto.c](/uploads/8feb2b09fab3964d8240b54efa9b2d18/toto.c)