Frama-C Bug Tracking System - Frama-C
View Issue Details
0000809Frama-CPlug-in > slicingpublic2011-04-29 13:082011-10-10 14:14
pascal 
Anne 
normalminorhave not tried
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000809: sliced program does not terminate (csmith)
same conditions as 808
No tags attached.
tgz nt.tgz (6,839) 2011-04-29 13:08
https://bts.frama-c.com/file_download.php?file_id=210&type=bug
Issue History
2011-04-29 13:08pascalNew Issue
2011-04-29 13:08pascalStatusnew => assigned
2011-04-29 13:08pascalAssigned To => Anne
2011-04-29 13:08pascalFile Added: nt.tgz
2011-05-13 13:21AnneNote Added: 0001884
2011-07-28 17:00AnneNote Added: 0002067
2011-07-28 17:00AnneStatusassigned => resolved
2011-07-28 17:00AnneResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001884)
Anne   
2011-05-13 13:21   
Simple example : frama-c -slice-value G toto.c -slice-print

int G;

void main (void) {
  while (1) {
    G = 10;
    goto L;
    while (G) {
L: return;
    }
  }
}

gives :

int G;
void main(void)
{
  while (1) { G = 10; }
  return;
}
(0002067)
Anne   
2011-07-28 17:00   
fixed in rev 14384