Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0001264 | Frama-C | Plug-in > Eva | public | 2012-08-08 13:31 | 2013-04-19 11:05 |
|
| Reporter | yakobowski | |
| Assigned To | yakobowski | |
| Priority | low | Severity | tweak | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | | OS Version | |
| Product Version | Frama-C Nitrogen-20111001 | |
| Target Version | | Fixed in Version | Frama-C Fluorine-20130401 | |
|
| Summary | 0001264: Locations.valid_enumerate_bits enumerate invalid bits |
| Description | The program below shows that valid_enumerate_bits can return Top intervals, even on bases where the validity is completely known. This defeats the purpose of the function, and can cause very subtle bugs with the "default" flag in Offsetmap_bitwise.
---------- many.c ----------------
struct s {
int f1;
int f2;
};
struct s t[10][10];
void main() {
for (int i=0; i<10; i++) {
for (int j=0; j<10; j++) {
t[i][j].f1 = 1;
}
}
}
-------------------------------------
Command-line: frama-c -val many.c -out -plevel 80 -slevel 50
This combination of slevel/plevel will result in only one " more than foo elements to enumerate. Approximating." message, caused by the Out plugin.
----------------------------------------
Output:
[inout] Out (internal) for function main:
t[..]; i; j
The expected output is t[0..9][0..9]; i; j
|
| Steps To Reproduce | |
| Additional Information | The problem lies either in valid_enumerate_bits itself, or in Lattice_Interval_Set.from_ival_int |
| Tags | No tags attached. |
| Relationships | |
| Attached Files | |
|
| Issue History |
| Date Modified | Username | Field | Change |
| 2012-08-08 13:31 | yakobowski | New Issue | |
| 2012-08-08 13:31 | yakobowski | Status | new => assigned |
| 2012-08-08 13:31 | yakobowski | Assigned To | => pascal |
| 2013-01-25 21:39 | yakobowski | Assigned To | pascal => yakobowski |
| 2013-01-25 21:40 | yakobowski | Note Added: 0003674 | |
| 2013-02-08 19:45 | yakobowski | Note Added: 0003687 | |
| 2013-02-08 19:57 | svn | Checkin | |
| 2013-02-08 19:57 | svn | Status | assigned => resolved |
| 2013-02-08 19:57 | svn | Resolution | open => fixed |
| 2013-04-19 11:05 | signoles | Fixed in Version | => Frama-C Fluorine |
| 2013-04-19 11:05 | signoles | Status | resolved => closed |
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |