2021-03-01 05:55 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001024Frama-CPlug-in > Evapublic2014-02-12 16:58
Assigned Toyakobowski 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFrama-C Oxygen-20120901Fixed in VersionFrama-C Oxygen-20120901 
Summary0001024: Emitted assertion wrongly reduces to bottom (apparently) (csmith)
DescriptionSoundness 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 ======
TagsNo tags attached.
Attached Files




pascal (reporter)

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.


yakobowski (manager)

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)


pascal (reporter)

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)


yakobowski (manager)

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.


yakobowski (manager)

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.


pascal (reporter)

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.


yakobowski (manager)

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.


pascal (reporter)

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


yakobowski (manager)

Will be fixed by making -collapse-call-cast less agressive.


yakobowski (manager)

Fix committed to stable/neon branch.

-Issue History
Date Modified Username Field Change
2011-11-19 10:57 pascal New Issue
2011-11-19 10:57 pascal Status new => assigned
2011-11-19 10:57 pascal Assigned To => yakobowski
2011-11-19 10:57 pascal File Added: emassert.tgz
2011-11-19 10:59 pascal Note Added: 0002481
2011-11-19 11:14 yakobowski Note Added: 0002482
2011-11-19 11:16 pascal Note Added: 0002483
2011-11-19 11:32 yakobowski Note Added: 0002484
2011-11-19 12:49 yakobowski Note Added: 0002486
2011-11-19 12:52 pascal Note Added: 0002487
2011-11-19 12:53 yakobowski Note Added: 0002488
2011-11-19 12:58 pascal Note Added: 0002489
2011-11-21 23:38 svn
2012-02-23 18:31 yakobowski Note Added: 0002730
2012-04-08 00:05 yakobowski Target Version => Frama-C Oxygen-2012xx01
2012-04-16 22:13 svn
2012-04-16 22:13 svn Status assigned => resolved
2012-04-16 22:13 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master d9cf7118
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon d9cf7118
2014-02-12 16:58 yakobowski Note Added: 0004698
2014-02-12 16:58 yakobowski Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History