RTE does not check for downcast of unsigned integer
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.