Frama-C Bug Tracking System - Frama-C
View Issue Details
0001024Frama-CPlug-in > Evapublic2011-11-19 10:572014-02-12 16:58
pascal 
yakobowski 
normalmajoralways
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901Frama-C Oxygen-20120901 
0001024: Emitted assertion wrongly reduces to bottom (apparently) (csmith)
Soundness bug, probably caused by wrong reduction on emitted assertions. ~/ppc/bin/toplevel.opt -slevel 5 -slevel-function main:0 -no-results -val-signed-overflow-alarms -cpp-command "gcc -C -E -Iruntime -m32 " a.c -precise-unions -val ... a.c:236:[value] Assertion got status invalid (stopping propagation). [value] Recording results for func_1 [value] Done for function func_1 [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ====== L'analyse avec -slevel 5 dit que la fin du programme et le Frama_C_dump... n'est pas atteint. Pourtant, il l'est comme le montre l'analyse avec -slevel 5000000: ~/ppc/bin/toplevel.opt -slevel 5000000 -slevel-function main:0 -no-results -val-signed-overflow-alarms -cpp-command "gcc -C -E -Iruntime -m32 " a.c -precise-unions -val ... && *(unsigned short*)&g_1113 == 65535) End of Frama_C_dump_assert_each output [value] Recording results for main [value] done for function main [value] ====== VALUES COMPUTED ======
No tags attached.
tgz emassert.tgz (78,479) 2011-11-19 10:57
https://bts.frama-c.com/file_download.php?file_id=297&type=bug
Issue History
2011-11-19 10:57pascalNew Issue
2011-11-19 10:57pascalStatusnew => assigned
2011-11-19 10:57pascalAssigned To => yakobowski
2011-11-19 10:57pascalFile Added: emassert.tgz
2011-11-19 10:59pascalNote Added: 0002481
2011-11-19 11:14yakobowskiNote Added: 0002482
2011-11-19 11:16pascalNote Added: 0002483
2011-11-19 11:32yakobowskiNote Added: 0002484
2011-11-19 11:40yakobowskiNote Added: 0002485
2011-11-19 11:42yakobowskiNote Deleted: 0002485
2011-11-19 12:49yakobowskiNote Added: 0002486
2011-11-19 12:52pascalNote Added: 0002487
2011-11-19 12:53yakobowskiNote Added: 0002488
2011-11-19 12:58pascalNote Added: 0002489
2011-11-21 23:38svnCheckin
2012-02-23 18:31yakobowskiNote Added: 0002730
2012-04-08 00:05yakobowskiTarget Version => Frama-C Oxygen-2012xx01
2012-04-16 22:13svnCheckin
2012-04-16 22:13svnStatusassigned => resolved
2012-04-16 22:13svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:58yakobowskiNote Added: 0004698
2014-02-12 16:58yakobowskiStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002481)
pascal   
2011-11-19 10:59   
This bug was found a long while ago (at least a month) and is still there. It is unlikely to be related to recent changes in \initialized interpretation. Note that with -slevel 5, there are two emitted assertions for line 236.
(0002482)
yakobowski   
2011-11-19 11:14   
Cannot reproduce. Using string.h from my os results in a platform-dependent link error. With -nostdinc and Frama-C libc, I get runtime/safe_math.h:452: error: macro "__smax" requires 2 arguments, but only 1 given (this is one line amongst around 30 similar ones)
(0002483)
pascal   
2011-11-19 11:16   
a.i contains a pre-processed version of the file that should be okay (it's almost the same but was pre-processed before a call to Frama_C_dump_each() was added, hence a one-line difference in error locations)
(0002484)
yakobowski   
2011-11-19 11:32   
No need to search for long: the faulty code is tmp = (type_to_cast)f(); and the emitted assertion is \assert \initialized(&tmp) This is trivially almost always false, so the problem is not in the evaluation. The good question is: why is this assertion emitted at all? The warning should instead be on the line 'return foo;' inside f. There is no currently none, and I believe I known why, but the warning on the call point is plain wrong.
(0002486)
yakobowski   
2011-11-19 12:49   
I haven't been able to reproduce the problem on a smaller example. It seems one needs an "undefined sequence" to have the exact same parsed tree, but on my examples the assertion occurs after the call.
(0002487)
pascal   
2011-11-19 12:52   
There are prototypal automatic tools available for reducing a C program to a smaller one that exhibits the same bug in Frama-C. Let's try these Monday. It is high time we looked at them in any case.
(0002488)
yakobowski   
2011-11-19 12:53   
Temporary workaround: use -no-collapse-call-cast, which is the source of All Evils. I'm not sure a workaround exists as long as some operation can introduce a RTE between a call and the storing of the call result.
(0002489)
pascal   
2011-11-19 12:58   
> runtime/safe_math.h:452: error: macro "__smax" requires 2 arguments, but only 1 given (this is one line amongst around 30 similar ones) Most headers in Frama-C/share produce syntax errors as soon as the macros in them are used. They have never been tested.
(0002730)
yakobowski   
2012-02-23 18:31   
Will be fixed by making -collapse-call-cast less agressive.
(0004698)
yakobowski   
2014-02-12 16:58   
Fix committed to stable/neon branch.