addsub.res.oracle

[kernel] Parsing tests/rte/addsub.c (with preprocessing)
[rte] annotating function main
[rte] tests/rte/addsub.c:9: Warning: 
  guaranteed RTE:
  assert signed_overflow: 0x7fffffff + 0x7fffffff ≤ 2147483647;
[rte] tests/rte/addsub.c:10: Warning: 
  guaranteed RTE:
  assert signed_overflow: -2147483648 ≤ (int)(-0x7fffffff) - 0x7fffffff;
[rte] tests/rte/addsub.c:11: Warning: 
  guaranteed RTE:
  assert signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1;
[rte] tests/rte/addsub.c:11: Warning: 
  guaranteed RTE:
  assert
  signed_overflow: -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
/* Generated by Frama-C */
int main(void)
{
  int __retres;
  int x = 0;
  int y = 0;
  int z = 0;
  /*@ assert rte: signed_overflow: 0x7fffffff + 0x7fffffff ≤ 2147483647; */
  z = 0x7fffffff + 0x7fffffff;
  /*@ assert
      rte: signed_overflow: -2147483648 ≤ (int)(-0x7fffffff) - 0x7fffffff;
  */
  z = -0x7fffffff - 0x7fffffff;
  /*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */
  /*@ assert
      rte: signed_overflow:
        -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
  */
  z = - (-0x7fffffff - 1) - 1;
  z = 0x7fffffff + 0;
  z = -0x7fffffff - 1;
  /*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
  /*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
  z = x + y;
  /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-0x7ffffffc) - y; */
  z = -0x7ffffffc - y;
  /*@ assert rte: signed_overflow: -2147483647 ≤ x; */
  /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-x) - 0x7ffffffc; */
  z = - x - 0x7ffffffc;
  /*@ assert rte: signed_overflow: 0x7ffffffc + y ≤ 2147483647; */
  z = 0x7ffffffc + y;
  /*@ assert rte: signed_overflow: x + 0x7ffffffc ≤ 2147483647; */
  z = x + 0x7ffffffc;
  /*@ assert rte: signed_overflow: -2147483648 ≤ y + (int)(-2); */
  z = y + -2;
  /*@ assert rte: signed_overflow: y - (int)(-2) ≤ 2147483647; */
  z = y - -2;
  z = -1 - y;
  /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-2) - y; */
  z = -2 - y;
  /*@ assert rte: signed_overflow: 0 - y ≤ 2147483647; */
  z = 0 - y;
  __retres = 0;
  return __retres;
}