Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001083Frama-CPlug-in > RTEpublic2012-02-07 11:052012-09-19 17:16
Reportersylvain nahas 
Assigned Topherrmann 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001083: RTE does not check for downcast of unsigned integer
DescriptionFrama-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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002667)
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.
(0002668)
sylvain nahas (reporter)
2012-02-07 11:31
edited on: 2012-02-07 11:41

BTW, UTF8 characters less-than, "<=", and "or", are displayed as ?.

(0002671)
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);
}
(0002672)
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 :-)
(0002673)
pherrmann (reporter)
2012-02-07 14:10

The feature will indeed be present in the next public distribution.

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker