Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000781Frama-CPlug-in > frompublic2011-04-11 12:362014-02-12 16:59
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityhave not tried
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 file icon incorrect_sliced_value.tgz [^] (42,146 bytes) 2011-04-11 12:36
tgz file icon small.tgz [^] (10,240 bytes) 2011-04-11 12:43

- Relationships

-  Notes
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.
Anne (reporter)
2011-04-11 13:03

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

It seems that [func_1] is erroneously sliced out... Still have to find why :-/
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).
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 ?
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.
Anne (reporter)
2011-04-11 13:39

It seems a little bit more complex : I try to build a simple example...
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...
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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker