unsigned long long constant becomes signed

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

---

Id	Project	Category	View	Due Date	Updated
ID0000376	Frama-C	Plug-in > jessie	public	2010-01-19	2010-04-13

Reporter	Mikhail Pritula	Assigned To	cmarche	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Beryllium-20090902	Target Version	-	Fixed in Version	Frama-C Boron-20100401

Description :

I have newest why and jessie and simple sample .c file: /*@ ensures \result == 1; @ */ int always_one(unsigned long long a) { if (a <= 0xFFFFFFFFFFFFFFFFull) return 1; return 0; } I run following command line: $ frama-c -jessie -jessie-atp simplify ull_constant.c which produces incorrect lemmas because this big constant becomes -1