View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001424 | Frama-C | Plug-in > Eva | public | 2013-05-22 16:40 | 2013-05-23 17:07 | ||||
Reporter | Anne | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Fluorine-20130401 | ||||||||
Target Version | Fixed in Version | Frama-C Fluorine-20130501 | |||||||
Summary | 0001424: Different signed_overflow assert with rte + val | ||||||||
Description | I use -rte to generate annotations, and then -val to check them, and usually, Value doesn't emit new annotations for 'signed_overflow' RTE. But in this case : int main (int x) { int a; if (0 <= x) a = x; else a = - x; return a; } RTE generates : /*@ assert rte: signed_overflow: -2147483648 ? x; */ Value validates it : [value] Assertion got status valid. but then emits an unchecked annotation : /*@ assert Value: signed_overflow: -x ? 2147483647; */ It looks strange, doesn't it. | ||||||||
Additional Information | I was expected to have no "Value:signed_overflow" properties after rte. Am I wrong ? | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
yakobowski (manager) 2013-05-22 17:32 |
Thanks Anne. There are two things at work here: - there is a off-by-one error in the RTE alarm - Value and RTE do not emit the same alarms: Value constrains -x, RTE constrains x. We will fix the first one in the imminent bugfix release of Fluorine. |
Anne (reporter) 2013-05-23 08:13 |
Ok. Thanks :-) |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-05-22 16:40 | Anne | New Issue | |
2013-05-22 16:40 | Anne | Status | new => assigned |
2013-05-22 16:40 | Anne | Assigned To | => yakobowski |
2013-05-22 17:32 | yakobowski | Note Added: 0003868 | |
2013-05-23 08:13 | Anne | Note Added: 0003869 | |
2013-05-23 10:14 | yakobowski | Status | assigned => resolved |
2013-05-23 10:14 | yakobowski | Resolution | open => fixed |
2013-05-23 17:07 | signoles | Fixed in Version | => Frama-C Fluorine-20130501 |
2013-05-23 17:07 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |