Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001024Frama-CPlug-in > value analysispublic2011-11-19 10:572014-02-12 16:58
Reporterpascal 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filestgz file icon emassert.tgz [^] (78,479 bytes) 2011-11-19 10:57

- Relationships

-  Notes
(0002481)
pascal (reporter)
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 (manager)
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 (reporter)
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 (manager)
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 (manager)
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 (reporter)
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 (manager)
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 (reporter)
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 (manager)
2012-02-23 18:31

Will be fixed by making -collapse-call-cast less agressive.
(0004698)
yakobowski (manager)
2014-02-12 16:58

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 11:40 yakobowski Note Added: 0002485
2011-11-19 11:42 yakobowski Note Deleted: 0002485
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 Checkin
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 Checkin
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
2014-02-12 16:58 yakobowski Note Added: 0004698
2014-02-12 16:58 yakobowski Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker