0000827: sliced program computes differently from original (csmith)

(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

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.

Relationships