- Added a test case for processing of global initializers

- Updated CI configuration

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

src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c

+/* 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;
+}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle

+[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

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle

+[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

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c

+/* 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;
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers2.c

+/* 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;
+}
+
+