0000781: Sliced program computes value different from original (csmith)

(0001703)
pascal (reporter)
2011-04-11 12:44
edited on: 2011-04-11 13:00

small.tgz contains a problem with the same description, but smaller files. The name is wrong: it's an uncompressed tar file.

(0001705)
Anne (reporter)
2011-04-11 13:03

Strange indeed ! I'll have a look. Thanks for the smaller example :-)

(0001706)
Anne (reporter)
2011-04-11 13:13

It seems that [func_1] is erroneously sliced out... Still have to find why :-/

(0001707)
pascal (reporter)
2011-04-11 13:18

Strange... func_1 is always the entry point of the randomly generated part. When I said the value analysis was well tested on generated programs of this kind, I made a mistake : I had well tested the 32-bit default target. I changed to the 64-bit target at the same time I moved to look for bugs in slicing. I should perhaps go back to the 32-bit target for slicing, because I have just obtained my first 64-bit target bug in the value analysis (after half a day only of random generation).

(0001709)
Anne (reporter)
2011-04-11 13:28
edited on: 2011-04-11 13:28

With option [-deps], we get : Function func_1: \result FROM g_4 which is strange because it seems that [func_1] modifies [g_4]... With option [-calldeps] : call func_1 at statement 648: \result FROM g_4 In the GUI: Function: main Statement: 648 (line 46 in s.11112949.1.c) Modifies g_4; l_5; __retres which is better ! Where does it take this information from ?

(0001710)
pascal (reporter)
2011-04-11 13:36

The "Modifies ..." in the GUI displays the imperative outputs. So we seem to have narrowed it to an issue where a global variable that is modified along an execution path that terminates is not on the left-hand side of the FROMs of the function.

(0001711)
Anne (reporter)
2011-04-11 13:39

It seems a little bit more complex : I try to build a simple example...

(0001712)
Anne (reporter)
2011-04-11 14:05

It seems to be related to the cast on the call return type. Example : typedef unsigned char T; // typedef int T; int G; T f (int left, int right ) { return left + right; } void main (void) { int * p = &G; *p = f (G, 3); } With the first definition of T, the [main] dependencies are wrong. The are ok with the second one...

(0004812)
pascal (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-04-11 12:36	pascal	New Issue
2011-04-11 12:36	pascal	Status	new => assigned
2011-04-11 12:36	pascal	Assigned To	=> Anne
2011-04-11 12:36	pascal	File Added: incorrect_sliced_value.tgz
2011-04-11 12:37	pascal	Summary	Sliced program computes different value from original => Sliced program computes value different from original (csmith)
2011-04-11 12:43	pascal	File Added: small.tgz
2011-04-11 12:44	pascal	Note Added: 0001703
2011-04-11 13:00	pascal	Note Edited: 0001703
2011-04-11 13:03	Anne	Note Added: 0001705
2011-04-11 13:04	Anne	Status	assigned => acknowledged
2011-04-11 13:13	Anne	Note Added: 0001706
2011-04-11 13:18	pascal	Note Added: 0001707
2011-04-11 13:28	Anne	Note Added: 0001709
2011-04-11 13:28	Anne	Note Edited: 0001709
2011-04-11 13:36	pascal	Note Added: 0001710
2011-04-11 13:37	pascal	Status	acknowledged => assigned
2011-04-11 13:37	pascal	Assigned To	Anne => pascal
2011-04-11 13:39	Anne	Note Added: 0001711
2011-04-11 13:40	pascal	Category	Plug-in > slicing => Plug-in > functional dependencies
2011-04-11 14:05	Anne	Note Added: 0001712
2011-04-11 19:33	svn	Checkin
2011-04-11 19:33	svn	Status	assigned => resolved
2011-04-11 19:33	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	pascal	Note Added: 0004812
2014-02-12 16:59	pascal	Status	closed => resolved

Notes
(0001703) pascal (reporter) 2011-04-11 12:44 edited on: 2011-04-11 13:00	small.tgz contains a problem with the same description, but smaller files. The name is wrong: it's an uncompressed tar file.

(0001705) Anne (reporter) 2011-04-11 13:03	Strange indeed ! I'll have a look. Thanks for the smaller example :-)

(0001706) Anne (reporter) 2011-04-11 13:13	It seems that [func_1] is erroneously sliced out... Still have to find why :-/

(0001707) pascal (reporter) 2011-04-11 13:18	Strange... func_1 is always the entry point of the randomly generated part. When I said the value analysis was well tested on generated programs of this kind, I made a mistake : I had well tested the 32-bit default target. I changed to the 64-bit target at the same time I moved to look for bugs in slicing. I should perhaps go back to the 32-bit target for slicing, because I have just obtained my first 64-bit target bug in the value analysis (after half a day only of random generation).

(0001709) Anne (reporter) 2011-04-11 13:28 edited on: 2011-04-11 13:28	With option [-deps], we get : Function func_1: \result FROM g_4 which is strange because it seems that [func_1] modifies [g_4]... With option [-calldeps] : call func_1 at statement 648: \result FROM g_4 In the GUI: Function: main Statement: 648 (line 46 in s.11112949.1.c) Modifies g_4; l_5; __retres which is better ! Where does it take this information from ?

(0001710) pascal (reporter) 2011-04-11 13:36	The "Modifies ..." in the GUI displays the imperative outputs. So we seem to have narrowed it to an issue where a global variable that is modified along an execution path that terminates is not on the left-hand side of the FROMs of the function.

(0001711) Anne (reporter) 2011-04-11 13:39	It seems a little bit more complex : I try to build a simple example...

(0001712) Anne (reporter) 2011-04-11 14:05	It seems to be related to the cast on the call return type. Example : typedef unsigned char T; // typedef int T; int G; T f (int left, int right ) { return left + right; } void main (void) { int * p = &G; *p = f (G, 3); } With the first definition of T, the [main] dependencies are wrong. The are ok with the second one...

(0004812) pascal (reporter) 2014-02-12 16:59	Fix committed to stable/neon branch.

Relationships