ID0001279: **This issue was created automatically from Mantis Issue 1279. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001279 | Frama-C | Plug-in > wp | public | 2012-10-13 | 2012-10-13 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | sjw | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | crash | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - | ### Description : The following code: /*@ ensures \result == x; */ int test(int x) { again: if (x > 10) goto again; if (x > 10) goto again; return x; } gives $ ~/frama-c/bin/frama-c -wp doublegoto.c [kernel] preprocessing with "gcc -C -E -I. doublegoto.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] failure: CFG node <loop-1> has 2 successors instead of 1 ... This is caused by the use of a list for loop headers in cil2cfg.ml. The attached patch fixes this by using a set of nodes. ## Attachments - [goto.diff](/uploads/7ba7b9828d39e5be247e9fb3e8ba11cb/goto.diff)