gen_ghost.c

/* Generated by Frama-C */
struct __anonstruct___mpz_struct_1 {
   int _mp_alloc ;
   int _mp_size ;
   unsigned long *_mp_d ;
};
typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
typedef unsigned int size_t;
/*@ requires predicate ≢ 0;
    assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
                                                           char *kind,
                                                           char *fct,
                                                           char *pred_txt,
                                                           int line);

/*@
model __mpz_struct { ℤ n };
*/
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */

/*@
axiomatic
  dynamic_allocation {
  predicate is_allocable{L}(size_t n) 
    reads __fc_heap_status;
  
  }
 */
/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
                                                            size_t size);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
                                                          size_t size);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);

/*@ assigns \nothing; */
extern  __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
                                                         size_t size);

/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
    ensures
      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
    assigns \nothing;
 */
extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
                                                          size_t size);

extern  __attribute__((__FC_BUILTIN__)) void __clean(void);

extern size_t __memory_size;

/*@
predicate diffSize{L1, L2}(ℤ i) =
  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
 */
int G = 0;
int *P;
void e_acsl_global_init(void)
{
  __store_block((void *)(& P),4U);
  __store_block((void *)(& G),4U);
  return;
}

int main(void)
{
  int __retres;
  int *q;
  e_acsl_global_init();
  __store_block((void *)(& q),4U);
  P = & G;
  __full_init((void *)(& q));
  q = P;
  {
    int __e_acsl_valid_read;
    int __e_acsl_valid;
    __initialize((void *)P,sizeof(int));
    __e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
    e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",(char *)"main",
                  (char *)"mem_access: \\valid_read(P)",16);
    __e_acsl_valid = __valid((void *)P,sizeof(int));
    e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
                  (char *)"mem_access: \\valid(P)",16);
    (*P) ++;
  }
  /*@ assert *q ≡ G; */
  {
    int __e_acsl_initialized;
    int __e_acsl_and;
    __e_acsl_initialized = __initialized((void *)(& q),sizeof(int *));
    if (__e_acsl_initialized) {
      int __e_acsl_valid_read_2;
      __e_acsl_valid_read_2 = __valid_read((void *)q,sizeof(int));
      __e_acsl_and = __e_acsl_valid_read_2;
    }
    else __e_acsl_and = 0;
    e_acsl_assert(__e_acsl_and,(char *)"RTE",(char *)"main",
                  (char *)"mem_access: \\valid_read(q)",17);
    e_acsl_assert(*q == G,(char *)"Assertion",(char *)"main",
                  (char *)"*q == G",17);
  }
  __retres = 0;
  __delete_block((void *)(& P));
  __delete_block((void *)(& G));
  __delete_block((void *)(& q));
  __clean();
  return __retres;
}