Frama-C Bug Tracking System - Frama-C
View Issue Details
0001968Frama-CPlug-in > Evapublic2014-11-13 21:132016-06-21 14:08
pascal 
valentin.perrelle 
normalmajoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Aluminium 
0001968: Values inferred for 32-bit variable do not fit in 32-bit type
The 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
No tags attached.
Issue History
2014-11-13 21:13pascalNew Issue
2014-11-13 21:13pascalStatusnew => assigned
2014-11-13 21:13pascalAssigned To => yakobowski
2015-12-04 22:21yakobowskiAssigned Toyakobowski => valentin.perrelle
2016-01-14 01:01yakobowskiStatusassigned => resolved
2016-01-14 01:01yakobowskiResolutionopen => fixed
2016-06-21 14:08signolesFixed in Version => Frama-C Aluminium
2016-06-21 14:08signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

There are no notes attached to this issue.