Unsoundness in value analysis when bitfield initializer exceeds range (csmith)
ID0000721: This issue was created automatically from Mantis Issue 721. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000721 | Frama-C | Plug-in > Eva | public | 2011-02-13 | 2014-02-12 |
| Reporter | regehr | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
The 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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information