Frama-C Bug Tracking System - Frama-C
View Issue Details
0000781Frama-CPlug-in > frompublic2011-04-11 12:362014-02-12 16:59
normalminorhave not tried
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000781: Sliced program computes value different from original (csmith)
The 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
I 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.
No tags attached.
tgz incorrect_sliced_value.tgz (42,146) 2011-04-11 12:36
tgz small.tgz (10,240) 2011-04-11 12:43
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:33svnCheckin
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
2014-02-12 16:59pascalNote Added: 0004812
2014-02-12 16:59pascalStatusclosed => resolved

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