2021-01-27 08:16 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000781Frama-CPlug-in > frompublic2011-04-11 12:362014-02-12 16:59
Reporterpascal 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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 Files

-Relationships
+Relationships

-Notes

~0001703

pascal (reporter)

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 (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

Last edited: 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.
+Notes

-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
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
2013-12-19 01:12 pascal Source_changeset_attached => framac master 8ee1efd5
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon 8ee1efd5
2014-02-12 16:59 pascal Note Added: 0004812
2014-02-12 16:59 pascal Status closed => resolved
+Issue History