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 - 2018 MantisBT Team
Powered by Mantis Bugtracker