shift.0.res.oracle

[kernel] Parsing shift.c (with preprocessing)
[rte:annot] annotating function main
[rte] shift.c:13: Warning: 
  guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift.c:14: Warning: 
  guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift.c:16: Warning: guaranteed RTE: assert shift: 0 ≤ (int)(-3);
[rte] shift.c:18: Warning: 
  guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift.c:19: Warning: 
  guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift.c:20: Warning: guaranteed RTE: assert shift: 0 ≤ 60 < 32;
[rte] shift.c:20: Warning: 
  guaranteed RTE: assert signed_overflow: 5 << 60 ≤ 2147483647;
[rte] shift.c:22: Warning: 
  guaranteed RTE: assert signed_overflow: 5 << 29 ≤ 2147483647;
[rte] shift.c:36: Warning: guaranteed RTE: assert shift: 0 ≤ (int)(-2) < 32;
[rte] shift.c:38: Warning: guaranteed RTE: assert shift: 0 ≤ 32 < 32;
/* Generated by Frama-C */
int main(void)
{
  int __retres;
  int i = 0;
  int x = 0;
  int y = 0;
  int z = 0;
  unsigned int ux = (unsigned int)0;
  unsigned int uy = (unsigned int)0;
  unsigned int uz = (unsigned int)0;
  long lx = (long)0;
  long ly = (long)0;
  long lz = (long)0;
  z = (int)(5u << 30);
  /*@ assert rte: signed_overflow: 5 << 30 ≤ 2147483647; */
  uz = (unsigned int)(5 << 30);
  /*@ assert rte: signed_overflow: 5 << 30 ≤ 2147483647; */
  z = 5 << 30;
  /*@ assert rte: shift: 0 ≤ (int)(-3); */
  z = -3 << 2;
  /*@ assert rte: signed_overflow: 5 << 30 ≤ 2147483647; */
  z = 5 << 30;
  /*@ assert rte: signed_overflow: 5 << 30 ≤ 2147483647; */
  lz = (long)(5 << 30);
  /*@ assert rte: shift: 0 ≤ 60 < 32; */
  /*@ assert rte: signed_overflow: 5 << 60 ≤ 2147483647; */
  lz = (long)(5 << 60);
  /*@ assert rte: signed_overflow: 5 << 29 ≤ 2147483647; */
  z = 5 << 29;
  z = 5 << 28;
  z = 5 << 3;
  z = 5 << 1;
  i = 0;
  while (i < 10) {
    /*@ assert rte: shift: 0 ≤ i < 32; */
    /*@ assert rte: signed_overflow: 1 << i ≤ 2147483647; */
    z = 1 << i;
    /*@ assert rte: shift: 0 ≤ i; */
    /*@ assert rte: signed_overflow: i << 1 ≤ 2147483647; */
    z = i << 1;
    /*@ assert rte: shift: 0 ≤ i < 32; */
    /*@ assert rte: shift: 0 ≤ i; */
    /*@ assert rte: signed_overflow: i << i ≤ 2147483647; */
    z = i << i;
    /*@ assert rte: signed_overflow: i + 1 ≤ 2147483647; */
    i ++;
  }
  /*@ assert rte: shift: 0 ≤ (int)(-2) < 32; */
  z = 3 >> -2;
  z = 3 >> 5;
  /*@ assert rte: shift: 0 ≤ 32 < 32; */
  z = 3 >> 32;
  z = 3 >> 31;
  z = -5 >> 1;
  /*@ assert rte: shift: 0 ≤ y < 32; */
  z = x >> y;
  /*@ assert rte: shift: 0 ≤ y < 32; */
  uz = (unsigned int)x >> y;
  z = -2 >> 1;
  uz = (unsigned int)(-2) >> 1;
  z = 0 << 10;
  z = 0 >> 10;
  __retres = 0;
  return __retres;
}