View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000781 | Frama-C | Plug-in > from | public | 2011-04-11 12:36 | 2014-02-12 16:59 | ||||
Reporter | pascal | ||||||||
Assigned To | pascal | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C GIT, precise the release id | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000781: Sliced program computes value different from original (csmith) | ||||||||
Description | 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 | ||||||||
Additional Information | 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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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. |
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 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 ? |
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. |
![]() |
|||
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 |