Values inferred for 32-bit variable do not fit in 32-bit type
ID0001968: This issue was created automatically from Mantis Issue 1968. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001968 | Frama-C | Plug-in > Eva | public | 2014-11-13 | 2016-06-21 |
| Reporter | pascal | Assigned To | valentin.perrelle | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Aluminium |
Description :
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