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 ce014ccd5a215298c2a3c9c4ae1dd555b8370ba5..302c3300239726a0a820d3994caa18b325329cab 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 6d1267a9d469ab70610f0a1780379c547b1ee5b9..05cb29087444c1b343832cdd7fa8b0accfb7ec37 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 17548f9748faf1e134e95e69f22f699a9c562c0a..7590860f25d34a639c82fa914f7aacc7d1c35d63 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 bf0bad741ae717ff9c570e6930b0c44fc353233d..831b85625355f051f00237befc9132fb00357235 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 6e144ae4c6ba74051c36cd4a818a48937df3e59a..411b78b847c5889bc91a18f398a327d0877231ea 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 0e557f01a22c86fd63f61598bb2181e7e6400661..b37cd30f8605e2668de7a89d16abdb4fc23545dd 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 1c9ad38e4f6aa5495d9d57c4e5b45b888420a9fb..b2e92bae8574da15979cac3295a25ea7f1c9e759 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 51c73767c0b7b137687547f1d062bee5fefee43d..715376d7d149aeb7e0dc2247bdae7c978d042c10 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 9c3148f7c7daf97ce7dbb6557a042de93323196a..dd106c8ef5abb5e534800df0a7fcd2a806949279 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 339b5444392d122902f45165008a06b6b277ab30..46a3c991ac23ca885e72df47211214f1e517ce96 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 530fd07a576621e3e848f48b733a251f93775932..a3079f4d26dd29e1b0ad0d563ea2e9baebdb1167 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 4454b3561d1e508bf95574e599693cd2327b0878..1cf38271a56e4968444983a2d9b855e0aa61fde9 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 37e2b743a3b3d653efd0b9f27ed72398565477eb..595ba4cc19bd2974bc24c29402398a56ffdb1910 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 539675b4d2eff4a14e49ab7e65298d9e0c7f0b8e..d36a9c6b6d6735560b3529d3930ae5f7178276a6 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 7842dfe4d5c932fdc1bd795fef7683dcca97dab8..e8121408525e175d99858297b8b28312abbd9a6d 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 e1dd8c915e95a4371123f8a9fea44241dca3d4d8..282b13219b29409508d7de3340269bfb30d42688 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 d4dbd0a6d7a3c007c6c74fe4266fb22c384249ff..74c2e1316d22df27fc213a024c580f3c5acfbb89 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 73e543642d222b1de63b121805a798dcdac30140..5241992159c1504d20aa3a86848def181829a23e 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 0a158b23d0d7754da379462420581b44b71dadb4..6ee57dffc305a91a1b9e190cda79a9815d757023 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 0cfd5c18cfe697c4e0ff608cb3258fbee6e501e8..c552cc84f1800f562ad34384fef8e7a64279ffc3 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 54f71bd22459331445f3abd3c869e19d97bb293c..640b3b3af1e52b03724d512c0c3648700b8caf78 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 63c54b491ae603e40c4b95561aea382e19e5c40a..165aaaf9940f535f75fb586217561f17130a17d8 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 9c3148f7c7daf97ce7dbb6557a042de93323196a..dd106c8ef5abb5e534800df0a7fcd2a806949279 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 e693a600c6130975a9383d5309185bbbd962dfc0..a760a3c8324d95dea91efa320779a3063bbbb974 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 14ecebbb2ed6deeef42e3efcae7ab999563d3ba9..1eb771c7ae389b5c3cf508b135676513c9891834 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 d2f07efc1d2ea9c95f5fc44008831978b1e86a2d..9c07803917ff166930e4aaab947b1ff10ebb2196 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 f1c3f7afb6dfb98de5654eed151989e3ef9098e8..291fb0d05552c82f665cb5feb9008df5f8e35393 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 2a91bd6f06402b214e3e4706b901c0d21474d6d8..74f7527423e9b9455ad69b125845b482d2d3caa5 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 6fd208997af1ee105c57e1c393f0ce0edab7f2b1..71d59a04e1783ac482a8725a2a34e6f0728e508a 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 61bd1c83fe81f284b181cb3aa5e1e388848b8b81..d07486a7c52f9985bad8f933682a9a5f2de618e4 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 411d9156a849d35841f3248b168f7579169b4910..2a96ff1a633fd904c18f678d6b40cb5b82688b87 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 64f20c885816b1144ee810e16013b50121a58179..dc9943a1413309390b49f852002716b055bc31da 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 3d0ab3670f7428dddcc2d911ed302fcae61df258..e0791ac88cb29a81155f515ee9b2d1b302acc2cd 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 7edd52d481debfbb6f44fcd1337980018761205f..370901be5960d198d2ec5ebfeced43dd3b23b1bf 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 106da5a584157f745b8e9098899dc533a84e5e66..69110b0e12ab26b167e8d0485ef2bd39a6f26eaa 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 43bfd7919feb6b3d70e6b1695c7607ccae49ddc0..e1b1662641a9f65ac6fc4eac0b3d8d57d9835398 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 2fc9e9b524e2e29ae51e21adf960c3041b9c3514..50b033f93b4653de09658914eac0a4c55f7ef7e5 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",