ID0001083: **This issue was created automatically from Mantis Issue 1083. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001083 | Frama-C | Plug-in > RTE | public | 2012-02-07 | 2012-09-19 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | sylvain nahas | **Assigned To** | pherrmann | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 | ### Description : Frama-C does not behave as one could expect with the following code: unsigned char main(unsigned char a, unsigned char b) { return (a + b); } $frama-c -rte -rte-unsigned-ov toto.c -rte-print -then -val -then -werror ... unsigned char main(unsigned char a, unsigned char b) { unsigned char __retres; /*@ assert rte: (int)a+(int)b ? 2147483647 ? (int)a+(int)b ? (-0x7FFFFFFF-1); */ __retres = (unsigned char)((int)a + (int)b); return (__retres); } The plug-in generates checks for the overflow of int, but not for the downcasting of int to unsigned char. One would expect: 0 ? (int)a+(int)b ? USCHR_MAX In my opinion, this is not a bug, but rather a missing functionality. The RTE plugin should offer an option symmetrical to -rte-downcast for unsigned integers, which generates annotation for unsigned downcast.