Missing cast in code generated by RTE
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