Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000808Frama-CPlug-in > slicingpublic2011-04-29 12:482014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000808: r13089 sliced program computes differently from original (csmith)
Description~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.29114540.2.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.29114540.2.s.c

original compiled as 32-bit produces:

each: 1877464688
each: 923383238
each: 3118711398
each: 2770598846
each: 3750958151
each: 1873579612
each: 1348507732
each: 1348507732

sliced program produces:

each: 1877464688
each: 923383238
each: 3118711398
each: 2770598846
each: 130171288
each: 3207316278
each: 3201788839
each: 3201788839

It seems that the sliced program does not preserve the value of g_14 (see sequence of calls to transparent_crc() in main()).
TagsNo tags attached.
Attached Filestgz file icon di.tgz [^] (38,911 bytes) 2011-04-29 12:48

- Relationships

-  Notes
(0001833)
pascal (reporter)
2011-04-29 12:51

Note: the value analysis

~/ppc/bin/toplevel.opt -cpp-command "gcc -m32 -C -E -I runtime -D__FRAMAC " -val -slevel 5000 s.29114540.2.c -no-results -machdep x86_32

computes the correct value for the CRC:

[value] Called Frama_C_show_each({1348507732})
(0001834)
Anne (reporter)
2011-04-29 14:04

Waouh : a new kind of bug ! It will be a change from infinite loop problem ;-)
(0001879)
Anne (reporter)
2011-05-13 09:54

The problem is that we have something like :
  if (c) { ... goto L; ... } else { ... L: ... }
and the value analysis knows that [c != 0]. So the slicing (rightly) says that the condition can be sliced out. Since neither the 'then' block, nor the 'else' block are invisible, the filter preserves the [if] statement, but because it knows that the condition doesn't mater, it (wrongly) chose anything, and substitutes [c] by ... [0] !

I don't know yet how to fix that, but I'll try to find out.
(0001880)
Anne (reporter)
2011-05-13 09:59

A small example : frama-c -slice-return main -slice-print toto.c

int main (void) {
  int x; int i = 1;
  if (i) { x = 1; goto L; }
  else { x = 0; L: x++; }
  return x;
}
(0004790)
Anne (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-04-29 12:48 pascal New Issue
2011-04-29 12:48 pascal Status new => assigned
2011-04-29 12:48 pascal Assigned To => Anne
2011-04-29 12:48 pascal File Added: di.tgz
2011-04-29 12:51 pascal Note Added: 0001833
2011-04-29 14:04 Anne Note Added: 0001834
2011-05-13 09:54 Anne Note Added: 0001879
2011-05-13 09:59 Anne Note Added: 0001880
2011-05-13 11:22 svn Checkin
2011-05-13 11:22 svn Status assigned => resolved
2011-05-13 11:22 svn 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
2014-02-12 16:59 Anne Note Added: 0004790
2014-02-12 16:59 Anne Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker