gen_at2.c

/* Generated by Frama-C */
#include "stdlib.h"
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);

/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
  __e_acsl_mpz_t __gen_e_acsl_at_3;
  __e_acsl_mpz_t __gen_e_acsl_at_2;
  __e_acsl_mpz_t __gen_e_acsl_at;
  {
    __e_acsl_mpz_t __gen_e_acsl_A_4;
    __gmpz_init_set_si(__gen_e_acsl_A_4,(long)A);
    __gmpz_init_set(__gen_e_acsl_at,
                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_4));
    __gmpz_clear(__gen_e_acsl_A_4);
  }
  {
    __e_acsl_mpz_t __gen_e_acsl_A;
    __gmpz_init_set_si(__gen_e_acsl_A,(long)A);
    __gmpz_init_set(__gen_e_acsl_at,
                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
    __gmpz_clear(__gen_e_acsl_A);
  }
  A = 1;
  F:
    __gmpz_init_set(__gen_e_acsl_at_3,
                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
    {
      __e_acsl_mpz_t __gen_e_acsl_A_2;
      __gmpz_init_set_si(__gen_e_acsl_A_2,(long)A);
      __gmpz_init_set(__gen_e_acsl_at_2,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_A_2));
      __gmpz_clear(__gen_e_acsl_A_2);
    }
    A = 2;
  /*@ assert \at(A,Pre) ≡ 0; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl_;
      int __gen_e_acsl_eq;
      __gmpz_init_set_si(__gen_e_acsl_,0L);
      __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
      __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"f",
                      (char *)"\\at(A,Pre) == 0",11);
      __gmpz_clear(__gen_e_acsl_);
    }
  }
  /*@ assert \at(A,F) ≡ 1; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl__2;
      int __gen_e_acsl_eq_2;
      __gmpz_init_set_si(__gen_e_acsl__2,1L);
      __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
      __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"f",
                      (char *)"\\at(A,F) == 1",12);
      __gmpz_clear(__gen_e_acsl__2);
    }
  }
  /*@ assert \at(A,Here) ≡ 2; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl_A_3;
      __e_acsl_mpz_t __gen_e_acsl__3;
      int __gen_e_acsl_eq_3;
      __gmpz_init_set_si(__gen_e_acsl_A_3,(long)A);
      __gmpz_init_set_si(__gen_e_acsl__3,2L);
      __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_A_3),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
      __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",(char *)"f",
                      (char *)"\\at(A,Here) == 2",13);
      __gmpz_clear(__gen_e_acsl_A_3);
      __gmpz_clear(__gen_e_acsl__3);
    }
  }
  /*@ assert \at(\at(A,Pre),F) ≡ 0; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl__4;
      int __gen_e_acsl_eq_4;
      __gmpz_init_set_si(__gen_e_acsl__4,0L);
      __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_3),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
      __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",(char *)"f",
                      (char *)"\\at(\\at(A,Pre),F) == 0",14);
      __gmpz_clear(__gen_e_acsl__4);
    }
  }
  A = 3;
  __gmpz_clear(__gen_e_acsl_at);
  __gmpz_clear(__gen_e_acsl_at_2);
  __gmpz_clear(__gen_e_acsl_at_3);
  return;
}

void g(int *p, int *q)
{
  int __gen_e_acsl_at_3;
  __e_acsl_mpz_t __gen_e_acsl_at_2;
  int __gen_e_acsl_at;
  __e_acsl_store_block((void *)(& p),(size_t)8);
  __e_acsl_store_block((void *)(& q),(size_t)8);
  __e_acsl_initialize((void *)p,sizeof(int));
  *p = 0;
  __e_acsl_initialize((void *)(p + 1),sizeof(int));
  *(p + 1) = 1;
  __e_acsl_initialize((void *)q,sizeof(int));
  *q = 0;
  L1:
    {
      int __gen_e_acsl_valid_read_3;
      __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)q,sizeof(int));
      __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"g",
                      (char *)"mem_access: \\valid_read(q)",28);
      __gen_e_acsl_at_3 = *q;
    }
    {
      int __gen_e_acsl_valid_read;
      __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)q,sizeof(int));
      __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"g",
                      (char *)"mem_access: \\valid_read(q)",26);
      __gen_e_acsl_at = *q;
    }
    __e_acsl_initialize((void *)p,sizeof(int));
  *p = 2;
  __e_acsl_initialize((void *)(p + 1),sizeof(int));
  *(p + 1) = 3;
  __e_acsl_initialize((void *)q,sizeof(int));
  *q = 1;
  L2:
    {
      int __gen_e_acsl_valid_read_2;
      __e_acsl_mpz_t __gen_e_acsl_;
      __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + __gen_e_acsl_at),
                                                      sizeof(int));
      __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"g",
                      (char *)"mem_access: \\valid_read(p + __gen_e_acsl_at)",
                      26);
      __gmpz_init_set_si(__gen_e_acsl_,(long)*(p + __gen_e_acsl_at));
      __gmpz_init_set(__gen_e_acsl_at_2,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
      __gmpz_clear(__gen_e_acsl_);
    }
    A = 4;
  /*@ assert \at(*(p + \at(*q,L1)),L2) ≡ 2; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl__2;
      int __gen_e_acsl_eq;
      __gmpz_init_set_si(__gen_e_acsl__2,2L);
      __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
      __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"g",
                      (char *)"\\at(*(p + \\at(*q,L1)),L2) == 2",26);
      __gmpz_clear(__gen_e_acsl__2);
    }
  }
  L3:
    /*@ assert \at(*(p + \at(*q,L1)),Here) ≡ 2; */
    {
      {
        __e_acsl_mpz_t __gen_e_acsl__3;
        __e_acsl_mpz_t __gen_e_acsl__4;
        int __gen_e_acsl_eq_2;
        __gmpz_init_set_si(__gen_e_acsl__3,(long)*(p + __gen_e_acsl_at_3));
        __gmpz_init_set_si(__gen_e_acsl__4,2L);
        __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__3),
                                       (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
        __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
                        (char *)"g",
                        (char *)"\\at(*(p + \\at(*q,L1)),Here) == 2",28);
        __gmpz_clear(__gen_e_acsl__3);
        __gmpz_clear(__gen_e_acsl__4);
      }
    }
    __e_acsl_delete_block((void *)(& p));
    __e_acsl_delete_block((void *)(& q));
    __gmpz_clear(__gen_e_acsl_at_2);
    return;
}

/*@ ensures \result ≡ \old(x); */
int __gen_e_acsl_h(int x);

/*@ ensures \result ≡ \old(x); */
int h(int x)
{
  __e_acsl_store_block((void *)(& x),(size_t)4);
  __e_acsl_delete_block((void *)(& x));
  return x;
}

int main(void)
{
  __e_acsl_mpz_t __gen_e_acsl_at_2;
  __e_acsl_mpz_t __gen_e_acsl_at;
  int __retres;
  int x;
  int t[2];
  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
  __e_acsl_store_block((void *)(t),(size_t)8);
  __e_acsl_store_block((void *)(& x),(size_t)4);
  __e_acsl_full_init((void *)(& x));
  x = __gen_e_acsl_h(0);
  L:
    {
      __e_acsl_mpz_t __gen_e_acsl_x_4;
      __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
      __gmpz_init_set(__gen_e_acsl_at,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4));
      __gmpz_clear(__gen_e_acsl_x_4);
    }
    {
      __e_acsl_mpz_t __gen_e_acsl_x_3;
      __e_acsl_mpz_t __gen_e_acsl__3;
      __e_acsl_mpz_t __gen_e_acsl_add;
      __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
      __gmpz_init_set_si(__gen_e_acsl__3,1L);
      __gmpz_init(__gen_e_acsl_add);
      __gmpz_add(__gen_e_acsl_add,
                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
      __gmpz_init_set(__gen_e_acsl_at_2,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_add));
      __gmpz_clear(__gen_e_acsl_x_3);
      __gmpz_clear(__gen_e_acsl__3);
      __gmpz_clear(__gen_e_acsl_add);
    }
    {
      __e_acsl_mpz_t __gen_e_acsl_x_2;
      __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
      __gmpz_init_set(__gen_e_acsl_at,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2));
      __gmpz_clear(__gen_e_acsl_x_2);
    }
    /*@ assert x ≡ 0; */
    {
      {
        __e_acsl_mpz_t __gen_e_acsl_x;
        __e_acsl_mpz_t __gen_e_acsl_;
        int __gen_e_acsl_eq;
        __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
        __gmpz_init_set_si(__gen_e_acsl_,0L);
        __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
        __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",
                        (char *)"main",(char *)"x == 0",43);
        __gmpz_clear(__gen_e_acsl_x);
        __gmpz_clear(__gen_e_acsl_);
      }
    }
    __e_acsl_full_init((void *)(& x));
    x = 1;
  __e_acsl_full_init((void *)(& x));
  x = 2;
  __gen_e_acsl_f();
  /*@ assert \at(x,L) ≡ 0; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl__2;
      int __gen_e_acsl_eq_2;
      __gmpz_init_set_si(__gen_e_acsl__2,0L);
      __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
      __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
                      (char *)"main",(char *)"\\at(x,L) == 0",48);
      __gmpz_clear(__gen_e_acsl__2);
    }
  }
  /*@ assert \at(x + 1,L) ≡ 1; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl__4;
      int __gen_e_acsl_eq_3;
      __gmpz_init_set_si(__gen_e_acsl__4,1L);
      __gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at_2),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
      __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
                      (char *)"main",(char *)"\\at(x + 1,L) == 1",49);
      __gmpz_clear(__gen_e_acsl__4);
    }
  }
  /*@ assert \at(x,L) + 1 ≡ 1; */
  {
    {
      __e_acsl_mpz_t __gen_e_acsl__5;
      __e_acsl_mpz_t __gen_e_acsl_add_2;
      int __gen_e_acsl_eq_4;
      __gmpz_init_set_si(__gen_e_acsl__5,1L);
      __gmpz_init(__gen_e_acsl_add_2);
      __gmpz_add(__gen_e_acsl_add_2,
                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
      __gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
                                     (__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
      __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
                      (char *)"main",(char *)"\\at(x,L) + 1 == 1",50);
      __gmpz_clear(__gen_e_acsl__5);
      __gmpz_clear(__gen_e_acsl_add_2);
    }
  }
  g(t,& x);
  __retres = 0;
  __gmpz_clear(__gen_e_acsl_at);
  __gmpz_clear(__gen_e_acsl_at_2);
  __e_acsl_delete_block((void *)(t));
  __e_acsl_delete_block((void *)(& x));
  __e_acsl_memory_clean();
  return __retres;
}

/*@ ensures \result ≡ \old(x); */
int __gen_e_acsl_h(int x)
{
  __e_acsl_mpz_t __gen_e_acsl_at;
  int __retres;
  __e_acsl_store_block((void *)(& __retres),(size_t)4);
  __e_acsl_store_block((void *)(& x),(size_t)4);
  {
    __e_acsl_mpz_t __gen_e_acsl_x;
    __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
    __gmpz_init_set(__gen_e_acsl_at,
                    (__e_acsl_mpz_struct const *)(__gen_e_acsl_x));
    __gmpz_clear(__gen_e_acsl_x);
  }
  __retres = h(x);
  {
    __e_acsl_mpz_t __gen_e_acsl_result;
    int __gen_e_acsl_eq;
    __gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_at));
    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"h",
                    (char *)"\\result == \\old(x)",35);
    __e_acsl_delete_block((void *)(& x));
    __gmpz_clear(__gen_e_acsl_result);
    __gmpz_clear(__gen_e_acsl_at);
    __e_acsl_delete_block((void *)(& __retres));
    return __retres;
  }
}

/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void)
{
  __e_acsl_mpz_t __gen_e_acsl_at;
  f();
  {
    __e_acsl_mpz_t __gen_e_acsl_;
    int __gen_e_acsl_eq;
    {
      __e_acsl_mpz_t __gen_e_acsl_A;
      __gmpz_init_set_si(__gen_e_acsl_A,(long)A);
      __gmpz_init_set(__gen_e_acsl_at,
                      (__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
      __gmpz_clear(__gen_e_acsl_A);
    }
    __gmpz_init_set_si(__gen_e_acsl_,3L);
    __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_at),
                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
    __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
                    (char *)"\\at(A,Post) == 3",7);
    __gmpz_clear(__gen_e_acsl_);
    __gmpz_clear(__gen_e_acsl_at);
    return;
  }
}