Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000721Frama-CPlug-in > value analysispublic2011-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 file icon foo_pp.c [^] (56,338 bytes) 2011-02-13 23:14 [Show Content]

- Relationships

-  Notes
(0001490)
pascal (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-02-13 23:14 regehr New Issue
2011-02-13 23:14 regehr Status new => assigned
2011-02-13 23:14 regehr Assigned To => pascal
2011-02-13 23:14 regehr File Added: foo_pp.c
2011-02-13 23:50 pascal Note Added: 0001490
2011-02-13 23:50 pascal Status assigned => acknowledged
2011-02-14 01:06 svn Checkin
2011-02-14 01:09 pascal Note Added: 0001492
2011-02-14 01:11 pascal Status acknowledged => confirmed
2011-03-04 16:50 pascal Note Added: 0001535
2011-03-04 16:54 pascal Product Version Frama-C GIT, precise the release id => Frama-C Carbon-20110201
2011-03-04 16:54 pascal Summary possible unsoundness in r11870 => Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
2011-03-04 17:58 svn Checkin
2011-03-04 17:58 svn Status confirmed => resolved
2011-03-04 17:58 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 pascal Note Added: 0004826
2014-02-12 16:59 pascal Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker