diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
index aa21266b8c8266aee648615e72d6df675a25adc8..a449692806591f8493465d496a6533d927511774 100644
--- a/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-40.c
@@ -1,6 +1,19 @@
/* 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];
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
index ad1fd155052e5c428dc732b8365cd7a6ce1c43c9..ff974a15990493fc1ff382718a01ec6baa6ba8f1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
+++ b/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);
}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle
similarity index 96%
rename from src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.0.res.oracle
index a33ac7b284bde4a5fa2360f566b232758a18102e..42cba99e4ca3d95a97530e0abced583e29429625 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
+++ b/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.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.1.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c
new file mode 100644
index 0000000000000000000000000000000000000000..5288e9f6f6960ae59fed9d9b1550d75d8361b078
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.out.frama.c
@@ -0,0 +1,484 @@
+/* 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;
+ }
+}
+
+