goto L; with L: in a if/else branch
ID0001502: This issue was created automatically from Mantis Issue 1502. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001502 | Frama-C | Kernel | public | 2013-10-16 | 2014-03-13 |
| Reporter | dpariente | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
[STANCE]
The following code:
void f(int a) { goto _LOR_0; if (a) _LOR_0: ; }
analyzed by:
frama-c ../skip.c -print -ocode ../skip2.c (with or without -no-simplify-cfg)
generates a warning: [kernel] user error: Label _LOR_0 not found
and an error when parsing pretty-printed code in skip2.c: frama-c ../skip2.c [kernel] user error: Label _LOR_0 not found
It seems that the branch containing the label is pruned as considered as empty! Typically, modifying cabs2cil.ml (line 1142) so that Instr (Skip _) is no more considered as an empty stmt solves the problem (of course this is just a workaround!). Is something more robust available?