Frama-C Bug Tracking System - Frama-C
View Issue Details
0000781Frama-CPlug-in > frompublic2011-04-11 12:362014-02-12 16:59
Reporterpascal 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000781: Sliced program computes value different from original (csmith)
DescriptionThe program does not contain undefined behaviors in the sense of the value analysis, as checked by ~/ppc/bin/toplevel.opt -val -slevel 5000 -cpp-command "gcc -C -E -I runtime " s.11114014.1.c -no-results -machdep x86_64

But, when compiling and executing the sliced program, the number displayed is different from the number displayed by the original program.

cuoq@ns61143:~/csmith-2.0.0$ gcc -I runtime s.11114014.1.c -o s1
s.11114014.1.c: In function ‘func_59’:
s.11114014.1.c:448: warning: comparison of distinct pointer types lacks a cast
s.11114014.1.c: In function ‘func_93’:
s.11114014.1.c:895: warning: large integer implicitly truncated to unsigned type
cuoq@ns61143:~/csmith-2.0.0$ ./s1
[value] Called Frama_C_show_each({3932636802; })
cuoq@ns61143:~/csmith-2.0.0$ gcc -I runtime s.11114014.1.s.c -o s2
cuoq@ns61143:~/csmith-2.0.0$ ./s2
[value] Called Frama_C_show_each({1079028560; })

The sliced program was obtained using 12793+patch from bug report 780, with the command:

~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.11114014.1.c -cpp-command "gcc -C -E -I. -I runtime " -machdep x86_64 -slice-calls printf -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s...s.c
Additional InformationI am in a good position to know that these big random programs can be a pain to debug. It is possible to wait for a smaller problematic program to come along.

I have quite thoroughly tested the value analysis on these random generated programs earlier. I would have liked to be more progressive and now check building blocks of the slicing, but I do not know what to use as oracle then. Only the slicing at the top of the pyramid offers a testable interface again.

Take it easy, it's only random programs.

I should replace the variadic printf by something less variadic, just in case.
TagsNo tags attached.
Attached Filestgz incorrect_sliced_value.tgz (42,146) 2011-04-11 12:36
https://bts.frama-c.com/file_download.php?file_id=192&type=bug
tgz small.tgz (10,240) 2011-04-11 12:43
https://bts.frama-c.com/file_download.php?file_id=193&type=bug

Notes
(0001703)
pascal   
2011-04-11 12:44   
(Last edited: 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   
2011-04-11 13:03   
Strange indeed ! I'll have a look. Thanks for the smaller example :-)
(0001706)
Anne   
2011-04-11 13:13   
It seems that [func_1] is erroneously sliced out... Still have to find why :-/
(0001707)
pascal   
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   
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   
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   
2011-04-11 13:39   
It seems a little bit more complex : I try to build a simple example...
(0001712)
Anne   
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   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
2011-04-11 12:36pascalNew Issue
2011-04-11 12:36pascalStatusnew => assigned
2011-04-11 12:36pascalAssigned To => Anne
2011-04-11 12:36pascalFile Added: incorrect_sliced_value.tgz
2011-04-11 12:37pascalSummarySliced program computes different value from original => Sliced program computes value different from original (csmith)
2011-04-11 12:43pascalFile Added: small.tgz
2011-04-11 12:44pascalNote Added: 0001703
2011-04-11 13:00pascalNote Edited: 0001703
2011-04-11 13:03AnneNote Added: 0001705
2011-04-11 13:04AnneStatusassigned => acknowledged
2011-04-11 13:13AnneNote Added: 0001706
2011-04-11 13:18pascalNote Added: 0001707
2011-04-11 13:28AnneNote Added: 0001709
2011-04-11 13:28AnneNote Edited: 0001709
2011-04-11 13:36pascalNote Added: 0001710
2011-04-11 13:37pascalStatusacknowledged => assigned
2011-04-11 13:37pascalAssigned ToAnne => pascal
2011-04-11 13:39AnneNote Added: 0001711
2011-04-11 13:40pascalCategoryPlug-in > slicing => Plug-in > functional dependencies
2011-04-11 14:05AnneNote Added: 0001712
2011-04-11 19:33svn
2011-04-11 19:33svnStatusassigned => resolved
2011-04-11 19:33svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12pascalSource_changeset_attached => framac master 8ee1efd5
2014-02-12 16:54pascalSource_changeset_attached => framac stable/neon 8ee1efd5
2014-02-12 16:59pascalNote Added: 0004812
2014-02-12 16:59pascalStatusclosed => resolved