Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001502Frama-CKernelpublic2013-10-16 17:262014-03-13 15:57
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001502: goto L; with L: in a if/else branch
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?
TagsNo tags attached.
Attached Filespatch file icon bts1502.patch [^] (584 bytes) 2013-10-18 09:42 [Show Content]

- Relationships

-  Notes
(0004133)
virgile (developer)
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 (reporter)
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 (developer)
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 (reporter)
2013-10-18 09:50

Many thanks!
(0004185)
virgile (developer)
2013-10-29 14:32

fixed in svn and patch is attached.
(0004556)

2014-02-12 16:57

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2013-10-16 17:26 dpariente New Issue
2013-10-16 17:44 signoles Status new => assigned
2013-10-16 17:44 signoles Assigned To => virgile
2013-10-16 18:26 virgile Note Added: 0004133
2013-10-16 18:26 virgile Status assigned => confirmed
2013-10-17 15:02 svn Checkin
2013-10-17 15:02 svn Status confirmed => resolved
2013-10-17 15:02 svn Resolution open => fixed
2013-10-18 09:30 dpariente Note Added: 0004142
2013-10-18 09:30 dpariente Status resolved => feedback
2013-10-18 09:30 dpariente Resolution fixed => reopened
2013-10-18 09:42 virgile File Added: bts1502.patch
2013-10-18 09:47 virgile Note Added: 0004143
2013-10-18 09:50 dpariente Note Added: 0004144
2013-10-29 14:32 virgile Note Added: 0004185
2013-10-29 14:32 virgile Status feedback => resolved
2013-10-29 14:32 virgile Resolution reopened => fixed
2014-02-12 16:57 Note Added: 0004556
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker