gen_e-acsl-bittree-model.c 368 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int main(void)
{
  int __retres;
  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
  __e_acsl_store_block((void *)(& __retres),(size_t)4);
  __e_acsl_full_init((void *)(& __retres));
  __retres = 0;
  __e_acsl_delete_block((void *)(& __retres));
  __e_acsl_memory_clean();
  return __retres;
}