Frama-C Bug Tracking System - Frama-C
View Issue Details
0000827Frama-CPlug-in > slicingpublic2011-05-18 10:392014-02-12 16:59
pascal 
Anne 
highminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000827: sliced program computes differently from original (csmith)
The commands used and results obtained are in the included testslicing.sh
No tags attached.
tgz s.tgz (63,223) 2011-05-18 10:39
https://bts.frama-c.com/file_download.php?file_id=218&type=bug
Issue History
2011-05-18 10:39pascalNew Issue
2011-05-18 10:39pascalStatusnew => assigned
2011-05-18 10:39pascalAssigned To => Anne
2011-05-18 10:39pascalFile Added: s.tgz
2011-05-18 10:48pascalNote Added: 0001909
2011-05-18 11:00pascalSummarysliced program computes differently from original => sliced program computes differently from original (csmith)
2011-06-15 20:09monatePrioritynormal => high
2011-06-16 17:10AnneNote Added: 0001980
2011-06-16 17:43AnneNote Added: 0001981
2011-06-16 17:51svnCheckin
2011-06-16 17:51svnStatusassigned => resolved
2011-06-16 17:51svnResolutionopen => fixed
2011-06-17 08:50monateNote Added: 0001983
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59AnneNote Added: 0004772
2014-02-12 16:59AnneStatusclosed => resolved

Notes
(0001909)
pascal   
2011-05-18 10:48   
I forgot to include in the archive show_each.c, the source file that is compiled into show_each-x86_32.o. Here it is: ___ #include void Frama_C_show_each(unsigned int crc) { printf ("[value] Called Frama_C_show_each({%u})\n", crc); } void Frama_C_show_each_int(int c) { printf ("[value] Called Frama_C_show_each_int({%d})\n", c); }
(0001980)
Anne   
2011-06-16 17:10   
Here is a shorter example with the same problem : int G; int f (void) { G = 3; return 5; } int main (void) { G = f (); return G; } $ frama-c -slice-return main toto.c -slice-print gives : int G; void f_slice_1(void) { G = 3; return; } int main(void) { f_slice_1(); return (G); } In the original program, main returns 5 while in the sliced one, it returns 3. Don't know why yet :-(
(0001981)
Anne   
2011-06-16 17:43   
It is a PDG problem : the return output is processed before the implicit outputs. So the dependencies are mixed-up...
(0001983)
monate   
2011-06-17 08:50   
Merci Anne !
(0004772)
Anne   
2014-02-12 16:59   
Fix committed to stable/neon branch.