[E-ACSL] add test for unpaired fopen

src/plugins/e-acsl/tests/bts/issue-eacsl-40.c

 /* run.config
    COMMENT: frama-c/e-acsl#40, test for initialized memory after a call to fread
    on /dev/urandom.
+   STDOPT:
+   COMMENT: In some GCC/libc versions, GCC uses 'malloc' function attributes
+   COMMENT: with deallocator names; if these deallocators have been cleaned up
+   COMMENT: by Rmtmps, the resulting code will not parse. To avoid that, such
+   COMMENT: attributes are erased by Frama-C's kernel. The test below checks
+   COMMENT: whether code produced by E-ACSL's instrumentation remains parsable
+   COMMENT: by GCC.
+   COMMENT: The 'LIBS:' line below disables the filter set by E_ACSL_test.ml
+   LIBS:
+   LOG: @PTEST_NAME@.out.frama.c
+   OPT: @GLOBAL@ @EACSL@ -cpp-extra-args="-DNO_FCLOSE" -c11 -no-frama-c-stdlib -then-last -print -ocode @PTEST_NAME@.out.frama.c
+ ENABLED_IF: %{bin-available:gcc}
+   EXECNOW: BIN @PTEST_NAME@.o gcc -Wno-attributes %{dep:@PTEST_NAME@.out.frama.c} -c -o @PTEST_NAME@.o >@DEV_NULL@ 2>@DEV_NULL@
 */
 
 #include <stdio.h>
@@ -11,7 +24,9 @@ int main() {
   if (f) {
     char buf[4];
     int res = fread(buf, 1, 4, f);
+#ifndef NO_FCLOSE
     fclose(f);
+#endif
     if (res == 4) {
       //@ assert \initialized(&buf[3]);
       buf[0] = buf[3];

src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c

@@ -527,7 +527,7 @@ int main(void)
         __gen_e_acsl_assert_data.pred_txt = "\\initialized(&buf_0[3])";
         __gen_e_acsl_assert_data.file = "issue-eacsl-40.c";
         __gen_e_acsl_assert_data.fct = "main";
-        __gen_e_acsl_assert_data.line = 16;
+        __gen_e_acsl_assert_data.line = 31;
         __e_acsl_assert(__gen_e_acsl_initialized,& __gen_e_acsl_assert_data);
         __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
       }

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle → src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle

@@ -87,12 +87,12 @@
 [eva:alarm] FRAMAC_SHARE/libc/stdio.h:122: Warning: 
   function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                       \valid(data->values) got status unknown.
-[eva:alarm] issue-eacsl-40.c:16: Warning: 
+[eva:alarm] issue-eacsl-40.c:31: Warning: 
   function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                         \valid(data->values) got status unknown.
-[eva:alarm] issue-eacsl-40.c:16: Warning: 
+[eva:alarm] issue-eacsl-40.c:31: Warning: 
   function __e_acsl_assert_register_int: precondition data->values == \null ||
                                                       \valid(data->values) got status unknown.
-[eva:alarm] issue-eacsl-40.c:16: Warning: 
+[eva:alarm] issue-eacsl-40.c:31: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] issue-eacsl-40.c:16: Warning: assertion got status unknown.
+[eva:alarm] issue-eacsl-40.c:31: Warning: assertion got status unknown.

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c

+/* Generated by Frama-C */
+char *__gen_e_acsl_literal_string;
+char *__gen_e_acsl_literal_string_2;
+typedef long __off_t;
+typedef long __off64_t;
+typedef unsigned long uintptr_t;
+typedef unsigned long size_t;
+typedef int wchar_t;
+struct _IO_FILE;
+typedef struct _IO_FILE FILE;
+struct _IO_marker;
+struct _IO_codecvt;
+struct _IO_wide_data;
+typedef void _IO_lock_t;
+struct _IO_FILE;
+struct __e_acsl_mpz_struct {
+   int _mp_alloc ;
+   int _mp_size ;
+   unsigned long *_mp_d ;
+};
+typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
+typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
+struct __e_acsl_mpq_struct {
+   __e_acsl_mpz_struct _mp_num ;
+   __e_acsl_mpz_struct _mp_den ;
+};
+typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
+typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
+typedef unsigned long __e_acsl_mp_bitcnt_t;
+enum __e_acsl_assert_data_type_t {
+    E_ACSL_INT = 0,
+    E_ACSL_REAL = 1,
+    E_ACSL_PTR = 2,
+    E_ACSL_ARRAY = 3,
+    E_ACSL_FUN = 4,
+    E_ACSL_STRUCT = 5,
+    E_ACSL_UNION = 6,
+    E_ACSL_OTHER = 1000
+};
+typedef enum __e_acsl_assert_data_type_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_type_t;
+enum __e_acsl_assert_data_ikind_t {
+    E_ACSL_IBOOL = 0,
+    E_ACSL_ICHAR = 1,
+    E_ACSL_ISCHAR = 2,
+    E_ACSL_IUCHAR = 3,
+    E_ACSL_IINT = 4,
+    E_ACSL_IUINT = 5,
+    E_ACSL_ISHORT = 6,
+    E_ACSL_IUSHORT = 7,
+    E_ACSL_ILONG = 8,
+    E_ACSL_IULONG = 9,
+    E_ACSL_ILONGLONG = 10,
+    E_ACSL_IULONGLONG = 11,
+    E_ACSL_IMPZ = 12
+};
+typedef enum __e_acsl_assert_data_ikind_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_ikind_t;
+enum __e_acsl_assert_data_rkind_t {
+    E_ACSL_RFLOAT = 0,
+    E_ACSL_RDOUBLE = 1,
+    E_ACSL_RLONGDOUBLE = 2,
+    E_ACSL_RMPQ = 3
+};
+typedef enum __e_acsl_assert_data_rkind_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_rkind_t;
+union __e_acsl_assert_data_int_value_t {
+   _Bool value_bool ;
+   char value_char ;
+   signed char value_schar ;
+   unsigned char value_uchar ;
+   int value_int ;
+   unsigned int value_uint ;
+   short value_short ;
+   unsigned short value_ushort ;
+   long value_long ;
+   unsigned long value_ulong ;
+   long long value_llong ;
+   unsigned long long value_ullong ;
+   struct __e_acsl_mpz_struct *value_mpz ;
+};
+typedef union __e_acsl_assert_data_int_value_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_int_value_t;
+union __e_acsl_assert_data_real_value_t {
+   float value_float ;
+   double value_double ;
+   long double value_ldouble ;
+   struct __e_acsl_mpq_struct *value_mpq ;
+};
+typedef union __e_acsl_assert_data_real_value_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_real_value_t;
+struct __e_acsl_assert_data_int_content_t {
+   int is_enum ;
+   __e_acsl_assert_data_ikind_t kind ;
+   __e_acsl_assert_data_int_value_t value ;
+};
+typedef struct __e_acsl_assert_data_int_content_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_int_content_t;
+struct __e_acsl_assert_data_real_content_t {
+   __e_acsl_assert_data_rkind_t kind ;
+   __e_acsl_assert_data_real_value_t value ;
+};
+typedef struct __e_acsl_assert_data_real_content_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_real_content_t;
+union __e_acsl_assert_data_content_t {
+   __e_acsl_assert_data_int_content_t int_content ;
+   __e_acsl_assert_data_real_content_t real_content ;
+   uintptr_t value_ptr ;
+   uintptr_t value_array ;
+};
+typedef union __e_acsl_assert_data_content_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_content_t;
+struct __e_acsl_assert_data_value_t {
+   char const *name ;
+   __e_acsl_assert_data_type_t type ;
+   __e_acsl_assert_data_content_t content ;
+   struct __e_acsl_assert_data_value_t *next ;
+};
+typedef struct __e_acsl_assert_data_value_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_value_t;
+struct __e_acsl_assert_data_t {
+   int blocking ;
+   char const *kind ;
+   char const *name ;
+   char const *pred_txt ;
+   char const *file ;
+   char const *fct ;
+   int line ;
+   __e_acsl_assert_data_value_t *values ;
+};
+typedef struct __e_acsl_assert_data_t __attribute__((__FC_BUILTIN__)) __e_acsl_assert_data_t;
+struct __e_acsl_contract_t;
+typedef struct __e_acsl_contract_t __attribute__((__FC_BUILTIN__)) __e_acsl_contract_t;
+typedef unsigned long pthread_t;
+union pthread_attr_t {
+   char __size[56] ;
+   long __align ;
+};
+typedef union pthread_attr_t pthread_attr_t;
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ requires !\initialized(z);
+    ensures \valid(\old(z));
+    assigns *z;
+    assigns *z \from __e_acsl_init;
+    allocates \old(z);
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __gmpz_init(__e_acsl_mpz_struct ( __attribute__((
+                                                         __FC_BUILTIN__)) z)[1]);
+
+/*@ requires !\initialized(z);
+    ensures \valid(\old(z));
+    ensures \initialized(\old(z));
+    assigns *z;
+    assigns *z \from n;
+    allocates \old(z);
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__e_acsl_mpz_struct ( __attribute__((
+                                                                __FC_BUILTIN__)) z)[1],
+                                                                unsigned long n);
+
+/*@ requires \valid(x);
+    assigns *x;
+    assigns *x \from *x; */
+extern  __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__e_acsl_mpz_struct ( __attribute__((
+                                                          __FC_BUILTIN__)) x)[1]);
+
+/*@ requires \valid_read(z1);
+    requires \valid_read(z2);
+    assigns \result;
+    assigns \result \from *z1, *z2;
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__e_acsl_mpz_struct const ( __attribute__((
+                                                       __FC_BUILTIN__)) z1)[1],
+                                                       __e_acsl_mpz_struct const ( __attribute__((
+                                                       __FC_BUILTIN__)) z2)[1]);
+
+/*@ requires \valid(z1);
+    requires \valid_read(z2);
+    requires \valid_read(z3);
+    assigns *z1;
+    assigns *z1 \from *z2, *z3;
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__e_acsl_mpz_struct ( __attribute__((
+                                                        __FC_BUILTIN__)) z1)[1],
+                                                        __e_acsl_mpz_struct const ( __attribute__((
+                                                        __FC_BUILTIN__)) z2)[1],
+                                                        __e_acsl_mpz_struct const ( __attribute__((
+                                                        __FC_BUILTIN__)) z3)[1]);
+
+/*@ requires \valid_read(z);
+    assigns \result;
+    assigns \result \from *z; */
+extern  __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__e_acsl_mpz_struct const ( __attribute__((
+                                                                    __FC_BUILTIN__)) z)[1]);
+
+/*@ requires \valid_read(data) && \initialized(data);
+    assigns \nothing;
+    
+    behavior blocking:
+      assumes data->blocking != 0;
+      requires predicate != 0;
+    
+    behavior non_blocking:
+      assumes data->blocking == 0;
+      check requires predicate != 0;
+    
+    complete behaviors non_blocking, blocking;
+    disjoint behaviors non_blocking, blocking;
+ */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert(int predicate,
+                                                      __e_acsl_assert_data_t *data);
+
+extern size_t __e_acsl_heap_allocation_size;
+
+extern size_t __e_acsl_heap_allocated_blocks;
+
+/*@ ghost extern int __fc_heap_status; */
+
+/*@ requires \valid(data);
+    requires data->values == \null || \valid(data->values);
+    assigns data->values;
+    assigns data->values \from (indirect: __fc_heap_status), value;
+ */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_register_int(__e_acsl_assert_data_t *data,
+                                                                   char const *name,
+                                                                   int is_enum,
+                                                                   int value);
+
+/*@ requires \valid(data);
+    requires data->values == \null || \valid(data->values);
+    assigns data->values;
+    assigns data->values \from (indirect: __fc_heap_status), value;
+ */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_register_ulong(
+                                                                    __e_acsl_assert_data_t *data,
+                                                                    char const *name,
+                                                                    int is_enum,
+                                                                    unsigned long value);
+
+/*@ requires \valid(data);
+    requires data->values == \null || \valid(data->values);
+    assigns data->values;
+    assigns data->values \from (indirect: __fc_heap_status), ptr;
+ */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_register_ptr(__e_acsl_assert_data_t *data,
+                                                                   char const *name,
+                                                                   void *ptr);
+
+/*@ requires \valid(data);
+    assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_assert_clean(__e_acsl_assert_data_t *data);
+
+/*@
+axiomatic dynamic_allocation {
+  predicate is_allocable{L}(integer n) 
+    reads __fc_heap_status;
+  
+  axiom never_allocable{L}:
+    \forall integer i;
+      i < 0 || i > 18446744073709551615UL ==> !is_allocable(i);
+  
+  }
+ */
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_init(int *argc_ref,
+                                                           char ***argv,
+                                                           size_t ptr_size);
+
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+/*@ ensures \result == \old(ptr);
+    assigns \result;
+    assigns \result \from *((char *)ptr + (0 .. size - 1)), ptr, size;
+ */
+ __attribute__((__FC_BUILTIN__)) void *__e_acsl_store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_initialize(void *ptr,
+                                                          size_t size);
+
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_full_init(void *ptr);
+
+/*@ assigns \nothing; */
+ __attribute__((__FC_BUILTIN__)) void __e_acsl_mark_readonly(void *ptr);
+
+/*@ assigns \result;
+    assigns \result \from *((char *)ptr + (0 .. size - 1)), ptr, size;
+    
+    behavior initialized:
+      assumes \initialized((char *)ptr + (0 .. size - 1));
+      ensures \result == 1;
+    
+    behavior uninitialized:
+      assumes !\initialized((char *)ptr + (0 .. size - 1));
+      ensures \result == 0;
+    
+    complete behaviors uninitialized, initialized;
+    disjoint behaviors uninitialized, initialized;
+ */
+ __attribute__((__FC_BUILTIN__)) int __e_acsl_initialized(void *ptr,
+                                                          size_t size);
+
+long valid_nstring(char *s, long n, int wrtbl);
+
+long valid_nwstring(wchar_t *s, long n, int wrtbl);
+
+__inline static long valid_string__fc_inline(char *s, int wrtbl)
+{
+  long tmp;
+  tmp = valid_nstring(s,(long)(-1),wrtbl);
+  return tmp;
+}
+
+__inline static long valid_wstring__fc_inline(wchar_t *s, int wrtbl)
+{
+  long tmp;
+  tmp = valid_nwstring(s,(long)(-1),wrtbl);
+  return tmp;
+}
+
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+typedef unsigned long size_t;
+typedef long __off_t;
+typedef long __off64_t;
+struct _IO_FILE;
+typedef struct _IO_FILE FILE;
+struct _IO_marker;
+struct _IO_codecvt;
+struct _IO_wide_data;
+typedef void _IO_lock_t;
+struct _IO_FILE {
+   int _flags ;
+   char *_IO_read_ptr ;
+   char *_IO_read_end ;
+   char *_IO_read_base ;
+   char *_IO_write_base ;
+   char *_IO_write_ptr ;
+   char *_IO_write_end ;
+   char *_IO_buf_base ;
+   char *_IO_buf_end ;
+   char *_IO_save_base ;
+   char *_IO_backup_base ;
+   char *_IO_save_end ;
+   struct _IO_marker *_markers ;
+   struct _IO_FILE *_chain ;
+   int _fileno ;
+   int _flags2 ;
+   __off_t _old_offset ;
+   unsigned short _cur_column ;
+   signed char _vtable_offset ;
+   char _shortbuf[1] ;
+   _IO_lock_t *_lock ;
+   __off64_t _offset ;
+   struct _IO_codecvt *_codecvt ;
+   struct _IO_wide_data *_wide_data ;
+   struct _IO_FILE *_freeres_list ;
+   void *_freeres_buf ;
+   size_t __pad5 ;
+   int _mode ;
+   char _unused2[((unsigned long)15 * sizeof(int) - (unsigned long)4 * sizeof(void *)) - sizeof(size_t)] ;
+};
+extern FILE *fopen(char const * restrict __filename,
+                   char const * restrict __modes);
+
+extern size_t fread(void * restrict __ptr, size_t __size, size_t __n,
+                    FILE * restrict __stream);
+
+void __e_acsl_globals_init(void)
+{
+  static char __e_acsl_already_run = 0;
+  if (! __e_acsl_already_run) {
+    __e_acsl_already_run = 1;
+    __gen_e_acsl_literal_string = "r";
+    __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("r"));
+    __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+    __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string);
+    __gen_e_acsl_literal_string_2 = "/dev/urandom";
+    __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+                         sizeof("/dev/urandom"));
+    __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+    __e_acsl_mark_readonly((void *)__gen_e_acsl_literal_string_2);
+  }
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  char buf[4];
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  __e_acsl_globals_init();
+  FILE *f = fopen(__gen_e_acsl_literal_string_2,__gen_e_acsl_literal_string);
+  if (f) {
+    char buf_0[4];
+    size_t tmp_0;
+    __e_acsl_store_block((void *)(buf_0),4UL);
+    tmp_0 = fread((void *)(buf_0),(size_t)1,(size_t)4,f);
+    {
+      size_t __gen_e_acsl_;
+      __e_acsl_mpz_t __gen_e_acsl_tmp_0;
+      __e_acsl_mpz_t __gen_e_acsl___gen_e_acsl_;
+      __e_acsl_mpz_t __gen_e_acsl_mul;
+      __e_acsl_mpz_t __gen_e_acsl__2;
+      int __gen_e_acsl_le;
+      unsigned long __gen_e_acsl_size;
+      __gen_e_acsl_ = (size_t)1;
+      __e_acsl_assert_data_t __gen_e_acsl_assert_data =
+        {.values = (void *)0};
+      __gmpz_init_set_ui(__gen_e_acsl_tmp_0,tmp_0);
+      __gmpz_init_set_ui(__gen_e_acsl___gen_e_acsl_,__gen_e_acsl_);
+      __gmpz_init(__gen_e_acsl_mul);
+      __gmpz_mul(__gen_e_acsl_mul,
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl_tmp_0),
+                 (__e_acsl_mpz_struct const *)(__gen_e_acsl___gen_e_acsl_));
+      __gmpz_init_set_ui(__gen_e_acsl__2,18446744073709551615UL);
+      __gen_e_acsl_le = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul),
+                                   (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+      __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"tmp_0",0,
+                                     tmp_0);
+      __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,
+                                     "__gen_e_acsl_",0,__gen_e_acsl_);
+      __gen_e_acsl_assert_data.blocking = 1;
+      __gen_e_acsl_assert_data.kind = "RTE";
+      __gen_e_acsl_assert_data.pred_txt = "tmp_0 * __gen_e_acsl_ <= 18446744073709551615";
+      __gen_e_acsl_assert_data.file = "issue-eacsl-40.c";
+      __gen_e_acsl_assert_data.fct = "main";
+      __gen_e_acsl_assert_data.line = 26;
+      __gen_e_acsl_assert_data.name = "size_lesser_or_eq_than_SIZE_MAX";
+      __e_acsl_assert(__gen_e_acsl_le <= 0,& __gen_e_acsl_assert_data);
+      __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+      __gen_e_acsl_size = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
+      __e_acsl_initialize((void *)(buf_0),__gen_e_acsl_size);
+      __gmpz_clear(__gen_e_acsl_tmp_0);
+      __gmpz_clear(__gen_e_acsl___gen_e_acsl_);
+      __gmpz_clear(__gen_e_acsl_mul);
+      __gmpz_clear(__gen_e_acsl__2);
+    }
+    int res = (int)tmp_0;
+    if (res == 4) {
+      {
+        int __gen_e_acsl_initialized;
+        __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
+          {.values = (void *)0};
+        __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& buf_0[3]),
+                                                        sizeof(char));
+        __e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,
+                                     "&buf_0[3]",(void *)(& buf_0[3]));
+        __e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
+                                       "sizeof(char)",0,sizeof(char));
+        __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
+                                     "\\initialized(&buf_0[3])",0,
+                                     __gen_e_acsl_initialized);
+        __gen_e_acsl_assert_data_2.blocking = 1;
+        __gen_e_acsl_assert_data_2.kind = "Assertion";
+        __gen_e_acsl_assert_data_2.pred_txt = "\\initialized(&buf_0[3])";
+        __gen_e_acsl_assert_data_2.file = "issue-eacsl-40.c";
+        __gen_e_acsl_assert_data_2.fct = "main";
+        __gen_e_acsl_assert_data_2.line = 31;
+        __e_acsl_assert(__gen_e_acsl_initialized,
+                        & __gen_e_acsl_assert_data_2);
+        __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
+      }
+      /*@ assert \initialized(&buf_0[3]); */ ;
+      __e_acsl_initialize((void *)(buf_0),sizeof(char));
+      buf_0[0] = buf_0[3];
+    }
+    else {
+      __retres = 2;
+      __e_acsl_delete_block((void *)(buf_0));
+      goto return_label;
+    }
+    __e_acsl_delete_block((void *)(buf_0));
+  }
+  else {
+    __retres = 1;
+    goto return_label;
+  }
+  __retres = 0;
+  return_label: {
+                  __e_acsl_memory_clean();
+                  return __retres;
+                }
+}
+
+