0001424: Different signed_overflow assert with rte + val - Frama-C Bug Tracking System

Frama-C Bug Tracking System

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

Platform

OS

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.

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 - 2020 MantisBT Team