array_index.0.res.oracle

[kernel] Parsing array_index.c (with preprocessing)
[rte:annot] annotating function main
/* Generated by Frama-C */
struct s_arr {
   int t[15] ;
};
struct __anonstruct_s_1 {
   int u[12] ;
};
struct _s {
   int t[15] ;
   struct __anonstruct_s_1 s ;
   struct s_arr v[12] ;
};
typedef struct _s ts;
int t[10];
int u[8 + 3];
int v[16][17];
ts s;
unsigned int c[10];
void main(int i, int j, unsigned int k)
{
  int x;
  int t_0[(unsigned int)100 / sizeof(x)];
  t[0] = 0;
  u[1] = 0;
  v[2][3] = 0;
  s.t[1] = 0;
  s.s.u[2] = 0;
  s.v[3].t[4] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 10; */
  t[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < (int)(8 + 3); */
  u[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 16; */
  /*@ assert rte: index_bound: 0 ≤ j; */
  /*@ assert rte: index_bound: j < 17; */
  v[i][j] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 15; */
  s.t[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 12; */
  s.s.u[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 12; */
  /*@ assert rte: index_bound: 0 ≤ j; */
  /*@ assert rte: index_bound: j < 15; */
  s.v[i].t[j] = 0;
  /*@ assert rte: index_bound: k < 10; */
  t[k] = 0;
  /*@ assert rte: index_bound: k < (int)(8 + 3); */
  u[k] = 0;
  /*@ assert rte: index_bound: k < 16; */
  /*@ assert rte: index_bound: c[k] < 17; */
  /*@ assert rte: index_bound: k < 10; */
  v[k][c[k]] = 0;
  /*@ assert rte: index_bound: k < 15; */
  s.t[k] = 0;
  /*@ assert rte: index_bound: k < 12; */
  s.s.u[k] = 0;
  /*@ assert rte: index_bound: k < 12; */
  /*@ assert rte: index_bound: c[k] < 15; */
  /*@ assert rte: index_bound: k < 10; */
  s.v[k].t[c[k]] = 0;
  return;
}


[rte:annot] annotating function main
/* Generated by Frama-C */
struct s_arr {
   int t[15] ;
};
struct __anonstruct_s_1 {
   int u[12] ;
};
struct _s {
   int t[15] ;
   struct __anonstruct_s_1 s ;
   struct s_arr v[12] ;
};
typedef struct _s ts;
int t[10];
int u[8 + 3];
int v[16][17];
ts s;
unsigned int c[10];
void main(int i, int j, unsigned int k)
{
  int x;
  int t_0[(unsigned int)100 / sizeof(x)];
  /*@ assert rte: index_bound: 0 ≤ 0; */
  /*@ assert rte: index_bound: 0 < 10; */
  t[0] = 0;
  /*@ assert rte: index_bound: 0 ≤ 1; */
  /*@ assert rte: index_bound: 1 < (int)(8 + 3); */
  u[1] = 0;
  /*@ assert rte: index_bound: 0 ≤ 2; */
  /*@ assert rte: index_bound: 2 < 16; */
  /*@ assert rte: index_bound: 0 ≤ 3; */
  /*@ assert rte: index_bound: 3 < 17; */
  v[2][3] = 0;
  /*@ assert rte: index_bound: 0 ≤ 1; */
  /*@ assert rte: index_bound: 1 < 15; */
  s.t[1] = 0;
  /*@ assert rte: index_bound: 0 ≤ 2; */
  /*@ assert rte: index_bound: 2 < 12; */
  s.s.u[2] = 0;
  /*@ assert rte: index_bound: 0 ≤ 3; */
  /*@ assert rte: index_bound: 3 < 12; */
  /*@ assert rte: index_bound: 0 ≤ 4; */
  /*@ assert rte: index_bound: 4 < 15; */
  s.v[3].t[4] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 10; */
  t[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < (int)(8 + 3); */
  u[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 16; */
  /*@ assert rte: index_bound: 0 ≤ j; */
  /*@ assert rte: index_bound: j < 17; */
  v[i][j] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 15; */
  s.t[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 12; */
  s.s.u[i] = 0;
  /*@ assert rte: index_bound: 0 ≤ i; */
  /*@ assert rte: index_bound: i < 12; */
  /*@ assert rte: index_bound: 0 ≤ j; */
  /*@ assert rte: index_bound: j < 15; */
  s.v[i].t[j] = 0;
  /*@ assert rte: index_bound: k < 10; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  t[k] = 0;
  /*@ assert rte: index_bound: k < (int)(8 + 3); */
  /*@ assert rte: index_bound: 0 ≤ k; */
  u[k] = 0;
  /*@ assert rte: index_bound: k < 16; */
  /*@ assert rte: index_bound: c[k] < 17; */
  /*@ assert rte: index_bound: k < 10; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  /*@ assert rte: index_bound: 0 ≤ c[k]; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  v[k][c[k]] = 0;
  /*@ assert rte: index_bound: k < 15; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  s.t[k] = 0;
  /*@ assert rte: index_bound: k < 12; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  s.s.u[k] = 0;
  /*@ assert rte: index_bound: k < 12; */
  /*@ assert rte: index_bound: c[k] < 15; */
  /*@ assert rte: index_bound: k < 10; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  /*@ assert rte: index_bound: 0 ≤ c[k]; */
  /*@ assert rte: index_bound: 0 ≤ k; */
  s.v[k].t[c[k]] = 0;
  return;
}