gen_freeable.c

/* Generated by Frama-C */
char array[1024];
void __e_acsl_globals_init(void)
{
  __e_acsl_store_block((void *)(array),1024UL);
  __e_acsl_full_init((void *)(& array));
  return;
}

int main(void)
{
  int __retres;
  int *p;
  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
  __e_acsl_globals_init();
  __e_acsl_store_block((void *)(& p),8UL);
  /*@ assert ¬\freeable(p); */
  {
    int __gen_e_acsl_freeable;
    /*@ assert Value: initialisation: \initialized(&p); */
    __gen_e_acsl_freeable = __e_acsl_freeable((void *)p);
    __e_acsl_assert(! __gen_e_acsl_freeable,(char *)"Assertion",
                    (char *)"main",(char *)"!\\freeable(p)",15);
  }
  /*@ assert ¬\freeable((void *)0); */
  {
    int __gen_e_acsl_freeable_2;
    __gen_e_acsl_freeable_2 = __e_acsl_freeable((void *)0);
    __e_acsl_assert(! __gen_e_acsl_freeable_2,(char *)"Assertion",
                    (char *)"main",(char *)"!\\freeable((void *)0)",16);
  }
  __e_acsl_full_init((void *)(& p));
  p = (int *)malloc((unsigned long)4 * sizeof(int));
  /*@ assert ¬\freeable(p+1); */
  {
    int __gen_e_acsl_freeable_3;
    __gen_e_acsl_freeable_3 = __e_acsl_freeable((void *)(p + 1UL));
    __e_acsl_assert(! __gen_e_acsl_freeable_3,(char *)"Assertion",
                    (char *)"main",(char *)"!\\freeable(p+1)",18);
  }
  /*@ assert \freeable(p); */
  {
    int __gen_e_acsl_freeable_4;
    __gen_e_acsl_freeable_4 = __e_acsl_freeable((void *)p);
    __e_acsl_assert(__gen_e_acsl_freeable_4,(char *)"Assertion",
                    (char *)"main",(char *)"\\freeable(p)",19);
  }
  free((void *)p);
  /*@ assert ¬\freeable(p); */
  {
    int __gen_e_acsl_freeable_5;
    __gen_e_acsl_freeable_5 = __e_acsl_freeable((void *)p);
    __e_acsl_assert(! __gen_e_acsl_freeable_5,(char *)"Assertion",
                    (char *)"main",(char *)"!\\freeable(p)",21);
  }
  /*@ assert ¬\freeable((char *)array); */
  {
    int __gen_e_acsl_freeable_6;
    __gen_e_acsl_freeable_6 = __e_acsl_freeable((void *)(array));
    __e_acsl_assert(! __gen_e_acsl_freeable_6,(char *)"Assertion",
                    (char *)"main",(char *)"!\\freeable((char *)array)",24);
  }
  /*@ assert ¬\freeable(&array[5]); */
  {
    int __gen_e_acsl_freeable_7;
    __gen_e_acsl_freeable_7 = __e_acsl_freeable((void *)(& array[5UL]));
    __e_acsl_assert(! __gen_e_acsl_freeable_7,(char *)"Assertion",
                    (char *)"main",(char *)"!\\freeable(&array[5])",25);
  }
  __retres = 0;
  __e_acsl_delete_block((void *)(array));
  __e_acsl_delete_block((void *)(& p));
  __e_acsl_memory_clean();
  return __retres;
}