Frama-C Bug Tracking System - Frama-C
View Issue Details
0000808Frama-CPlug-in > slicingpublic2011-04-29 12:482014-02-12 16:59
pascal 
Anne 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000808: r13089 sliced program computes differently from original (csmith)
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.29114540.2.c -cpp-command "gcc -m32 -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode s.29114540.2.s.c original compiled as 32-bit produces: each: 1877464688 each: 923383238 each: 3118711398 each: 2770598846 each: 3750958151 each: 1873579612 each: 1348507732 each: 1348507732 sliced program produces: each: 1877464688 each: 923383238 each: 3118711398 each: 2770598846 each: 130171288 each: 3207316278 each: 3201788839 each: 3201788839 It seems that the sliced program does not preserve the value of g_14 (see sequence of calls to transparent_crc() in main()).
No tags attached.
tgz di.tgz (38,911) 2011-04-29 12:48
https://bts.frama-c.com/file_download.php?file_id=209&type=bug
Issue History
2011-04-29 12:48pascalNew Issue
2011-04-29 12:48pascalStatusnew => assigned
2011-04-29 12:48pascalAssigned To => Anne
2011-04-29 12:48pascalFile Added: di.tgz
2011-04-29 12:51pascalNote Added: 0001833
2011-04-29 14:04AnneNote Added: 0001834
2011-05-13 09:54AnneNote Added: 0001879
2011-05-13 09:59AnneNote Added: 0001880
2011-05-13 11:22svnCheckin
2011-05-13 11:22svnStatusassigned => resolved
2011-05-13 11:22svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59AnneNote Added: 0004790
2014-02-12 16:59AnneStatusclosed => resolved

Notes
(0001833)
pascal   
2011-04-29 12:51   
Note: the value analysis ~/ppc/bin/toplevel.opt -cpp-command "gcc -m32 -C -E -I runtime -D__FRAMAC " -val -slevel 5000 s.29114540.2.c -no-results -machdep x86_32 computes the correct value for the CRC: [value] Called Frama_C_show_each({1348507732})
(0001834)
Anne   
2011-04-29 14:04   
Waouh : a new kind of bug ! It will be a change from infinite loop problem ;-)
(0001879)
Anne   
2011-05-13 09:54   
The problem is that we have something like : if (c) { ... goto L; ... } else { ... L: ... } and the value analysis knows that [c != 0]. So the slicing (rightly) says that the condition can be sliced out. Since neither the 'then' block, nor the 'else' block are invisible, the filter preserves the [if] statement, but because it knows that the condition doesn't mater, it (wrongly) chose anything, and substitutes [c] by ... [0] ! I don't know yet how to fix that, but I'll try to find out.
(0001880)
Anne   
2011-05-13 09:59   
A small example : frama-c -slice-return main -slice-print toto.c int main (void) { int x; int i = 1; if (i) { x = 1; goto L; } else { x = 0; L: x++; } return x; }
(0004790)
Anne   
2014-02-12 16:59   
Fix committed to stable/neon branch.