| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001083 | Frama-C | Plug-in > RTE | public | 2012-02-07 11:05 | 2012-09-19 17:16 | ||||
| Reporter | sylvain nahas | ||||||||
| Assigned To | pherrmann | ||||||||
| Priority | normal | Severity | major | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001083: RTE does not check for downcast of unsigned integer | ||||||||
| 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
sylvain nahas (reporter) 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 (reporter) 2012-02-07 11:31 Last edited: 2012-02-07 11:41 |
BTW, UTF8 characters less-than, "<=", and "or", are displayed as ?. |
|
pherrmann (reporter) 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 (reporter) 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 :-) |
|
pherrmann (reporter) 2012-02-07 14:10 |
The feature will indeed be present in the next public distribution. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2012-02-07 11:05 | sylvain nahas | New Issue | |
| 2012-02-07 11:05 | sylvain nahas | Status | new => assigned |
| 2012-02-07 11:05 | sylvain nahas | Assigned To | => pherrmann |
| 2012-02-07 11:08 | sylvain nahas | Note Added: 0002667 | |
| 2012-02-07 11:31 | sylvain nahas | Note Added: 0002668 | |
| 2012-02-07 11:41 | sylvain nahas | Note Edited: 0002668 | |
| 2012-02-07 13:35 | pherrmann | Note Added: 0002671 | |
| 2012-02-07 13:59 | sylvain nahas | Note Added: 0002672 | |
| 2012-02-07 14:10 | pherrmann | Note Added: 0002673 | |
| 2012-02-08 14:05 | signoles | Status | assigned => resolved |
| 2012-02-08 14:05 | signoles | Resolution | open => fixed |
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| Issue History |