gen_offset.c

/* Generated by Frama-C */
int A[4] = {1, 2, 3, 4};
int *PA;
void __e_acsl_globals_init(void)
{
  __e_acsl_store_block((void *)(& PA),8UL);
  __e_acsl_full_init((void *)(& PA));
  __e_acsl_store_block((void *)(A),16UL);
  __e_acsl_full_init((void *)(& A));
  return;
}

int main(void)
{
  int __retres;
  int a[4];
  long l;
  char *pl;
  int *pi;
  char *p;
  long *q;
  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
  __e_acsl_globals_init();
  __e_acsl_store_block((void *)(& q),8UL);
  __e_acsl_store_block((void *)(& p),8UL);
  __e_acsl_store_block((void *)(& pi),8UL);
  __e_acsl_store_block((void *)(& pl),8UL);
  __e_acsl_store_block((void *)(& l),8UL);
  __e_acsl_store_block((void *)(a),16UL);
  PA = (int *)(& A);
  /*@ assert \offset((int *)A) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset;
      __gen_e_acsl_offset = __e_acsl_offset((void *)(A));
      __e_acsl_assert(__gen_e_acsl_offset == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset((int *)A) == 0",13);
    }
  }
  /*@ assert \offset(&A[3]) ≡ 12; */
  {
    {
      int __gen_e_acsl_offset_2;
      __gen_e_acsl_offset_2 = __e_acsl_offset((void *)(& A[3]));
      __e_acsl_assert(__gen_e_acsl_offset_2 == 12UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(&A[3]) == 12",14);
    }
  }
  /*@ assert \offset(PA) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_3;
      __gen_e_acsl_offset_3 = __e_acsl_offset((void *)PA);
      __e_acsl_assert(__gen_e_acsl_offset_3 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(PA) == 0",15);
    }
  }
  PA ++;
  /*@ assert \offset(PA + 1) ≡ 8; */
  {
    {
      int __gen_e_acsl_offset_4;
      __gen_e_acsl_offset_4 = __e_acsl_offset((void *)(PA + 1));
      __e_acsl_assert(__gen_e_acsl_offset_4 == 8UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(PA + 1) == 8",17);
    }
  }
  __e_acsl_initialize((void *)(a),sizeof(int));
  a[0] = 1;
  __e_acsl_initialize((void *)(& a[1]),sizeof(int));
  a[1] = 2;
  __e_acsl_initialize((void *)(& a[2]),sizeof(int));
  a[2] = 3;
  __e_acsl_initialize((void *)(& a[3]),sizeof(int));
  a[3] = 4;
  /*@ assert \offset((int *)a) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_5;
      __gen_e_acsl_offset_5 = __e_acsl_offset((void *)(a));
      __e_acsl_assert(__gen_e_acsl_offset_5 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset((int *)a) == 0",21);
    }
  }
  /*@ assert \offset(&a[1]) ≡ 4; */
  {
    {
      int __gen_e_acsl_offset_6;
      __gen_e_acsl_offset_6 = __e_acsl_offset((void *)(& a[1]));
      __e_acsl_assert(__gen_e_acsl_offset_6 == 4UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(&a[1]) == 4",22);
    }
  }
  /*@ assert \offset(&a[3]) ≡ 12; */
  {
    {
      int __gen_e_acsl_offset_7;
      __gen_e_acsl_offset_7 = __e_acsl_offset((void *)(& a[3]));
      __e_acsl_assert(__gen_e_acsl_offset_7 == 12UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(&a[3]) == 12",23);
    }
  }
  __e_acsl_full_init((void *)(& l));
  l = (long)4;
  __e_acsl_full_init((void *)(& pl));
  pl = (char *)(& l);
  /*@ assert \offset(&l) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_8;
      __gen_e_acsl_offset_8 = __e_acsl_offset((void *)(& l));
      __e_acsl_assert(__gen_e_acsl_offset_8 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(&l) == 0",28);
    }
  }
  /*@ assert \offset(pl) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_9;
      __gen_e_acsl_offset_9 = __e_acsl_offset((void *)pl);
      __e_acsl_assert(__gen_e_acsl_offset_9 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(pl) == 0",29);
    }
  }
  /*@ assert \offset(pl + 1) ≡ 1; */
  {
    {
      int __gen_e_acsl_offset_10;
      __gen_e_acsl_offset_10 = __e_acsl_offset((void *)(pl + 1));
      __e_acsl_assert(__gen_e_acsl_offset_10 == 1UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(pl + 1) == 1",30);
    }
  }
  /*@ assert \offset(pl + 7) ≡ 7; */
  {
    {
      int __gen_e_acsl_offset_11;
      __gen_e_acsl_offset_11 = __e_acsl_offset((void *)(pl + 7));
      __e_acsl_assert(__gen_e_acsl_offset_11 == 7UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(pl + 7) == 7",31);
    }
  }
  __e_acsl_full_init((void *)(& pi));
  pi = (int *)(& l);
  /*@ assert \offset(pi) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_12;
      __gen_e_acsl_offset_12 = __e_acsl_offset((void *)pi);
      __e_acsl_assert(__gen_e_acsl_offset_12 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(pi) == 0",33);
    }
  }
  __e_acsl_full_init((void *)(& pi));
  pi ++;
  /*@ assert \offset(pi) ≡ 4; */
  {
    {
      int __gen_e_acsl_offset_13;
      __gen_e_acsl_offset_13 = __e_acsl_offset((void *)pi);
      __e_acsl_assert(__gen_e_acsl_offset_13 == 4UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(pi) == 4",35);
    }
  }
  __e_acsl_full_init((void *)(& p));
  p = (char *)malloc((unsigned long)12);
  /*@ assert \offset(p) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_14;
      __gen_e_acsl_offset_14 = __e_acsl_offset((void *)p);
      __e_acsl_assert(__gen_e_acsl_offset_14 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(p) == 0",39);
    }
  }
  /*@ assert \offset(p + 1) ≡ 1; */
  {
    {
      int __gen_e_acsl_offset_15;
      __gen_e_acsl_offset_15 = __e_acsl_offset((void *)(p + 1));
      __e_acsl_assert(__gen_e_acsl_offset_15 == 1UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(p + 1) == 1",40);
    }
  }
  /*@ assert \offset(p + 11) ≡ 11; */
  {
    {
      int __gen_e_acsl_offset_16;
      __gen_e_acsl_offset_16 = __e_acsl_offset((void *)(p + 11));
      __e_acsl_assert(__gen_e_acsl_offset_16 == 11UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(p + 11) == 11",41);
    }
  }
  __e_acsl_full_init((void *)(& p));
  p += 5;
  /*@ assert \offset(p + 5) ≡ 10; */
  {
    {
      int __gen_e_acsl_offset_17;
      __gen_e_acsl_offset_17 = __e_acsl_offset((void *)(p + 5));
      __e_acsl_assert(__gen_e_acsl_offset_17 == 10UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(p + 5) == 10",43);
    }
  }
  /*@ assert \offset(p - 5) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_18;
      __gen_e_acsl_offset_18 = __e_acsl_offset((void *)(p - 5));
      __e_acsl_assert(__gen_e_acsl_offset_18 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(p - 5) == 0",44);
    }
  }
  __e_acsl_full_init((void *)(& q));
  q = (long *)malloc((unsigned long)30 * sizeof(long));
  /*@ assert \offset(q) ≡ 0; */
  {
    {
      int __gen_e_acsl_offset_19;
      __gen_e_acsl_offset_19 = __e_acsl_offset((void *)q);
      __e_acsl_assert(__gen_e_acsl_offset_19 == 0UL,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(q) == 0",49);
    }
  }
  __e_acsl_full_init((void *)(& q));
  q ++;
  /*@ assert \offset(q) ≡ sizeof(long); */
  {
    {
      int __gen_e_acsl_offset_20;
      __gen_e_acsl_offset_20 = __e_acsl_offset((void *)q);
      __e_acsl_assert(__gen_e_acsl_offset_20 == 8,(char *)"Assertion",
                      (char *)"main",(char *)"\\offset(q) == sizeof(long)",
                      51);
    }
  }
  __e_acsl_full_init((void *)(& q));
  q += 2;
  /*@ assert \offset(q) ≡ sizeof(long) * 3; */
  {
    {
      int __gen_e_acsl_offset_21;
      __gen_e_acsl_offset_21 = __e_acsl_offset((void *)q);
      __e_acsl_assert(__gen_e_acsl_offset_21 == 8 * 3,(char *)"Assertion",
                      (char *)"main",
                      (char *)"\\offset(q) == sizeof(long) * 3",53);
    }
  }
  __e_acsl_full_init((void *)(& q));
  q += 4;
  /*@ assert \offset(q) ≡ sizeof(long) * 7; */
  {
    {
      int __gen_e_acsl_offset_22;
      __gen_e_acsl_offset_22 = __e_acsl_offset((void *)q);
      __e_acsl_assert(__gen_e_acsl_offset_22 == 8 * 7,(char *)"Assertion",
                      (char *)"main",
                      (char *)"\\offset(q) == sizeof(long) * 7",55);
    }
  }
  __retres = 0;
  __e_acsl_delete_block((void *)(& PA));
  __e_acsl_delete_block((void *)(A));
  __e_acsl_delete_block((void *)(& q));
  __e_acsl_delete_block((void *)(& p));
  __e_acsl_delete_block((void *)(& pi));
  __e_acsl_delete_block((void *)(& pl));
  __e_acsl_delete_block((void *)(& l));
  __e_acsl_delete_block((void *)(a));
  __e_acsl_memory_clean();
  return __retres;
}