Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001424Frama-CPlug-in > Evapublic2013-05-22 16:402013-05-23 17:07
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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

-  Notes
(0003868)
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.
(0003869)
Anne (reporter)
2013-05-23 08:13

Ok. Thanks :-)

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker