Frama-C Bug Tracking System - Frama-C
View Issue Details
0000721Frama-CPlug-in > Evapublic2011-02-13 23:142014-02-12 16:59
Reporterregehr 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000721: Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
DescriptionThe attached program, analyzed like this:

  toplevel.opt -val -slevel 25 foo_pp.c

causes Frama-C to emit this assertion:

   assert(*(unsigned int*)&g_115 == 9362872);

However, running the program gives the value of g_115 as 23992 at the end of execution.

This is on Ubuntu 10.10 on x86.
TagsNo tags attached.
Attached Filesc foo_pp.c (56,338) 2011-02-13 23:14
https://bts.frama-c.com/file_download.php?file_id=173&type=bug

Notes
(0001490)
pascal   
2011-02-13 23:50   
This test reveals an issue when passing bitfields in argument to functions. But this issue may not be the one causing the incorrect analysis, it's just the first one I noticed.
(0001492)
pascal   
2011-02-14 01:09   
In 11872 no alarm is emitted and the predicted value of g_115 is still the same (different from gcc -m32), so it's indeed a soundness issue other than the first one that caught my eye.
(0001535)
pascal   
2011-03-04 16:50   
The first correctness problem that, with 12189, happens in this program, can be reproduced with the program below.

struct t1 { unsigned int a:2; int b:4; int c:22;} h;

struct t1 ini = { 14, -55, 99999 } ;

main() { Frama_C_dump_each(); return 0; }
(0004826)
pascal   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
2011-02-13 23:14regehrNew Issue
2011-02-13 23:14regehrStatusnew => assigned
2011-02-13 23:14regehrAssigned To => pascal
2011-02-13 23:14regehrFile Added: foo_pp.c
2011-02-13 23:50pascalNote Added: 0001490
2011-02-13 23:50pascalStatusassigned => acknowledged
2011-02-14 01:06svn
2011-02-14 01:09pascalNote Added: 0001492
2011-02-14 01:11pascalStatusacknowledged => confirmed
2011-03-04 16:50pascalNote Added: 0001535
2011-03-04 16:54pascalProduct VersionFrama-C GIT, precise the release id => Frama-C Carbon-20110201
2011-03-04 16:54pascalSummarypossible unsoundness in r11870 => Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
2011-03-04 17:58svn
2011-03-04 17:58svnStatusconfirmed => resolved
2011-03-04 17:58svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12pascalSource_changeset_attached => framac master 45f30f4f
2013-12-19 01:12pascalSource_changeset_attached => framac master 2495456d
2014-02-12 16:54pascalSource_changeset_attached => framac stable/neon 45f30f4f
2014-02-12 16:54pascalSource_changeset_attached => framac stable/neon 2495456d
2014-02-12 16:59pascalNote Added: 0004826
2014-02-12 16:59pascalStatusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva