Multiple branches to a label/loop entries crashes wp
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 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.