2021-01-15 19:18 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001083Frama-CPlug-in > RTEpublic2012-09-19 17:16
Reportersylvain nahas 
Assigned Topherrmann 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0002667

sylvain nahas (reporter)

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)

Last edited: 2012-02-07 11:41

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

~0002671

pherrmann (reporter)

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)

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)

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