GitLab

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