initialized.res.oracle

[kernel] Parsing initialized.c (with preprocessing)
[kernel:parser:decimal-float] initialized.c:111: Warning: 
  Floating-point constant 1.1234 is not represented exactly. Will use 0x1.1f972474538efp0.
  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[rte:annot] annotating function f
[rte:annot] annotating function g
[rte:annot] annotating function main
/* Generated by Frama-C */
struct R {
   int v ;
};
struct P;
struct Q {
   int v ;
   int id[12] ;
   struct P *next ;
   struct R tr[13] ;
};
struct P {
   int val ;
   struct P *next ;
   int id[5] ;
   int oth[6][7] ;
   struct P *nexts[8][9] ;
   struct Q q ;
   struct Q tq[10][11] ;
   struct P ***znexts ;
};
int g(void)
{
  int x = 3;
  /*@ assert rte: initialization: \initialized(&x); */
  return x;
}

int f(struct P ***pppp_0, struct P **ppp_0, struct P *pp_0, struct P p_0,
      struct P p2_0, int v_0, struct Q q_0, int *i_0, int *j_0, int i0_0,
      int i1_0, int i2_0, int i3_0, int i4_0, double f_0)
{
  int tmp;
  struct P *tmp_0;
  i0_0 = 0;
  i1_0 = 1;
  i2_0 = 2;
  i3_0 = 3;
  i4_0 = 4;
  tmp = g();
  j_0 = (int *)(0 + tmp);
  i_0 = (int *)(& j_0);
  pp_0 = & p_0;
  ppp_0 = & pp_0;
  pppp_0 = & ppp_0;
  p_0.next = pp_0;
  p_0.znexts = pppp_0;
  tmp_0 = pp_0;
  /*@ assert rte: index_bound: 0 ≤ i2_0; */
  /*@ assert rte: index_bound: i2_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i3_0; */
  /*@ assert rte: index_bound: i3_0 < 9; */
  p_0.nexts[i2_0][i3_0] = tmp_0;
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 9; */
  p_0.nexts[i0_0][i1_0] = tmp_0;
  q_0.next = pp_0;
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 12; */
  q_0.id[i0_0] = 0;
  p_0.q = q_0;
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 11; */
  p_0.tq[i0_0][i1_0] = q_0;
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 5; */
  /*@ assert rte: index_bound: 0 ≤ i2_0; */
  /*@ assert rte: index_bound: i2_0 < 5; */
  /*@ assert rte: initialization: \initialized(&p_0.id[i2_0]); */
  p_0.id[i1_0] = p_0.id[i2_0];
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 5; */
  /*@ assert rte: index_bound: 0 ≤ i3_0; */
  /*@ assert rte: index_bound: i3_0 < 5; */
  /*@ assert rte: initialization: \initialized(&p_0.id[i3_0]); */
  p_0.id[i1_0] = p_0.id[i3_0];
  /*@ assert rte: initialization: \initialized(&p_0.next); */
  /*@ assert rte: mem_access: \valid_read(p_0.next); */
  struct P np = *(p_0.next);
  /*@ assert rte: initialization: \initialized(&p_0.next); */
  struct P *npp = p_0.next;
  /*@ assert rte: initialization: \initialized(&npp); */
  p_0.next = npp;
  /*@ assert rte: initialization: \initialized(&p_0.id[3]); */
  v_0 = p_0.id[3];
  /*@ assert rte: mem_access: \valid_read(&pp_0->id[3]); */
  /*@ assert rte: initialization: \initialized(&pp_0->id[3]); */
  v_0 = pp_0->id[3];
  /*@ assert rte: mem_access: \valid_read(i_0); */
  /*@ assert rte: initialization: \initialized(i_0); */
  v_0 = *i_0;
  /*@ assert rte: mem_access: \valid_read(&pp_0->val); */
  /*@ assert rte: initialization: \initialized(&pp_0->val); */
  v_0 = pp_0->val;
  /*@ assert rte: mem_access: \valid_read(&pp_0->id[3]); */
  /*@ assert rte: initialization: \initialized(&pp_0->id[3]); */
  v_0 = pp_0->id[3];
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 9; */
  /*@ assert rte: mem_access: \valid_read(&pp_0->nexts[i0_0][i1_0]); */
  /*@ assert rte: initialization: \initialized(&pp_0->nexts[i0_0][i1_0]); */
  struct P *z = pp_0->nexts[i0_0][i1_0];
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 9; */
  /*@ assert rte: mem_access: \valid_read(&pp_0->nexts[i0_0][i1_0]); */
  /*@ assert rte: initialization: \initialized(&pp_0->nexts[i0_0][i1_0]); */
  /*@ assert rte: mem_access: \valid_read(&(pp_0->nexts[i0_0][i1_0])->val);
  */
  /*@ assert
      rte: initialization: \initialized(&(pp_0->nexts[i0_0][i1_0])->val);
  */
  v_0 = (pp_0->nexts[i0_0][i1_0])->val;
  /*@ assert rte: mem_access: \valid_read(&pp_0->next); */
  /*@ assert rte: initialization: \initialized(&pp_0->next); */
  /*@ assert rte: mem_access: \valid_read(&(pp_0->next)->val); */
  /*@ assert rte: initialization: \initialized(&(pp_0->next)->val); */
  v_0 = (pp_0->next)->val;
  /*@ assert rte: mem_access: \valid_read(&pp_0->next); */
  /*@ assert rte: initialization: \initialized(&pp_0->next); */
  /*@ assert rte: mem_access: \valid_read(&(pp_0->next)->next); */
  /*@ assert rte: initialization: \initialized(&(pp_0->next)->next); */
  /*@ assert rte: mem_access: \valid_read(&((pp_0->next)->next)->val); */
  /*@ assert rte: initialization: \initialized(&((pp_0->next)->next)->val);
  */
  v_0 = ((pp_0->next)->next)->val;
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 9; */
  /*@ assert rte: initialization: \initialized(&p_0.nexts[i0_0][i1_0]); */
  /*@ assert rte: mem_access: \valid_read(&(p_0.nexts[i0_0][i1_0])->val); */
  /*@ assert
      rte: initialization: \initialized(&(p_0.nexts[i0_0][i1_0])->val);
  */
  v_0 = (p_0.nexts[i0_0][i1_0])->val;
  /*@ assert rte: index_bound: 0 ≤ i2_0; */
  /*@ assert rte: index_bound: i2_0 < 5; */
  /*@ assert rte: mem_access: \valid_read(&pp_0->id[i2_0]); */
  /*@ assert rte: initialization: \initialized(&pp_0->id[i2_0]); */
  v_0 = pp_0->id[i2_0];
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 6; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 7; */
  /*@ assert rte: mem_access: \valid_read(&pp_0->oth[i0_0][i1_0]); */
  /*@ assert rte: initialization: \initialized(&pp_0->oth[i0_0][i1_0]); */
  v_0 = pp_0->oth[i0_0][i1_0];
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i2_0; */
  /*@ assert rte: index_bound: i2_0 < 9; */
  /*@ assert rte: initialization: \initialized(&p_0.nexts[i1_0][i2_0]); */
  /*@ assert rte: mem_access: \valid_read(i_0); */
  /*@ assert rte: initialization: \initialized(i_0); */
  /*@ assert rte: index_bound: 0 ≤ i3_0; */
  /*@ assert rte: index_bound: i3_0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ *i_0; */
  /*@ assert rte: index_bound: *i_0 < 9; */
  /*@ assert
      rte: mem_access:
        \valid_read(&(p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0]);
  */
  /*@ assert
      rte: initialization:
        \initialized(&(p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0]);
  */
  /*@ assert rte: index_bound: 0 ≤ i4_0; */
  /*@ assert rte: index_bound: i4_0 < 5; */
  /*@ assert
      rte: mem_access:
        \valid_read(&((p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0])->id[i4_0]);
  */
  /*@ assert
      rte: initialization:
        \initialized(&((p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0])->id[i4_0]);
  */
  v_0 = ((p_0.nexts[i1_0][i2_0])->nexts[i3_0][*i_0])->id[i4_0];
  /*@ assert rte: initialization: \initialized(&p_0.q.v); */
  v_0 = p_0.q.v;
  /*@ assert rte: index_bound: 0 ≤ i4_0; */
  /*@ assert rte: index_bound: i4_0 < 12; */
  /*@ assert rte: initialization: \initialized(&p_0.q.id[i4_0]); */
  v_0 = p_0.q.id[i4_0];
  /*@ assert rte: index_bound: 0 ≤ i3_0; */
  /*@ assert rte: index_bound: i3_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 11; */
  /*@ assert rte: initialization: \initialized(&p_0.tq[i3_0][i1_0].v); */
  v_0 = p_0.tq[i3_0][i1_0].v;
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i2_0; */
  /*@ assert rte: index_bound: i2_0 < 11; */
  /*@ assert rte: initialization: \initialized(&p_0.tq[i1_0][i2_0].next); */
  /*@ assert rte: index_bound: 0 ≤ i3_0; */
  /*@ assert rte: index_bound: i3_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i4_0; */
  /*@ assert rte: index_bound: i4_0 < 11; */
  /*@ assert
      rte: mem_access:
        \valid_read(&(p_0.tq[i1_0][i2_0].next)->tq[i3_0][i4_0].v);
  */
  /*@ assert
      rte: initialization:
        \initialized(&(p_0.tq[i1_0][i2_0].next)->tq[i3_0][i4_0].v);
  */
  v_0 = (p_0.tq[i1_0][i2_0].next)->tq[i3_0][i4_0].v;
  /*@ assert rte: index_bound: 0 ≤ i3_0; */
  /*@ assert rte: index_bound: i3_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 11; */
  /*@ assert rte: mem_access: \valid_read(&pp_0->tq[i3_0][i1_0].v); */
  /*@ assert rte: initialization: \initialized(&pp_0->tq[i3_0][i1_0].v); */
  v_0 = pp_0->tq[i3_0][i1_0].v;
  /*@ assert rte: initialization: \initialized(&p_0.znexts); */
  /*@ assert rte: mem_access: \valid_read(p_0.znexts + i0_0); */
  /*@ assert rte: initialization: \initialized(p_0.znexts + i0_0); */
  /*@ assert rte: mem_access: \valid_read(*(p_0.znexts + i0_0) + i1_0); */
  /*@ assert rte: initialization: \initialized(*(p_0.znexts + i0_0) + i1_0);
  */
  /*@ assert
      rte: mem_access:
        \valid_read(&(*(*(p_0.znexts + i0_0) + i1_0) + i2_0)->val);
  */
  /*@ assert
      rte: initialization:
        \initialized(&(*(*(p_0.znexts + i0_0) + i1_0) + i2_0)->val);
  */
  v_0 = (*(*(p_0.znexts + i0_0) + i1_0) + i2_0)->val;
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 11; */
  q_0 = p_0.tq[i0_0][i1_0];
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 11; */
  /*@ assert rte: index_bound: 0 ≤ i2_0; */
  /*@ assert rte: index_bound: i2_0 < 13; */
  /*@ assert
      rte: initialization: \initialized(&p_0.tq[i0_0][i1_0].tr[i2_0].v);
  */
  v_0 = p_0.tq[i0_0][i1_0].tr[i2_0].v;
  /*@ assert rte: mem_access: \valid_read(&pp_0->val); */
  /*@ assert rte: initialization: \initialized(&pp_0->val); */
  v_0 = pp_0->val;
  /*@ assert rte: initialization: \initialized(&p_0.val); */
  v_0 = p_0.val;
  /*@ assert rte: index_bound: 0 ≤ i0_0; */
  /*@ assert rte: index_bound: i0_0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1_0; */
  /*@ assert rte: index_bound: i1_0 < 11; */
  /*@ assert rte: initialization: \initialized(&p_0.tq[i0_0][i1_0].v); */
  v_0 = p_0.tq[i0_0][i1_0].v;
  return v_0;
}

struct P ***pppp;
struct P **ppp;
struct P *pp;
struct P p;
struct P p2;
int v;
struct Q q;
int *i;
int j;
int i0 = 0;
int i1 = 1;
int i2 = 2;
int i3 = 3;
int i4 = 4;
double f0 = 1.1234;
int i5 = 1;
int main(void)
{
  unsigned char c1;
  unsigned char c2;
  struct P *tmp;
  j = 0;
  i = & j;
  pp = & p;
  ppp = & pp;
  pppp = & ppp;
  p.next = pp;
  p.znexts = pppp;
  tmp = pp;
  /*@ assert rte: index_bound: 0 ≤ i2; */
  /*@ assert rte: index_bound: i2 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i3; */
  /*@ assert rte: index_bound: i3 < 9; */
  p.nexts[i2][i3] = tmp;
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 9; */
  p.nexts[i0][i1] = tmp;
  q.next = pp;
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 12; */
  q.id[i0] = 0;
  p.q = q;
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 11; */
  p.tq[i0][i1] = q;
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 5; */
  /*@ assert rte: index_bound: 0 ≤ i2; */
  /*@ assert rte: index_bound: i2 < 5; */
  /*@ assert rte: initialization: \initialized(&p.id[i2]); */
  p.id[i1] = p.id[i2];
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 5; */
  /*@ assert rte: index_bound: 0 ≤ i3; */
  /*@ assert rte: index_bound: i3 < 5; */
  /*@ assert rte: initialization: \initialized(&p.id[i3]); */
  p.id[i1] = p.id[i3];
  /*@ assert rte: initialization: \initialized(&p.next); */
  /*@ assert rte: mem_access: \valid_read(p.next); */
  struct P np = *(p.next);
  /*@ assert rte: initialization: \initialized(&p.next); */
  struct P *npp = p.next;
  /*@ assert rte: initialization: \initialized(&p.id[3]); */
  v = p.id[3];
  /*@ assert rte: mem_access: \valid_read(&pp->id[3]); */
  /*@ assert rte: initialization: \initialized(&pp->id[3]); */
  v = pp->id[3];
  /*@ assert rte: mem_access: \valid_read(i); */
  /*@ assert rte: initialization: \initialized(i); */
  v = *i;
  /*@ assert rte: mem_access: \valid_read(&pp->val); */
  /*@ assert rte: initialization: \initialized(&pp->val); */
  v = pp->val;
  /*@ assert rte: mem_access: \valid_read(&pp->id[3]); */
  /*@ assert rte: initialization: \initialized(&pp->id[3]); */
  v = pp->id[3];
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 9; */
  /*@ assert rte: mem_access: \valid_read(&pp->nexts[i0][i1]); */
  /*@ assert rte: initialization: \initialized(&pp->nexts[i0][i1]); */
  struct P *z = pp->nexts[i0][i1];
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 9; */
  /*@ assert rte: mem_access: \valid_read(&pp->nexts[i0][i1]); */
  /*@ assert rte: initialization: \initialized(&pp->nexts[i0][i1]); */
  /*@ assert rte: mem_access: \valid_read(&(pp->nexts[i0][i1])->val); */
  /*@ assert rte: initialization: \initialized(&(pp->nexts[i0][i1])->val); */
  v = (pp->nexts[i0][i1])->val;
  /*@ assert rte: mem_access: \valid_read(&pp->next); */
  /*@ assert rte: initialization: \initialized(&pp->next); */
  /*@ assert rte: mem_access: \valid_read(&(pp->next)->val); */
  /*@ assert rte: initialization: \initialized(&(pp->next)->val); */
  v = (pp->next)->val;
  /*@ assert rte: mem_access: \valid_read(&pp->next); */
  /*@ assert rte: initialization: \initialized(&pp->next); */
  /*@ assert rte: mem_access: \valid_read(&(pp->next)->next); */
  /*@ assert rte: initialization: \initialized(&(pp->next)->next); */
  /*@ assert rte: mem_access: \valid_read(&((pp->next)->next)->val); */
  /*@ assert rte: initialization: \initialized(&((pp->next)->next)->val); */
  v = ((pp->next)->next)->val;
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 9; */
  /*@ assert rte: initialization: \initialized(&p.nexts[i0][i1]); */
  /*@ assert rte: mem_access: \valid_read(&(p.nexts[i0][i1])->val); */
  /*@ assert rte: initialization: \initialized(&(p.nexts[i0][i1])->val); */
  v = (p.nexts[i0][i1])->val;
  /*@ assert rte: index_bound: 0 ≤ i2; */
  /*@ assert rte: index_bound: i2 < 5; */
  /*@ assert rte: mem_access: \valid_read(&pp->id[i2]); */
  /*@ assert rte: initialization: \initialized(&pp->id[i2]); */
  v = pp->id[i2];
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 6; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 7; */
  /*@ assert rte: mem_access: \valid_read(&pp->oth[i0][i1]); */
  /*@ assert rte: initialization: \initialized(&pp->oth[i0][i1]); */
  v = pp->oth[i0][i1];
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 8; */
  /*@ assert rte: index_bound: 0 ≤ i2; */
  /*@ assert rte: index_bound: i2 < 9; */
  /*@ assert rte: initialization: \initialized(&p.nexts[i1][i2]); */
  /*@ assert rte: mem_access: \valid_read(i); */
  /*@ assert rte: initialization: \initialized(i); */
  /*@ assert rte: index_bound: 0 ≤ i3; */
  /*@ assert rte: index_bound: i3 < 8; */
  /*@ assert rte: index_bound: 0 ≤ *i; */
  /*@ assert rte: index_bound: *i < 9; */
  /*@ assert rte: mem_access: \valid_read(&(p.nexts[i1][i2])->nexts[i3][*i]);
  */
  /*@ assert
      rte: initialization: \initialized(&(p.nexts[i1][i2])->nexts[i3][*i]);
  */
  /*@ assert rte: index_bound: 0 ≤ i4; */
  /*@ assert rte: index_bound: i4 < 5; */
  /*@ assert
      rte: mem_access:
        \valid_read(&((p.nexts[i1][i2])->nexts[i3][*i])->id[i4]);
  */
  /*@ assert
      rte: initialization:
        \initialized(&((p.nexts[i1][i2])->nexts[i3][*i])->id[i4]);
  */
  v = ((p.nexts[i1][i2])->nexts[i3][*i])->id[i4];
  /*@ assert rte: initialization: \initialized(&p.q.v); */
  v = p.q.v;
  /*@ assert rte: index_bound: 0 ≤ i4; */
  /*@ assert rte: index_bound: i4 < 12; */
  /*@ assert rte: initialization: \initialized(&p.q.id[i4]); */
  v = p.q.id[i4];
  /*@ assert rte: index_bound: 0 ≤ i3; */
  /*@ assert rte: index_bound: i3 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 11; */
  /*@ assert rte: initialization: \initialized(&p.tq[i3][i1].v); */
  v = p.tq[i3][i1].v;
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i2; */
  /*@ assert rte: index_bound: i2 < 11; */
  /*@ assert rte: initialization: \initialized(&p.tq[i1][i2].next); */
  /*@ assert rte: index_bound: 0 ≤ i3; */
  /*@ assert rte: index_bound: i3 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i4; */
  /*@ assert rte: index_bound: i4 < 11; */
  /*@ assert
      rte: mem_access: \valid_read(&(p.tq[i1][i2].next)->tq[i3][i4].v);
  */
  /*@ assert
      rte: initialization: \initialized(&(p.tq[i1][i2].next)->tq[i3][i4].v);
  */
  v = (p.tq[i1][i2].next)->tq[i3][i4].v;
  /*@ assert rte: index_bound: 0 ≤ i3; */
  /*@ assert rte: index_bound: i3 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 11; */
  /*@ assert rte: mem_access: \valid_read(&pp->tq[i3][i1].v); */
  /*@ assert rte: initialization: \initialized(&pp->tq[i3][i1].v); */
  v = pp->tq[i3][i1].v;
  /*@ assert rte: initialization: \initialized(&p.znexts); */
  /*@ assert rte: mem_access: \valid_read(p.znexts + i0); */
  /*@ assert rte: initialization: \initialized(p.znexts + i0); */
  /*@ assert rte: mem_access: \valid_read(*(p.znexts + i0) + i1); */
  /*@ assert rte: initialization: \initialized(*(p.znexts + i0) + i1); */
  /*@ assert
      rte: mem_access: \valid_read(&(*(*(p.znexts + i0) + i1) + i2)->val);
  */
  /*@ assert
      rte: initialization:
        \initialized(&(*(*(p.znexts + i0) + i1) + i2)->val);
  */
  v = (*(*(p.znexts + i0) + i1) + i2)->val;
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 11; */
  q = p.tq[i0][i1];
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 11; */
  /*@ assert rte: index_bound: 0 ≤ i2; */
  /*@ assert rte: index_bound: i2 < 13; */
  /*@ assert rte: initialization: \initialized(&p.tq[i0][i1].tr[i2].v); */
  v = p.tq[i0][i1].tr[i2].v;
  /*@ assert rte: mem_access: \valid_read(&pp->val); */
  /*@ assert rte: initialization: \initialized(&pp->val); */
  v = pp->val;
  /*@ assert rte: initialization: \initialized(&p.val); */
  v = p.val;
  /*@ assert rte: index_bound: 0 ≤ i0; */
  /*@ assert rte: index_bound: i0 < 10; */
  /*@ assert rte: index_bound: 0 ≤ i1; */
  /*@ assert rte: index_bound: i1 < 11; */
  /*@ assert rte: initialization: \initialized(&p.tq[i0][i1].v); */
  v = p.tq[i0][i1].v;
  /*@ assert rte: initialization: \initialized(&c2); */
  c1 = c2;
  /*@ assert rte: initialization: \initialized(&c2); */
  unsigned char c3 = c2;
  return v;
}