Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Filestgz file icon nt.tgz [^] (37,873 bytes) 2011-04-20 18:11

- Relationships
related to 0000787closedAnne same conditions as 786, sliced program does not terminate when original does (csmith) 

-  Notes
(0001802)
Anne (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
2011-04-28 13:58

Fixed in rev 13064.

- Issue History
Date Modified Username Field Change
2011-04-20 16:33 pascal New Issue
2011-04-20 16:33 pascal Status new => assigned
2011-04-20 16:33 pascal Assigned To => Anne
2011-04-20 17:03 Anne Note Added: 0001800
2011-04-20 18:11 pascal File Added: nt.tgz
2011-04-21 09:09 Anne Relationship added related to 0000787
2011-04-21 09:16 Anne Note Deleted: 0001800
2011-04-21 10:11 Anne Note Added: 0001802
2011-04-21 10:19 pascal Note Added: 0001803
2011-04-21 13:20 Anne Note Added: 0001805
2011-04-28 13:58 Anne Note Added: 0001817
2011-04-28 13:58 Anne Status assigned => resolved
2011-04-28 13:58 Anne Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker