GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0002419	Frama-C	Plug-in > RTE	public	2018-12-17	2018-12-17

Reporter	signoles	Assigned To	signoles	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C 18-Argon	Target Version	-	Fixed in Version	-

Description :

========== int main(void) { int i = 2; unsigned int j = i < 2; return 0; }

$ frama-c -check -rte -warn-unsigned-downcast -print -ocode res.c [kernel] Parsing a.c (with preprocessing) [rte] annotating function main /* Generated by Frama-C / int main(void) { int __retres; int i = 2; /@ assert rte: unsigned_downcast: (i < 2) ≤ 4294967295; / /@ assert rte: unsigned_downcast: 0 ≤ (i < 2); */ unsigned int j = (unsigned int)(i < 2); __retres = 0; return __retres; }

$ frama-c res.c [kernel] Parsing res.c (with preprocessing) [kernel:annot-error] res.c:6: Warning: comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation [kernel] User Error: warning annot-error treated as fatal error.

The terms (i < 2) should be casted to int in the generated predicates