Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000802Frama-CPlug-in > slicingpublic2011-04-20 16:332011-10-10 14:14
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000802: r12951, sliced program does not terminate
DescriptionThe original program terminates:

gcc -I runtime -m32 show_each.c nonterminatingslice/s.20153409.4.c

./a.out
[value] Called Frama_C_show_each({1696784233; })
[value] Called Frama_C_show_each({538004427; })
[value] Called Frama_C_show_each({3729539076; })
[value] Called Frama_C_show_each({3984566477; })
[value] Called Frama_C_show_each({2563812225; })
[value] Called Frama_C_show_each({1179156549; })
[value] Called Frama_C_show_each({1179156549; })

The sliced one doesn't.

The slicing command was:

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms nonterminatingslice/s.20153409.4.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.c
TagsNo tags attached.
Relationships
related to 0000787closed Anne same conditions as 786, sliced program does not terminate when original does (csmith) 
Attached Filestgz nt.tgz (37,873) 2011-04-20 18:11
https://bts.frama-c.com/file_download.php?file_id=204&type=bug

Notes
(0001802)
Anne   
2011-04-21 10:11   
In 0000787, we have seen that there is a problem with unreachable control statement. I thought that it could happen only if we use the value analysis results, but unfortunately, it seems that it can also happen in other cases such as this one:

int g_4;
void main(void) {
  while (1) {
    g_4 = 6;
    while (1) {
      return ;
      return ; // <--- problem here
    }
  }
}
frama-c -slice-value g_4 toto.c -slice-print
/* Generated by Frama-C */
int g_4 ;
void main(void)
{
  while (1) {
    g_4 = (int )6L;
    while (1) { } // <-- infinite loop
    }
  return;
}

This doesn't happen when the second [return] is removed from the example...

Don't know yet how to fix that, but have to find out !
(0001803)
pascal   
2011-04-21 10:19   
Would the alternative solution to 787 (postdominator analysis that takes into account unreachable statements) fix this as well?
(0001805)
Anne   
2011-04-21 13:20   
Yes : I think so.
But I am wondering if it wouldn't be easier to have another tool to remove the dead code, optionally using the value analysis results... What do you think ?
(0001817)
Anne   
2011-04-28 13:58   
Fixed in rev 13064.

Issue History
Date ModifiedUsernameFieldChange
2011-04-20 16:33pascalNew Issue
2011-04-20 16:33pascalStatusnew => assigned
2011-04-20 16:33pascalAssigned To => Anne
2011-04-20 18:11pascalFile Added: nt.tgz
2011-04-21 09:09AnneRelationship addedrelated to 0000787
2011-04-21 10:11AnneNote Added: 0001802
2011-04-21 10:19pascalNote Added: 0001803
2011-04-21 13:20AnneNote Added: 0001805
2011-04-28 13:58AnneNote Added: 0001817
2011-04-28 13:58AnneStatusassigned => resolved
2011-04-28 13:58AnneResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed