Frama-C Bug Tracking System - Frama-C
View Issue Details
0001502Frama-CKernelpublic2013-10-16 17:262014-03-13 15:57
dpariente 
virgile 
normalmajoralways
closedfixed 
Frama-C Fluorine-20130601 
Frama-C Neon-20140301 
0001502: goto L; with L: in a if/else branch
[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?
No tags attached.
patch bts1502.patch (584) 2013-10-18 09:42
https://bts.frama-c.com/file_download.php?file_id=537&type=bug
Issue History
2013-10-16 17:26dparienteNew Issue
2013-10-16 17:44signolesStatusnew => assigned
2013-10-16 17:44signolesAssigned To => virgile
2013-10-16 18:26virgileNote Added: 0004133
2013-10-16 18:26virgileStatusassigned => confirmed
2013-10-17 15:02svnCheckin
2013-10-17 15:02svnStatusconfirmed => resolved
2013-10-17 15:02svnResolutionopen => fixed
2013-10-18 09:30dparienteNote Added: 0004142
2013-10-18 09:30dparienteStatusresolved => feedback
2013-10-18 09:30dparienteResolutionfixed => reopened
2013-10-18 09:42virgileFile Added: bts1502.patch
2013-10-18 09:47virgileNote Added: 0004143
2013-10-18 09:50dparienteNote Added: 0004144
2013-10-29 14:32virgileNote Added: 0004185
2013-10-29 14:32virgileStatusfeedback => resolved
2013-10-29 14:32virgileResolutionreopened => fixed
2014-02-12 16:57Note Added: 0004556
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004133)
virgile   
2013-10-16 18:26   
The proper fix is to avoid considering that a statement with a label is empty. I'll check that.
(0004142)
dpariente   
2013-10-18 09:30   
Thank you Virgile for your reactivity.
Is there any patch for this fix based on Fluorine-130601, or will it be for the next Frama-C release?
(0004143)
virgile   
2013-10-18 09:47   
patch is attached, apply it with patch -p0 < bts1502.patch on the top directory of Frama-C sources.
(0004144)
dpariente   
2013-10-18 09:50   
Many thanks!
(0004185)
virgile   
2013-10-29 14:32   
fixed in svn and patch is attached.
(0004556)
   
2014-02-12 16:57   
Fix committed to stable/neon branch.