diff --git a/src/plugins/e-acsl/.gitlab-ci.yml b/src/plugins/e-acsl/.gitlab-ci.yml
new file mode 100644
index 0000000000000000000000000000000000000000..a444867e757a58cdce3e68b625614fdcd9bf9a2b
--- /dev/null
+++ b/src/plugins/e-acsl/.gitlab-ci.yml
@@ -0,0 +1,6 @@
+Tests:
+ script:
+ - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --rootfs 1 --frama-c master --E-ACSL $(git rev-parse HEAD) E-ACSL
+ tags:
+ except:
+ - tags
\ No newline at end of file
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 5530d826bccb14f995d230f11bdcf06ecdb01f9a..5f2eeba808130e5898056e194369e98dd2d15c78 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2015/08/12] Fix bug #1817 about incloorect initialization of
+ literal strings in global in arrays with compound initializers.
-* E-ACSL [2015/11/06] Fix a crash occuring when using a recent libc
while GMP headers provided by E-ACSL are used.
diff --git a/src/plugins/e-acsl/tests/bts/bts1718.i b/src/plugins/e-acsl/tests/bts/bts1718.i
new file mode 100644
index 0000000000000000000000000000000000000000..0b13703f0a8a510aac910fe717bd0d90f897f230
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/bts1718.i
@@ -0,0 +1,19 @@
+/* run.config
+ COMMENT: bts #1718, issue regarding incorrect initialization of literal strings in global arrays with compound initializers
+ STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
+ EXECNOW: LOG gen_bts1718.c BIN gen_bts1718.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1718.c > /dev/null && ./gcc_bts.sh bts1718
+ EXECNOW: LOG gen_bts17182.c BIN gen_bts17182.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1718.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17182.c > /dev/null && ./gcc_bts.sh bts17182
+*/
+
+int main(void) {
+ int a = 10, *p;
+ goto lbl_1;
+
+ lbl_2:
+ /*@ assert \valid(p); */
+ return 0;
+
+ lbl_1:
+ p = &a;
+ goto lbl_2;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a4617af6a665293e6d96627c8dac6997f06fa11a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
@@ -0,0 +1,22 @@
+[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 ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/bts/bts1718.i:13:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[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.
+[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/bts/oracle/bts1718.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a4617af6a665293e6d96627c8dac6997f06fa11a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
@@ -0,0 +1,22 @@
+[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 ∈ [--..--]
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/bts/bts1718.i:13:[value] Assertion got status valid.
+[value] using specification for function __initialized
+[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.
+[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/bts/oracle/bts1837.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
index efd924c556296cc37747d56a5a72f0bae13e0177..cefeb276e61b9907bda3ef2e074dc0f0f3f7085d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
@@ -10,7 +10,7 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- S ∈ {0}
+ S ∈ {{ "foo" }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
__e_acsl_literal_string_3 ∈ {0}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
index efd924c556296cc37747d56a5a72f0bae13e0177..cefeb276e61b9907bda3ef2e074dc0f0f3f7085d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
@@ -10,7 +10,7 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- S ∈ {0}
+ S ∈ {{ "foo" }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
__e_acsl_literal_string_3 ∈ {0}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
new file mode 100644
index 0000000000000000000000000000000000000000..bfd83983a86a46b25cb49bae40eb908e42a9d0cb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -0,0 +1,111 @@
+/* Generated by Frama-C */
+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 int size_t;
+/*@ 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);
+
+/*@ 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 ⇒ \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 main(void)
+{
+ int __retres;
+ int a;
+ int *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& a));
+ a = 10;
+ goto lbl_1;
+ lbl_2:
+ /*@ assert \valid(p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)p,sizeof(int));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ goto return_label;
+ lbl_1: __full_init((void *)(& p));
+ p = & a;
+ goto lbl_2;
+ return_label:
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
new file mode 100644
index 0000000000000000000000000000000000000000..bfd83983a86a46b25cb49bae40eb908e42a9d0cb
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
@@ -0,0 +1,111 @@
+/* Generated by Frama-C */
+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 int size_t;
+/*@ 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);
+
+/*@ 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 ⇒ \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 main(void)
+{
+ int __retres;
+ int a;
+ int *p;
+ __store_block((void *)(& p),4U);
+ __store_block((void *)(& a),4U);
+ __full_init((void *)(& a));
+ a = 10;
+ goto lbl_1;
+ lbl_2:
+ /*@ assert \valid(p); */
+ {
+ int __e_acsl_initialized;
+ int __e_acsl_and;
+ __e_acsl_initialized = __initialized((void *)(& p),sizeof(int *));
+ if (__e_acsl_initialized) {
+ int __e_acsl_valid;
+ __e_acsl_valid = __valid((void *)p,sizeof(int));
+ __e_acsl_and = __e_acsl_valid;
+ }
+ else __e_acsl_and = 0;
+ e_acsl_assert(__e_acsl_and,(char *)"Assertion",(char *)"main",
+ (char *)"\\valid(p)",13);
+ }
+ __retres = 0;
+ goto return_label;
+ lbl_1: __full_init((void *)(& p));
+ p = & a;
+ goto lbl_2;
+ return_label:
+ __delete_block((void *)(& p));
+ __delete_block((void *)(& a));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 918ee7158336f8488f8767940f26c1ccd6a6c5f7..32445cb1f02704a681cefc0a633a3b5df006e254 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -86,7 +86,7 @@ extern size_t __memory_size;
predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
-char *S;
+char *S = (char *)"foo";
int f(void)
{
int __retres;
@@ -155,7 +155,6 @@ void __e_acsl_memory_init(void)
__literal_string((void *)__e_acsl_literal_string_2);
__store_block((void *)(& S),4U);
__full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string;
return;
}
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;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 5cbdd9a0e2b10458db2c4729b715aa3bd26d603d..ec689d560787bfd68d91ecffbbb85fc06b802764 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -89,7 +89,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
int main(void);
-char *T;
+char *T = (char *)"bar";
int G = 0;
void f(void)
{
@@ -106,8 +106,8 @@ void f(void)
return;
}
-char *S;
-char *S2;
+char *S = (char *)"foo";
+char *S2 = (char *)"foo2";
int IDX = 1;
int G2 = 2;
char *U = (char *)"baz";
@@ -131,13 +131,10 @@ void __e_acsl_memory_init(void)
__literal_string((void *)__e_acsl_literal_string_2);
__store_block((void *)(& S2),4U);
__full_init((void *)(& S2));
- S2 = (char *)__e_acsl_literal_string_4;
__store_block((void *)(& S),4U);
__full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string_3;
__store_block((void *)(& T),4U);
__full_init((void *)(& T));
- T = (char *)__e_acsl_literal_string_2;
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index d5bb4999c2dc6591705bfcf661b341809840aa94..97cb30890d153325e4c7dbc38086c731c0bd5b83 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -112,7 +112,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/
int main(void);
-char *T;
+char *T = (char *)"bar";
int G = 0;
void f(void)
{
@@ -134,8 +134,8 @@ void f(void)
return;
}
-char *S;
-char *S2;
+char *S = (char *)"foo";
+char *S2 = (char *)"foo2";
int IDX = 1;
int G2 = 2;
char *U = (char *)"baz";
@@ -159,13 +159,10 @@ void __e_acsl_memory_init(void)
__literal_string((void *)__e_acsl_literal_string_2);
__store_block((void *)(& S2),4U);
__full_init((void *)(& S2));
- S2 = (char *)__e_acsl_literal_string_4;
__store_block((void *)(& S),4U);
__full_init((void *)(& S));
- S = (char *)__e_acsl_literal_string_3;
__store_block((void *)(& T),4U);
__full_init((void *)(& T));
- T = (char *)__e_acsl_literal_string_2;
return;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
index 076a517b7e7e4ec7e44ac0a41bcfc2bdaf065d84..c04d9a8f696904fa8df6921de8706b24764cdf10 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
@@ -10,10 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- T ∈ {0}
+ T ∈ {{ "bar" }}
G ∈ {0}
- S ∈ {0}
- S2 ∈ {0}
+ S ∈ {{ "foo" }}
+ S2 ∈ {{ "foo2" }}
IDX ∈ {1}
G2 ∈ {2}
U ∈ {{ "baz" }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 7f69a2e063cfbc0fe4d453055ab4cd0de56c20b8..dcdcf9a030ef2a43fcafc5365d2b28e72ff0bb33 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -10,10 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- T ∈ {0}
+ T ∈ {{ "bar" }}
G ∈ {0}
- S ∈ {0}
- S2 ∈ {0}
+ S ∈ {{ "foo" }}
+ S2 ∈ {{ "foo2" }}
IDX ∈ {1}
G2 ∈ {2}
U ∈ {{ "baz" }}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index eb0f074bc8d71860e1dc617842b9ee07e7c5b2e9..8bcb9ad95a5cdb8d91b5429992cedfadc20eb5b7 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -83,10 +83,23 @@ class e_acsl_visitor prj generate = object (self)
[None] while the global corresponding to this fundec has not been
visited *)
- val mutable keep_initializer = None
+ val mutable is_initializer = false
+ (* Global flag set to [true] if a currently visited node
+ belongs to a global initializer and set to [false] otherwise *)
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
- (* keys belong to the original project while values belong to the new one *)
+ (* Hashtable mapping global variables (as Cil_type.varinfo) to their
+ initializers aiming to capture memory allocated by global variable
+ declarations and initilisation. At runtime the memory blocks corresponding
+ to space occupied by global are recorded via a call to
+ [__e_acsl_memory_init] instrumented before (almost) anything else in the
+ [main] function. Each variable stored by [global_vars] will be handled in
+ the body of [__e_acsl_memory_init] as follows:
+ __store_block(...); // Record a memory block used by the variable
+ __full_init(...); // ... and mark it as initialized memory
+
+ NOTE: In [global_vars] keys belong to the original project while values
+ belong to the new one *)
method private reset_env () =
function_env := Env.empty (self :> Visitor.frama_c_visitor)
@@ -131,6 +144,11 @@ class e_acsl_visitor prj generate = object (self)
Varinfo.Hashtbl.fold_sorted
(fun old_vi i (stmts, env) ->
let new_vi = Cil.get_varinfo self#behavior old_vi in
+ (* [model] creates an initialization statement
+ of the form [__full_init(...)]) for every global
+ variable which needs to be tracked and is not a Frama-C
+ builtin. Further the statement is appended to the provided
+ list of statements ([blk]) *)
let model blk =
if Mmodel_analysis.must_model_vi old_vi then
let blk =
@@ -148,12 +166,7 @@ class e_acsl_visitor prj generate = object (self)
| None -> model stmts, env
| Some (CompoundInit _) -> assert false
| Some (SingleInit e) ->
- let e, env = self#literal_string env e in
- let stmt =
- Cil.mkStmtOneInstr ~valid_sid:true
- (Set(Cil.var new_vi, e, e.eloc))
- in
- model (stmt :: stmts), env)
+ let _, env = self#literal_string env e in stmts, env)
global_vars
([ return ], env)
in
@@ -171,6 +184,7 @@ class e_acsl_visitor prj generate = object (self)
:: stmts)
stmts
in
+ (* Create a new code block with generated statements *)
let (b, env), stmts = match stmts with
| [] -> assert false
| stmt :: stmts ->
@@ -179,14 +193,19 @@ class e_acsl_visitor prj generate = object (self)
function_env := env;
let stmts = Cil.mkStmt ~valid_sid:true (Block b) :: stmts in
let blk = Cil.mkBlock stmts in
+ (* Create [__e_acsl_memory_init] function with definition
+ for initialization of global variables *)
let fname = "__e_acsl_memory_init" in
- let vi =
+ let vi =
Cil.makeGlobalVar ~source:true
fname
(TFun(Cil.voidType, Some [], false, []))
in
vi.vdefined <- true;
+ (* There is no contract associated with the function *)
let spec = Cil.empty_funspec () in
+ (* Create function definition which has the list of the
+ * generated initialization statements *)
let fundec =
{ svar = vi;
sformals = [];
@@ -199,6 +218,7 @@ class e_acsl_visitor prj generate = object (self)
in
self#add_generated_variables_in_function fundec;
let fct = Definition(fundec, Location.unknown) in
+ (* Create and register [__e_acsl_memory_init] as kernel function *)
let kf =
{ fundec = fct; return_stmt = Some return; spec = spec }
in
@@ -210,11 +230,14 @@ class e_acsl_visitor prj generate = object (self)
match main_fct with
| Some main ->
let exp = Cil.evar ~loc:Location.unknown vi in
+ (* Create [__e_acsl_memory_init();] call *)
let stmt =
Cil.mkStmtOneInstr ~valid_sid:true
(Call(None, exp, [], Location.unknown))
in
vi.vreferenced <- true;
+ (* Add [__e_acsl_memory_init();] call as the first statement
+ to the [main] function *)
main.sbody.bstmts <- stmt :: main.sbody.bstmts;
let new_globals =
List.fold_right
@@ -296,18 +319,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if generate then Cil.JustCopy else Cil.SkipChildren
| g ->
let do_it = function
- | GVar(vi, i, _) ->
- vi.vghost <- false;
- (* remove initializers on need *)
- if Mmodel_analysis.old_must_model_vi self#behavior vi then begin
- try
- let old_vi = Cil.get_original_varinfo self#behavior vi in
- match Varinfo.Hashtbl.find global_vars old_vi with
- | None -> ()
- | Some _ -> i.init <- None
- with Not_found ->
- assert false
- end
+ | GVar(vi, _, _) ->
+ vi.vghost <- false; ()
| GFun({ svar = vi } as fundec, _) ->
vi.vghost <- false;
(* remember that we have to remove the main later (see method
@@ -324,22 +337,31 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
(match g with
| GVar(vi, _, _) | GVarDecl(vi, _) ->
+ (* Make a unique mapping for each global variable omitting initializers.
+ Initializers (used to capture literal strings) are added to
+ [global_vars] via the [vinit] visitor method (see comments below). *)
Varinfo.Hashtbl.replace global_vars vi None
| _ -> ());
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
- method !vinit vi _off _i =
+ (* Add mappings from global variables to their initializers to [global_vars].
+ Note that the below function captures only [SingleInit]s. All compound
+ initializers (which contain single ones) are unrapped and thrown away. *)
+ method !vinit vi _off _i =
if generate then
if Mmodel_analysis.must_model_vi vi then begin
- keep_initializer <- Some true;
+ is_initializer <- true;
Cil.DoChildrenPost
- (fun i ->
- (match keep_initializer with
- | Some false -> Varinfo.Hashtbl.replace global_vars vi (Some i)
- | Some true | None -> ());
- keep_initializer <- None;
- i)
+ (fun i ->
+ (match is_initializer with
+ (* Note the use of [add] instead [replace]. This is because a
+ single variable can be associated with multiple initializers
+ and all of them need to be captured. *)
+ | true -> Varinfo.Hashtbl.add global_vars vi (Some i)
+ | false-> ());
+ is_initializer <- false;
+ i)
end else
Cil.JustCopy
else
@@ -553,10 +575,15 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let loc = Stmt.loc stmt in
let delete_stmts =
Varinfo.Hashtbl.fold_sorted
- (fun old_vi _ acc ->
+ (fun old_vi i acc ->
if Mmodel_analysis.must_model_vi old_vi then
let new_vi = Cil.get_varinfo self#behavior old_vi in
- Misc.mk_delete_stmt new_vi :: acc
+ (* Since there are multiple entries for same variables
+ do delete only variables without initializers, this
+ ensures that each variable is released once only *)
+ (match i with
+ | None -> Misc.mk_delete_stmt new_vi :: acc
+ | Some _ -> acc)
else
acc)
global_vars
@@ -693,21 +720,20 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
if generate then Cil.DoChildrenPost handle_memory else Cil.DoChildren
- method !vexpr exp =
- if generate then
- match keep_initializer with
- | Some false -> Cil.JustCopy
- | Some true ->
- let keep = match exp.enode with Const(CStr _) -> false | _ -> true in
- keep_initializer <- Some keep;
- if keep then Cil.DoChildren else Cil.JustCopy
- | None ->
- Cil.DoChildrenPost
- (fun e ->
- let e, env = self#literal_string !function_env e in
- function_env := env;
- e)
- else
+ (* Processing expressions for the purpose of replacing literal strings found
+ in the code with variables generated by E-ACSL. *)
+ method !vexpr _ =
+ if generate then begin
+ match is_initializer with
+ (* Do not touch global initializers because they accept only constants *)
+ | true -> Cil.DoChildren
+ (* Replace literal strings elsewhere *)
+ | false -> Cil.DoChildrenPost
+ (fun e ->
+ let e, env = self#literal_string !function_env e in
+ function_env := env;
+ e)
+ end else
Cil.SkipChildren
method !vterm _ =
@@ -736,7 +762,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Literal_strings.reset ();
self#reset_env ();
Translate.set_original_project (Project.current ())
-
end
let do_visit ?(prj=Project.current ()) generate =