Different signed_overflow assert with rte + val
ID0001424: This issue was created automatically from Mantis Issue 1424. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001424 | Frama-C | Plug-in > Eva | public | 2013-05-22 | 2013-05-23 |
| Reporter | Anne | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130401 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130501 |
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 ?