diff --git a/src/plugins/e-acsl/tests/memory/memsize.c b/src/plugins/e-acsl/tests/memory/memsize.c
index c214b60ebd4dcbb33a07b64bf3fddf3e7aec9a8e..2260a306878d6dfd4943d73ccbddc6436c2ec2f5 100644
--- a/src/plugins/e-acsl/tests/memory/memsize.c
+++ b/src/plugins/e-acsl/tests/memory/memsize.c
@@ -1,5 +1,6 @@
-/* run.config
+/* run.config_ci
    COMMENT: Checking heap memory size
+   STDOPT: +"-eva-no-builtins-auto"
 */
 
 #include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
index 594eb809025228428f8d77a55c247c7157cab650..86b350d6bcd47ce810e3942357482c1a1697e052 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
@@ -40,6 +40,12 @@ extern int __e_acsl_sound_verdict;
  */
 int __gen_e_acsl_posix_memalign(void **memptr, size_t alignment, size_t size);
 
+/*@ assigns __e_acsl_heap_allocation_size, __e_acsl_heap_allocated_blocks;
+    assigns __e_acsl_heap_allocation_size
+      \from (indirect: alignment), size, __e_acsl_heap_allocation_size;
+    assigns __e_acsl_heap_allocated_blocks
+      \from (indirect: alignment), size, __e_acsl_heap_allocated_blocks;
+ */
 void *aligned_alloc(size_t alignment, size_t size);
 
 int main(int argc, char const **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index 134e80f8dafed2dc211d27d63cf0ed3076a9c401..d31fa69d2a5df24b8d9189086ba15157c57864a5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -11,73 +11,73 @@ int main(int argc, char **argv)
   char *a = malloc((unsigned long)7);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 7",
-                  "tests/memory/memsize.c",14);
+                  "tests/memory/memsize.c",15);
   /*@ assert __e_acsl_heap_allocation_size ≡ 7; */ ;
   char *b = malloc((unsigned long)14);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 21UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 21",
-                  "tests/memory/memsize.c",16);
+                  "tests/memory/memsize.c",17);
   /*@ assert __e_acsl_heap_allocation_size ≡ 21; */ ;
   free((void *)a);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 14",
-                  "tests/memory/memsize.c",20);
+                  "tests/memory/memsize.c",21);
   /*@ assert __e_acsl_heap_allocation_size ≡ 14; */ ;
   a = (char *)0;
   free((void *)a);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 14UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 14",
-                  "tests/memory/memsize.c",25);
+                  "tests/memory/memsize.c",26);
   /*@ assert __e_acsl_heap_allocation_size ≡ 14; */ ;
   b = (char *)realloc((void *)b,(unsigned long)9);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 9UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 9",
-                  "tests/memory/memsize.c",29);
+                  "tests/memory/memsize.c",30);
   /*@ assert __e_acsl_heap_allocation_size ≡ 9; */ ;
   b = (char *)realloc((void *)b,(unsigned long)18);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 18UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 18",
-                  "tests/memory/memsize.c",33);
+                  "tests/memory/memsize.c",34);
   /*@ assert __e_acsl_heap_allocation_size ≡ 18; */ ;
   b = (char *)realloc((void *)b,(unsigned long)0);
   b = (char *)0;
   __e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 0",
-                  "tests/memory/memsize.c",38);
+                  "tests/memory/memsize.c",39);
   /*@ assert __e_acsl_heap_allocation_size ≡ 0; */ ;
   b = (char *)realloc((void *)b,(unsigned long)8);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 8UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 8",
-                  "tests/memory/memsize.c",42);
+                  "tests/memory/memsize.c",43);
   /*@ assert __e_acsl_heap_allocation_size ≡ 8; */ ;
   b = (char *)realloc((void *)0,(unsigned long)8);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 16",
-                  "tests/memory/memsize.c",46);
+                  "tests/memory/memsize.c",47);
   /*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
   b = (char *)realloc((void *)0,18446744073709551615UL);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 16",
-                  "tests/memory/memsize.c",50);
+                  "tests/memory/memsize.c",51);
   /*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
   __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
-                  "tests/memory/memsize.c",51);
+                  "tests/memory/memsize.c",52);
   /*@ assert b ≡ (char *)0; */ ;
   b = (char *)calloc(18446744073709551615UL,18446744073709551615UL);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 16",
-                  "tests/memory/memsize.c",55);
+                  "tests/memory/memsize.c",56);
   /*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
   __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
-                  "tests/memory/memsize.c",56);
+                  "tests/memory/memsize.c",57);
   /*@ assert b ≡ (char *)0; */ ;
   b = (char *)malloc(18446744073709551615UL);
   __e_acsl_assert(__e_acsl_heap_allocation_size == 16UL,"Assertion","main",
                   "__e_acsl_heap_allocation_size == 16",
-                  "tests/memory/memsize.c",60);
+                  "tests/memory/memsize.c",61);
   /*@ assert __e_acsl_heap_allocation_size ≡ 16; */ ;
   __e_acsl_assert(b == (char *)0,"Assertion","main","b == (char *)0",
-                  "tests/memory/memsize.c",61);
+                  "tests/memory/memsize.c",62);
   /*@ assert b ≡ (char *)0; */ ;
   __retres = 0;
   __e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
index 2db55f248cb6caa7f38d1c46c8c93f5bdc964f5e..68e3cc47739f873c790ec413966607107df9a811 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
@@ -1,7 +1,66 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/memsize.c:14: Warning: 
+[eva] tests/memory/memsize.c:14: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:15: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:15: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:16: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:17: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:17: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:20: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:20: Warning: 
+  function free: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:21: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:21: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:25: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:26: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:26: Warning: assertion got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:452: Warning: 
+  no 'assigns \result \from ...' clause specified for function realloc
+[eva] tests/memory/memsize.c:29: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:29: Warning: 
+  function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:30: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:30: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:33: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:33: Warning: 
+  function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:34: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:34: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:37: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:37: Warning: 
+  function realloc: precondition 'freeable' got status unknown.
+[eva:alarm] tests/memory/memsize.c:39: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:39: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:42: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:43: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:43: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:46: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:47: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:47: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:50: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:51: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:51: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:52: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva] FRAMAC_SHARE/libc/stdlib.h:385: Warning: 
+  no 'assigns \result \from ...' clause specified for function calloc
+[eva] tests/memory/memsize.c:55: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:56: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:56: Warning: assertion got status unknown.
+[eva] tests/memory/memsize.c:60: Warning: ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/memsize.c:61: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/memsize.c:61: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:62: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/memsize.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/memory/memsize.c:16: Warning: 
-  function __e_acsl_assert: precondition got status invalid.