diff --git a/src/plugins/e-acsl/.gitlab-ci.yml b/src/plugins/e-acsl/.gitlab-ci.yml
index 087f91d184fdd9203d47e51f0d002b793a4b914d..5aa854a9ec762fe73b1bd57c78e708762e8317b3 100644
--- a/src/plugins/e-acsl/.gitlab-ci.yml
+++ b/src/plugins/e-acsl/.gitlab-ci.yml
@@ -5,3 +5,7 @@ Tests:
- "./configure"
- make -j 12
- make PTESTS_OPTS="-error-code -j 4" tests -j 12
+ - make clean
+ tags:
+ except:
+ - tags
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c b/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c
new file mode 100644
index 0000000000000000000000000000000000000000..c83b3eb4eff1bcd7dcd75889e050f0d26e044f61
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c
@@ -0,0 +1,47 @@
+/* run.config
+ COMMENT: Compound initializers
+ EXECNOW: LOG gen_compound_initializers.c BIN gen_compound_initializers.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/compound_initializers.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_compound_initializers.c > /dev/null && ./gcc_runtime.sh compound_initializers
+ EXECNOW: LOG gen_compound_initializers2.c BIN gen_compound_initializers2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/compound_initializers.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_compound_initializers2.c > /dev/null && ./gcc_runtime.sh compound_initializers2
+*/
+
+
+
+int _F;
+
+char *_A[2] = { "XX", "YY" };
+char *_B = "ZZ";
+char *_C;
+int _D[] = { 44, 88 };
+int _E = 44;
+int _F = 9;;
+
+struct ST {
+ char *str;
+ int num;
+};
+
+struct ST _G[] = {
+ {
+ .str = "First",
+ .num = 99
+ },
+ {
+ .str = "Second",
+ .num = 147
+ }
+};
+
+int main(int argc, char **argv) {
+ /*@ assert \valid(_A); */
+ /*@ assert \valid_read(_A[0]); */
+ /*@ assert \valid_read(_A[1]); */
+ /*@ assert \valid_read(_B); */
+ /*@ assert \valid(&_C); */
+ /*@ assert \valid(_D); */
+ /*@ assert \valid(&_E); */
+ /*@ assert \valid(&_F); */
+ /*@ assert _E == 44; */
+ /*@ assert \valid(&_G); */
+ /*@ assert _G[0].num == 99; */
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f8184dd9d7f961f26e8c6a45a6b414e94727def2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
@@ -0,0 +1,52 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ _F ∈ {9}
+ _A[0] ∈ {{ "XX" }}
+ [1] ∈ {{ "YY" }}
+ _B ∈ {{ "ZZ" }}
+ _C ∈ {0}
+ _D[0] ∈ {44}
+ [1] ∈ {88}
+ _E ∈ {44}
+ _G[0].str ∈ {{ "First" }}
+ [0].num ∈ {99}
+ [1].str ∈ {{ "Second" }}
+ [1].num ∈ {147}
+ __e_acsl_literal_string ∈ {0}
+ __e_acsl_literal_string_2 ∈ {0}
+ __e_acsl_literal_string_3 ∈ {0}
+ __e_acsl_literal_string_4 ∈ {0}
+ __e_acsl_literal_string_5 ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
+tests/e-acsl-runtime/compound_initializers.c:35:[value] Assertion got status valid.
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/compound_initializers.c:36:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/compound_initializers.c:37:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:38:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:39:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:40:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:41:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:42:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:43:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/e-acsl-runtime/compound_initializers.c:44:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:45:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f170948d04d2eeaab43e6d9d08fe2e928d3a2abe
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle
@@ -0,0 +1,58 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __e_acsl_init ∈ [--..--]
+ __e_acsl_internal_heap ∈ [--..--]
+ __memory_size ∈ [--..--]
+ _F ∈ {9}
+ _A[0] ∈ {{ "XX" }}
+ [1] ∈ {{ "YY" }}
+ _B ∈ {{ "ZZ" }}
+ _C ∈ {0}
+ _D[0] ∈ {44}
+ [1] ∈ {88}
+ _E ∈ {44}
+ _G[0].str ∈ {{ "First" }}
+ [0].num ∈ {99}
+ [1].str ∈ {{ "Second" }}
+ [1].num ∈ {147}
+ __e_acsl_literal_string ∈ {0}
+ __e_acsl_literal_string_2 ∈ {0}
+ __e_acsl_literal_string_3 ∈ {0}
+ __e_acsl_literal_string_4 ∈ {0}
+ __e_acsl_literal_string_5 ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+[value] using specification for function __literal_string
+tests/e-acsl-runtime/compound_initializers.c:35:[value] Assertion got status valid.
+[value] using specification for function __valid
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/compound_initializers.c:36:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[value] using specification for function __valid_read
+tests/e-acsl-runtime/compound_initializers.c:37:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:38:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:39:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:40:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:41:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:42:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:43:[value] Assertion got status valid.
+[value] using specification for function __gmpz_init_set_si
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
+[value] using specification for function __gmpz_cmp
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function __gmpz_clear
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
+tests/e-acsl-runtime/compound_initializers.c:44:[value] Assertion got status valid.
+tests/e-acsl-runtime/compound_initializers.c:45:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
new file mode 100644
index 0000000000000000000000000000000000000000..27996ac8709e0d0fd748d7e102da690d3722b5af
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
@@ -0,0 +1,243 @@
+/* Generated by Frama-C */
+char *__e_acsl_literal_string_3;
+char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string_4;
+char *__e_acsl_literal_string_5;
+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 long size_t;
+struct ST {
+ char *str ;
+ int num ;
+};
+/*@ 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__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+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 __full_init(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+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 \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int _F;
+
+char *_A[2] = {(char *)"XX", (char *)"YY"};
+char *_B = (char *)"ZZ";
+char *_C;
+int _D[2] = {44, 88};
+int _E = 44;
+int _F = 9;
+struct ST _G[2] =
+ {{.str = (char *)"First", .num = 99}, {.str = (char *)"Second", .num = 147}};
+void __e_acsl_memory_init(void)
+{
+ __e_acsl_literal_string_3 = "ZZ";
+ __store_block((void *)__e_acsl_literal_string_3,sizeof("ZZ"));
+ __full_init((void *)__e_acsl_literal_string_3);
+ __literal_string((void *)__e_acsl_literal_string_3);
+ __e_acsl_literal_string = "YY";
+ __store_block((void *)__e_acsl_literal_string,sizeof("YY"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __e_acsl_literal_string_2 = "XX";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("XX"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __e_acsl_literal_string_4 = "Second";
+ __store_block((void *)__e_acsl_literal_string_4,sizeof("Second"));
+ __full_init((void *)__e_acsl_literal_string_4);
+ __literal_string((void *)__e_acsl_literal_string_4);
+ __e_acsl_literal_string_5 = "First";
+ __store_block((void *)__e_acsl_literal_string_5,sizeof("First"));
+ __full_init((void *)__e_acsl_literal_string_5);
+ __literal_string((void *)__e_acsl_literal_string_5);
+ __store_block((void *)(_G),32UL);
+ __full_init((void *)(& _G));
+ __store_block((void *)(& _E),4UL);
+ __full_init((void *)(& _E));
+ __store_block((void *)(_D),8UL);
+ __full_init((void *)(& _D));
+ __store_block((void *)(& _C),8UL);
+ __full_init((void *)(& _C));
+ __store_block((void *)(& _B),8UL);
+ __full_init((void *)(& _B));
+ __store_block((void *)(_A),16UL);
+ __full_init((void *)(& _A));
+ __store_block((void *)(& _F),4UL);
+ __full_init((void *)(& _F));
+ return;
+}
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init();
+ /*@ assert \valid((char **)_A); */
+ {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)(_A),sizeof(char *));
+ e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid((char **)_A)",35);
+ }
+ /*@ assert \valid_read(_A[0]); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(_A),sizeof(char *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)_A[0],sizeof(char));
+ __e_acsl_and = __e_acsl_valid_read;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_A[0])",36);
+ }
+ /*@ assert \valid_read(_A[1]); */
+ {
+ int __e_acsl_initialized_2;
+ int __e_acsl_and_2;
+ __e_acsl_initialized_2 = __initialized((void *)(& _A[1]),sizeof(char *));
+ if (__e_acsl_initialized_2) {
+ int __e_acsl_valid_read_2;
+ __e_acsl_valid_read_2 = __valid_read((void *)_A[1],sizeof(char));
+ __e_acsl_and_2 = __e_acsl_valid_read_2;
+ }
+ else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_A[1])",37);
+ }
+ /*@ assert \valid_read(_B); */
+ {
+ int __e_acsl_valid_read_3;
+ __e_acsl_valid_read_3 = __valid_read((void *)_B,sizeof(char));
+ e_acsl_assert(__e_acsl_valid_read_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_B)",38);
+ }
+ /*@ assert \valid(&_C); */
+ {
+ int __e_acsl_valid_2;
+ __e_acsl_valid_2 = __valid((void *)(& _C),sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_C)",39);
+ }
+ /*@ assert \valid((int *)_D); */
+ {
+ int __e_acsl_valid_3;
+ __e_acsl_valid_3 = __valid((void *)(_D),sizeof(int));
+ e_acsl_assert(__e_acsl_valid_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid((int *)_D)",40);
+ }
+ /*@ assert \valid(&_E); */
+ {
+ int __e_acsl_valid_4;
+ __e_acsl_valid_4 = __valid((void *)(& _E),sizeof(int));
+ e_acsl_assert(__e_acsl_valid_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_E)",41);
+ }
+ /*@ assert \valid(&_F); */
+ {
+ int __e_acsl_valid_5;
+ __e_acsl_valid_5 = __valid((void *)(& _F),sizeof(int));
+ e_acsl_assert(__e_acsl_valid_5,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_F)",42);
+ }
+ /*@ assert _E ≡ 44; */
+ e_acsl_assert(_E == 44,(char *)"Assertion",(char *)"main",
+ (char *)"_E == 44",43);
+ /*@ assert \valid(&_G); */
+ {
+ int __e_acsl_valid_6;
+ __e_acsl_valid_6 = __valid((void *)(& _G),sizeof(struct ST [2]));
+ e_acsl_assert(__e_acsl_valid_6,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_G)",44);
+ }
+ /*@ assert _G[0].num ≡ 99; */
+ e_acsl_assert(_G[0].num == 99,(char *)"Assertion",(char *)"main",
+ (char *)"_G[0].num == 99",45);
+ __retres = 0;
+ __delete_block((void *)(_G));
+ __delete_block((void *)(& _E));
+ __delete_block((void *)(_D));
+ __delete_block((void *)(& _C));
+ __delete_block((void *)(& _B));
+ __delete_block((void *)(_A));
+ __delete_block((void *)(& _F));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers2.c
new file mode 100644
index 0000000000000000000000000000000000000000..006f7b2a248b4d8f1c819547710bd269f940c1d1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers2.c
@@ -0,0 +1,288 @@
+/* Generated by Frama-C */
+char *__e_acsl_literal_string_3;
+char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_2;
+char *__e_acsl_literal_string_4;
+char *__e_acsl_literal_string_5;
+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 long size_t;
+struct ST {
+ char *str ;
+ int num ;
+};
+/*@ 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__, __FRAMA_C_MODEL__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */
+
+/*@
+axiomatic dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ 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_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(x);
+ assigns *x;
+ assigns *x \from *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
+ assigns \result;
+ assigns \result \from *z1, *z2;
+ */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
+/*@ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1)); */
+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 __full_init(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+ ensures
+ \result ≡ 1 ⇒ \valid_read((char *)\old(ptr)+(0 .. \old(size)-1));
+ assigns \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+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 \result;
+ assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+ size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+ assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int _F;
+
+char *_A[2] = {(char *)"XX", (char *)"YY"};
+char *_B = (char *)"ZZ";
+char *_C;
+int _D[2] = {44, 88};
+int _E = 44;
+int _F = 9;
+struct ST _G[2] =
+ {{.str = (char *)"First", .num = 99}, {.str = (char *)"Second", .num = 147}};
+void __e_acsl_memory_init(void)
+{
+ __e_acsl_literal_string_3 = "ZZ";
+ __store_block((void *)__e_acsl_literal_string_3,sizeof("ZZ"));
+ __full_init((void *)__e_acsl_literal_string_3);
+ __literal_string((void *)__e_acsl_literal_string_3);
+ __e_acsl_literal_string = "YY";
+ __store_block((void *)__e_acsl_literal_string,sizeof("YY"));
+ __full_init((void *)__e_acsl_literal_string);
+ __literal_string((void *)__e_acsl_literal_string);
+ __e_acsl_literal_string_2 = "XX";
+ __store_block((void *)__e_acsl_literal_string_2,sizeof("XX"));
+ __full_init((void *)__e_acsl_literal_string_2);
+ __literal_string((void *)__e_acsl_literal_string_2);
+ __e_acsl_literal_string_4 = "Second";
+ __store_block((void *)__e_acsl_literal_string_4,sizeof("Second"));
+ __full_init((void *)__e_acsl_literal_string_4);
+ __literal_string((void *)__e_acsl_literal_string_4);
+ __e_acsl_literal_string_5 = "First";
+ __store_block((void *)__e_acsl_literal_string_5,sizeof("First"));
+ __full_init((void *)__e_acsl_literal_string_5);
+ __literal_string((void *)__e_acsl_literal_string_5);
+ __store_block((void *)(_G),32UL);
+ __full_init((void *)(& _G));
+ __store_block((void *)(& _E),4UL);
+ __full_init((void *)(& _E));
+ __store_block((void *)(_D),8UL);
+ __full_init((void *)(& _D));
+ __store_block((void *)(& _C),8UL);
+ __full_init((void *)(& _C));
+ __store_block((void *)(& _B),8UL);
+ __full_init((void *)(& _B));
+ __store_block((void *)(_A),16UL);
+ __full_init((void *)(& _A));
+ __store_block((void *)(& _F),4UL);
+ __full_init((void *)(& _F));
+ return;
+}
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init();
+ /*@ assert \valid((char **)_A); */
+ {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)(_A),sizeof(char *));
+ e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid((char **)_A)",35);
+ }
+ /*@ assert \valid_read(_A[0]); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(_A),sizeof(char *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid_read;
+ __e_acsl_valid_read = __valid_read((void *)_A[0],sizeof(char));
+ __e_acsl_and = __e_acsl_valid_read;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_A[0])",36);
+ }
+ /*@ assert \valid_read(_A[1]); */
+ {
+ int __e_acsl_initialized_2;
+ int __e_acsl_and_2;
+ __e_acsl_initialized_2 = __initialized((void *)(& _A[1]),sizeof(char *));
+ if (__e_acsl_initialized_2) {
+ int __e_acsl_valid_read_2;
+ __e_acsl_valid_read_2 = __valid_read((void *)_A[1],sizeof(char));
+ __e_acsl_and_2 = __e_acsl_valid_read_2;
+ }
+ else __e_acsl_and_2 = 0;
+ e_acsl_assert(__e_acsl_and_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_A[1])",37);
+ }
+ /*@ assert \valid_read(_B); */
+ {
+ int __e_acsl_valid_read_3;
+ __e_acsl_valid_read_3 = __valid_read((void *)_B,sizeof(char));
+ e_acsl_assert(__e_acsl_valid_read_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid_read(_B)",38);
+ }
+ /*@ assert \valid(&_C); */
+ {
+ int __e_acsl_valid_2;
+ __e_acsl_valid_2 = __valid((void *)(& _C),sizeof(char *));
+ e_acsl_assert(__e_acsl_valid_2,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_C)",39);
+ }
+ /*@ assert \valid((int *)_D); */
+ {
+ int __e_acsl_valid_3;
+ __e_acsl_valid_3 = __valid((void *)(_D),sizeof(int));
+ e_acsl_assert(__e_acsl_valid_3,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid((int *)_D)",40);
+ }
+ /*@ assert \valid(&_E); */
+ {
+ int __e_acsl_valid_4;
+ __e_acsl_valid_4 = __valid((void *)(& _E),sizeof(int));
+ e_acsl_assert(__e_acsl_valid_4,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_E)",41);
+ }
+ /*@ assert \valid(&_F); */
+ {
+ int __e_acsl_valid_5;
+ __e_acsl_valid_5 = __valid((void *)(& _F),sizeof(int));
+ e_acsl_assert(__e_acsl_valid_5,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_F)",42);
+ }
+ /*@ assert _E ≡ 44; */
+ {
+ mpz_t __e_acsl__E;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ __gmpz_init_set_si(__e_acsl__E,(long)_E);
+ __gmpz_init_set_si(__e_acsl,(long)44);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl__E),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
+ (char *)"_E == 44",43);
+ __gmpz_clear(__e_acsl__E);
+ __gmpz_clear(__e_acsl);
+ }
+ /*@ assert \valid(&_G); */
+ {
+ int __e_acsl_valid_6;
+ __e_acsl_valid_6 = __valid((void *)(& _G),sizeof(struct ST [2]));
+ e_acsl_assert(__e_acsl_valid_6,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(&_G)",44);
+ }
+ /*@ assert _G[0].num ≡ 99; */
+ {
+ mpz_t __e_acsl_2;
+ mpz_t __e_acsl_3;
+ int __e_acsl_eq_2;
+ __gmpz_init_set_si(__e_acsl_2,(long)_G[0].num);
+ __gmpz_init_set_si(__e_acsl_3,(long)99);
+ __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_2),
+ (__mpz_struct const *)(__e_acsl_3));
+ e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",(char *)"main",
+ (char *)"_G[0].num == 99",45);
+ __gmpz_clear(__e_acsl_2);
+ __gmpz_clear(__e_acsl_3);
+ }
+ __retres = 0;
+ __delete_block((void *)(_G));
+ __delete_block((void *)(& _E));
+ __delete_block((void *)(_D));
+ __delete_block((void *)(& _C));
+ __delete_block((void *)(& _B));
+ __delete_block((void *)(_A));
+ __delete_block((void *)(& _F));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+