2021-02-27 10:50 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001424Frama-CPlug-in > Evapublic2013-05-23 17:07
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130401 
Target VersionFixed in VersionFrama-C Fluorine-20130501 
Summary0001424: Different signed_overflow assert with rte + val
DescriptionI 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 InformationI was expected to have no "Value:signed_overflow" properties after rte.
Am I wrong ?
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0003868

yakobowski (manager)

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.

~0003869

Anne (reporter)

Ok. Thanks :-)
+Notes

-Issue History
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
+Issue History