From f88e29cec2b098fc159c41da12d05b6b3200532d Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 18 May 2017 09:32:51 +0200
Subject: [PATCH] Test oracles update

---
 src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c                | 1 +
 src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c                | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle           | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle           | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle           | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle           | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle            | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle            | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle      | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle      | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c                  | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c                 | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c             | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c            | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c       | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c      | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_not.c                    | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c                   | 1 +
 .../e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle        | 1 +
 .../e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle        | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle        | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle        | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle             | 1 +
 src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle             | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_false.c              | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c  | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c       | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c               | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c      | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c  | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_null.c               | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c    | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_result.c             | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c             | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c      | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_true.c               | 1 +
 src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c            | 1 +
 37 files changed, 37 insertions(+)

diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index ce014ccd5a2..302c3300239 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -21,6 +21,7 @@ int fact(int n)
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = __gen_e_acsl_fact(5);
   /*@ assert x ≡ 120; */
   __e_acsl_assert(x == 120,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
index 6d1267a9d46..05cb2908744 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -4,6 +4,7 @@ long A = (long)0;
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert A + (long)((long)(3 * A) - 1) ≡ -1; */
   {
     __e_acsl_mpz_t __gen_e_acsl_A;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index 17548f9748f..7590860f25d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_assert
 [value] using specification for function __gmpz_init_set_str
 [value] using specification for function __gmpz_init_set_si
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
index bf0bad741ae..831b8562535 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_neg
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
index 6e144ae4c6b..411b78b847c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
@@ -15,6 +15,7 @@
   __e_acsl_heap_allocation_size ∈ [--..--]
   T1[0..2] ∈ {0}
   T2[0..3] ∈ {0}
+[value] using specification for function __e_acsl_memory_init
 tests/gmp/array.i:10:[value] entering loop for the first time
 tests/gmp/array.i:11:[value] entering loop for the first time
 tests/gmp/array.i:13:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
index 0e557f01a22..b37cd30f860 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
@@ -15,6 +15,7 @@
   __e_acsl_heap_allocation_size ∈ [--..--]
   T1[0..2] ∈ {0}
   T2[0..3] ∈ {0}
+[value] using specification for function __e_acsl_memory_init
 tests/gmp/array.i:10:[value] entering loop for the first time
 tests/gmp/array.i:11:[value] entering loop for the first time
 tests/gmp/array.i:13:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index 1c9ad38e4f6..b2e92bae857 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
@@ -15,6 +15,7 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_assert
 [value] user error: type long double not implemented. Using double instead
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 51c73767c0b..715376d7d14 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -15,6 +15,7 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_get_si
 [value] using specification for function __gmpz_cmp
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
index 9c3148f7c7d..dd106c8ef5a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
@@ -13,5 +13,6 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_assert
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index 339b5444392..46a3c991ac2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index 530fd07a576..a3079f4d26d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = -3;
   int y = 2;
   long z = 2L;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
index 4454b3561d1..1cf38271a56 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = -3;
   int y = 2;
   long z = 2L;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
index 37e2b743a3b..595ba4cc19b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   /*@ assert x < y; */
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
index 539675b4d2e..d36a9c6b6d6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   /*@ assert x < y; */
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
index 7842dfe4d5c..e8121408525 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
@@ -4,6 +4,7 @@ int main(void)
 {
   int __retres;
   int x;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert 0 ≡ 0; */
   __e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"main",(char *)"0 == 0",
                   6);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
index e1dd8c915e9..282b13219b2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
@@ -4,6 +4,7 @@ int main(void)
 {
   int __retres;
   int x;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert 0 ≡ 0; */
   {
     __e_acsl_mpz_t __gen_e_acsl_;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
index d4dbd0a6d7a..74c2e1316d2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   /*@ assert x ≡ 0; */
   __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
index 73e543642d2..5241992159c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   /*@ assert x ≡ 0; */
   {
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
index 0a158b23d0d..6ee57dffc30 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_assert
 [value] using specification for function __gmpz_init_set_str
 [value] using specification for function __gmpz_cmp
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index 0cfd5c18cfe..c552cc84f18 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 54f71bd2245..640b3b3af1e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 tests/gmp/longlong.i:9:[value] user error: recursive call during value analysis
                     of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
                     the call has no effect. The analysis will be unsound.]
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 63c54b491ae..165aaaf9940 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 tests/gmp/longlong.i:9:[value] user error: recursive call during value analysis
                     of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
                     the call has no effect. The analysis will be unsound.]
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
index 9c3148f7c7d..dd106c8ef5a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
@@ -13,5 +13,6 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __e_acsl_assert
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index e693a600c61..a760a3c8324 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
@@ -13,6 +13,7 @@
   __e_acsl_init ∈ [--..--]
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
+[value] using specification for function __e_acsl_memory_init
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
index 14ecebbb2ed..1eb771c7ae3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   if (x) 
     /*@ assert \false; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index d2f07efc1d2..9c07803917f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -172,6 +172,7 @@ void n(void)
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __gen_e_acsl_f();
   __gen_e_acsl_g();
   __gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index f1c3f7afb6d..291fb0d0555 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -8,6 +8,7 @@ int main(void);
 int __gen_e_acsl_main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   goto L1;
   L1:
   /*@ assert X ≡ 0; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
index 2a91bd6f064..74f7527423e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   /*@ assert x ≡ 0 ∧ y ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 6fd208997af..71d59a04e17 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -112,6 +112,7 @@ int main(void)
 {
   int __retres;
   int found;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int i = 0;
     while (i < 10) {
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
index 61bd1c83fe8..d07486a7c52 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   /*@ assert x < y; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
index 411d9156a84..2a96ff1a633 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert \null ≡ (void *)0; */
   __e_acsl_assert((void *)0 == (void *)0,(char *)"Assertion",(char *)"main",
                   (char *)"\\null == (void *)0",6);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
index 64f20c88581..dc9943a1413 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
@@ -7,6 +7,7 @@ enum bool {
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert 'c' ≡ 'c'; */
   __e_acsl_assert('c' == 'c',(char *)"Assertion",(char *)"main",
                   (char *)"\'c\' == \'c\'",10);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 3d0ab3670f7..e0791ac88cb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -34,6 +34,7 @@ int h(void)
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __gen_e_acsl_f(1);
   __gen_e_acsl_g(Y);
   __gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
index 7edd52d481d..370901be596 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   x ++;
   /*@ assert sizeof(int) ≡ sizeof(x); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 106da5a5841..69110b0e12a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 2;
   /*@ ensures x ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
index 43bfd7919fe..e1b1662641a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
@@ -3,6 +3,7 @@
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   x ++;
   /*@ assert \true; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
index 2fc9e9b524e..50b033f93b4 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
@@ -4,6 +4,7 @@ typedef unsigned char uint8;
 int main(void)
 {
   int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   uint8 x = (unsigned char)0;
   /*@ assert x ≡ 0; */
   __e_acsl_assert(x == 0,(char *)"Assertion",(char *)"main",(char *)"x == 0",
-- 
GitLab