float_to_int.res.oracle

[kernel] Parsing tests/rte/float_to_int.c (with preprocessing)
[kernel:parser:decimal-float] tests/rte/float_to_int.c:13: Warning: 
  Floating-point constant 1.5e255 is not represented exactly. Will use 0x1.99309cc247f15p847.
  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[rte] annotating function main
[rte] tests/rte/float_to_int.c:14: Warning: 
  guaranteed RTE: assert float_to_int: 258. < 128;
[rte] tests/rte/float_to_int.c:16: Warning: 
  guaranteed RTE: assert float_to_int: -2147483649 < -2147483649.5;
/* Generated by Frama-C */
void main(void)
{
  float f = (float)0.;
  /*@ assert rte: float_to_int: f < 2147483648; */
  /*@ assert rte: float_to_int: -2147483649 < f; */
  int i = (int)f;
  /*@ assert rte: float_to_int: f < 9223372036854775808; */
  /*@ assert rte: float_to_int: -9223372036854775809 < f; */
  long long l = (long long)f;
  /*@ assert rte: float_to_int: f < 65536; */
  /*@ assert rte: float_to_int: -1 < f; */
  unsigned short s = (unsigned short)f;
  int ci1 = (int)1.5;
  /*@ assert rte: float_to_int: 1.5e255 < 2147483648; */
  int ci2 = (int)1.5e255;
  /*@ assert rte: float_to_int: 258. < 128; */
  char ci3 = (char)258.;
  int ci4 = (int)2147483647.5;
  /*@ assert rte: float_to_int: -2147483649 < -2147483649.5; */
  int ci5 = (int)(- 2147483649.5);
  return;
}