2021-02-24 18:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001502Frama-CKernelpublic2014-03-13 15:57
Reporterdpariente 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • patch file icon bts1502.patch (584 bytes) 2013-10-18 09:42 -
    Index: cil/src/frontc/cabs2cil.ml
    ===================================================================
    --- cil/src/frontc/cabs2cil.ml	(révision 24172)
    +++ cil/src/frontc/cabs2cil.ml	(révision 24173)
    @@ -1193,7 +1193,7 @@
         let empty_stmts l =
           let rec is_empty_stmt s =
             match s.skind with
    -            Instr (Skip _) -> true
    +            Instr (Skip _) -> s.labels = []
               | Block b -> b.battrs = [] && List.for_all is_empty_stmt b.bstmts
               | UnspecifiedSequence seq ->
                 List.for_all is_empty_stmt (List.map (fun (x,_,_,_,_) -> x) seq)
    
    patch file icon bts1502.patch (584 bytes) 2013-10-18 09:42 +

-Relationships
+Relationships

-Notes

~0004133

virgile (developer)

The proper fix is to avoid considering that a statement with a label is empty. I'll check that.

~0004142

dpariente (reporter)

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)

patch is attached, apply it with patch -p0 < bts1502.patch on the top directory of Frama-C sources.

~0004144

dpariente (reporter)

Many thanks!

~0004185

virgile (developer)

fixed in svn and patch is attached.

~0004556

Fix committed to stable/neon branch.
+Notes

-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
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
2013-12-19 01:11 Source_changeset_attached => framac master 4db71fea
2014-02-12 16:53 Source_changeset_attached => framac stable/neon 4db71fea
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
+Issue History