GitLab

ID0000798: This issue was created automatically from Mantis Issue 798. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000798	Frama-C	Plug-in > Eva	public	2011-04-17	2014-02-12

Reporter	pascal	Assigned To	pascal	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

short x = -10; int y, z, t;

unsigned short f(void) { return x; }

unsigned short g(void) { unsigned short l = (unsigned short)&x; return l; }

main(){ y = (unsigned short)&x; z = f(); t = g(); }

y and z are computed correctly, but t is wrong:

[value] Values for function main: y IN {65526; } z IN {65526; } t IN {-10; }