0001083: RTE does not check for downcast of unsigned integer

(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

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.

Relationships