Frama-C Bug Tracking System - Frama-C
View Issue Details
0000786Frama-CPlug-in > slicingpublic2011-04-11 22:432014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000786: 12816: Missing label in sliced program (csmith)
DescriptionSame conventions as usual, the slicing command was

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.11215416.1.c -cpp-command "gcc -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s.11215416.1.s.c

But when compiling the sliced program:

$ gcc s.11215416.1.s.c show_each.c
s.11215416.1.s.c: In function ‘func_10_slice_1’:
s.11215416.1.s.c:163: error: label ‘_LOR’ used but not defined
TagsNo tags attached.
related to 0000799closed Anne r12925: Slicing: missing label (csmith) 
Attached Filestgz missing_label.tgz (44,239) 2011-04-11 22:43
https://bts.frama-c.com/file_download.php?file_id=195&type=bug

Notes
(0001729)
Anne   
2011-04-12 10:02   
The label is correctly marked as visible in the slicing results, but incorrectly filtered out during exportation... I am trying to find why !
(0004809)
Anne   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
2011-04-11 22:43pascalNew Issue
2011-04-11 22:43pascalStatusnew => assigned
2011-04-11 22:43pascalAssigned To => Anne
2011-04-11 22:43pascalFile Added: missing_label.tgz
2011-04-12 10:02AnneNote Added: 0001729
2011-04-12 10:42svn
2011-04-12 10:42svnStatusassigned => resolved
2011-04-12 10:42svnResolutionopen => fixed
2011-04-14 07:56svn
2011-04-20 09:11AnneRelationship addedrelated to 0000799
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12patrickSource_changeset_attached => framac master ad280f53
2013-12-19 01:12AnneSource_changeset_attached => framac master b4b73b49
2014-02-12 16:54patrickSource_changeset_attached => framac stable/neon ad280f53
2014-02-12 16:54AnneSource_changeset_attached => framac stable/neon b4b73b49
2014-02-12 16:59AnneNote Added: 0004809
2014-02-12 16:59AnneStatusclosed => resolved