Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000827Frama-CPlug-in > slicingpublic2011-05-18 10:392014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PriorityhighSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000827: sliced program computes differently from original (csmith)
DescriptionThe commands used and results obtained are in the included testslicing.sh
TagsNo tags attached.
Attached Filestgz file icon s.tgz [^] (63,223 bytes) 2011-05-18 10:39

- Relationships

-  Notes
(0001909)
pascal (reporter)
2011-05-18 10:48

I forgot to include in the archive show_each.c, the source file that is compiled into show_each-x86_32.o. Here it is:
___

#include <stdio.h>

void Frama_C_show_each(unsigned int crc)
{
  printf ("[value] Called Frama_C_show_each({%u})\n", crc);
}

void Frama_C_show_each_int(int c)
{
  printf ("[value] Called Frama_C_show_each_int({%d})\n", c);
}
(0001980)
Anne (reporter)
2011-06-16 17:10

Here is a shorter example with the same problem :
int G;
int f (void) { G = 3; return 5; }
int main (void) { G = f (); return G; }

$ frama-c -slice-return main toto.c -slice-print
gives :
int G;
void f_slice_1(void) { G = 3; return; }
int main(void) { f_slice_1(); return (G); }

In the original program, main returns 5 while in the sliced one, it returns 3.

Don't know why yet :-(
(0001981)
Anne (reporter)
2011-06-16 17:43

It is a PDG problem : the return output is processed before the implicit outputs. So the dependencies are mixed-up...
(0001983)
monate (reporter)
2011-06-17 08:50

Merci Anne !
(0004772)
Anne (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-05-18 10:39 pascal New Issue
2011-05-18 10:39 pascal Status new => assigned
2011-05-18 10:39 pascal Assigned To => Anne
2011-05-18 10:39 pascal File Added: s.tgz
2011-05-18 10:48 pascal Note Added: 0001909
2011-05-18 11:00 pascal Summary sliced program computes differently from original => sliced program computes differently from original (csmith)
2011-06-15 20:09 monate Priority normal => high
2011-06-16 17:10 Anne Note Added: 0001980
2011-06-16 17:43 Anne Note Added: 0001981
2011-06-16 17:51 svn Checkin
2011-06-16 17:51 svn Status assigned => resolved
2011-06-16 17:51 svn Resolution open => fixed
2011-06-17 08:50 monate Note Added: 0001983
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: 0004772
2014-02-12 16:59 Anne Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker