Frama-C Bug Tracking System - Frama-C
View Issue Details
0000807Frama-CPlug-in > slicingpublic2011-04-28 14:492014-02-12 16:59
pascal 
Anne 
normalminorhave not tried
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000807: sliced program does not terminate (csmith)
same conditions as bug 806. Compile the original with gcc -m32 -D__FRAMAC -I runtime show_each.c noterm.c (executable terminates) and the sliced program with gcc -m32 show_each.c noterm.s.c
No tags attached.
c noterm.c (7,874) 2011-04-28 14:49
https://bts.frama-c.com/file_download.php?file_id=208&type=bug
Issue History
2011-04-28 14:49pascalNew Issue
2011-04-28 14:49pascalStatusnew => assigned
2011-04-28 14:49pascalAssigned To => Anne
2011-04-28 14:49pascalFile Added: noterm.c
2011-04-28 14:54pascalSummarysliced program does not terminate => sliced program does not terminate (csmith)
2011-04-28 17:12AnneNote Added: 0001826
2011-04-28 17:22AnneNote Added: 0001827
2011-04-28 18:01AnneNote Added: 0001828
2011-04-29 10:16AnneNote Added: 0001831
2011-04-29 10:41svnCheckin
2011-04-29 10:41svnStatusassigned => resolved
2011-04-29 10:41svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59AnneNote Added: 0004800
2014-02-12 16:59AnneStatusclosed => resolved

Notes
(0001826)
Anne   
2011-04-28 17:12   
I managed to reduce the problem to : frama-c -slice-calls printf toto.c \ -then-on 'Slicing export' -print -ocode toto.s.c with toto.c : #include int G; void f (void) { int b = 7; int a = 2; if ((( a || 42) && b)) { while (1) { G = 21; return; } } } int main (void) { f(); printf ("RES = %d\n", G); return 0; } but now, I have to see what's going wrong...
(0001827)
Anne   
2011-04-28 17:22   
What I really don't understand is that if I put the internal form of the condition in the source code : if (a) { goto _LOR; } else { _LOR: /* internal */ ; if (b) { while (1) { ... } } } It works !
(0001828)
Anne   
2011-04-28 18:01   
Ok : in the generated internal form, there is a statement block in the else branch. This statement is unreachable since [a = 2] and the label is inside the block. That might be the reason why it doesn't work. Anyway, this is at least the difference between the 2 examples. To be continued...
(0001831)
Anne   
2011-04-29 10:16   
This is a problem with the lexical successor computation when there are unreachable statements. Will be fixed soon...
(0004800)
Anne   
2014-02-12 16:59   
Fix committed to stable/neon branch.