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