2021-03-01 05:55 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001024Frama-CPlug-in > Evapublic2014-02-12 16:58
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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

-Relationships
+Relationships

-Notes

~0002481

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.

~0002482

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)

~0002483

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)

~0002484

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.

~0002486

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.

~0002487

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.

~0002488

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.

~0002489

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.

~0002730

yakobowski (manager)

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

~0004698

yakobowski (manager)

Fix committed to stable/neon branch.
+Notes

-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