Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001968Frama-CPlug-in > Evapublic2014-11-13 21:132016-06-21 14:08
Reporterpascal 
Assigned Tovalentin.perrelle 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0001968: Values inferred for 32-bit variable do not fit in 32-bit type
DescriptionThe values inferred for the variable i below are 64-bit values that wouldn't even fit the 32-bit unsigned int that variable i is. Program: int main() { Frama_C_show_each(sizeof(unsigned int)); unsigned int i = 0; while (u()) { i+=2; } } $ frama-c -val t.c … [value] Called Frama_C_show_each({4}) … [value] Values at end of function main: i ∈ [0..9223372036854775806],0%2
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-11-13 21:13 pascal New Issue
2014-11-13 21:13 pascal Status new => assigned
2014-11-13 21:13 pascal Assigned To => yakobowski
2015-12-04 22:21 yakobowski Assigned To yakobowski => valentin.perrelle
2016-01-14 01:01 yakobowski Status assigned => resolved
2016-01-14 01:01 yakobowski Resolution open => fixed
2016-06-21 14:08 signoles Fixed in Version => Frama-C Aluminium
2016-06-21 14:08 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker