diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
index 7a579dc32d3c6c660a14d042948f8dc16e2191e1..0f80a70efb16cce469924cd3c6bd384fcabe2ec0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
@@ -4,11 +4,21 @@
 #include "stdlib.h"
 extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
+extern size_t __e_acsl_heap_allocation_size;
+
 int main(void)
 {
   int __retres;
   __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,1,"Assertion","main",
+                  "__e_acsl_heap_allocation_size == 0",
+                  "tests/memory/init_function.c",16);
+  /*@ assert __e_acsl_heap_allocation_size ≡ 0; */ ;
   char *a = malloc((unsigned long)7);
+  __e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,1,"Assertion","main",
+                  "__e_acsl_heap_allocation_size == 7",
+                  "tests/memory/init_function.c",18);
+  /*@ assert __e_acsl_heap_allocation_size ≡ 7; */ ;
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
index efd026311297e55d8fefb674326118e6ece88624..f8f3e0f93f7a84a7f02c488b6a9b4443fbea3b33 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
@@ -1,2 +1,12 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/init_function.c:16: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/init_function.c:16: Warning: 
+  assertion got status unknown.
+[eva] tests/memory/init_function.c:17: Warning: 
+  ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/init_function.c:18: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/init_function.c:18: Warning: 
+  assertion got status unknown.