Frama-C Bug Tracking System - Frama-C
View Issue Details
0001083Frama-CPlug-in > RTEpublic2012-02-07 11:052012-09-19 17:16
sylvain nahas 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001083: RTE does not check for downcast of unsigned integer
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.
No tags attached.
Issue History
2012-02-07 11:05sylvain nahasNew Issue
2012-02-07 11:05sylvain nahasStatusnew => assigned
2012-02-07 11:05sylvain nahasAssigned To => pherrmann
2012-02-07 11:08sylvain nahasNote Added: 0002667
2012-02-07 11:31sylvain nahasNote Added: 0002668
2012-02-07 11:41sylvain nahasNote Edited: 0002668
2012-02-07 13:35pherrmannNote Added: 0002671
2012-02-07 13:59sylvain nahasNote Added: 0002672
2012-02-07 14:10pherrmannNote Added: 0002673
2012-02-08 14:05signolesStatusassigned => resolved
2012-02-08 14:05signolesResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

sylvain nahas   
2012-02-07 11:08   
I have already had a look in the relevant code, and believe I could propose a patch against Nitrogen for review and possibly integration quite soon.
sylvain nahas   
2012-02-07 11:31   
(edited on: 2012-02-07 11:41)
BTW, UTF8 characters less-than, "<=", and "or", are displayed as ?.
2012-02-07 13:35   
The feature has already been added in the svn trunk version of Frama-C (see input below), although the documentation has not been updated yet. It is indeed a feature, since unsigned downcast are a perfectly defined behavior (while signed downcast are implementation defined, but are not undefined behavior either) Example for current trunk version (since svn 16483) : frama-c -rte -rte-unsigned-downcast /tmp/main.c -print [kernel] preprocessing with "gcc -C -E -I. /tmp/e.c" [rte] annotating function main /* Generated by Frama-C */ unsigned char main(unsigned char a, unsigned char b) { unsigned char __retres; /*@ assert rte: (int)a+(int)b ? 255 ? (int)a+(int)b ? 0; */ /*@ assert rte: (int)a+(int)b ? 2147483647 ? (int)a+(int)b ? (-0x7FFFFFFF-1); */ __retres = (unsigned char)((int)a + (int)b); return (__retres); }
sylvain nahas   
2012-02-07 13:59   
Great! Now I can not wait for the publication of the next public distribution, since I have not access to svn trunk :-)
2012-02-07 14:10   
The feature will indeed be present in the next public distribution.