0001424: Different signed_overflow assert with rte + val

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Platform

OS Version

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

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