From 9263dac86c97a6c1a77b1cb97782aea7130d6b63 Mon Sep 17 00:00:00 2001
From: Boris Yakobowski <boris.yakobowski@cea.fr>
Date: Mon, 18 Jan 2016 19:22:27 +0100
Subject: [PATCH] Update oracles w.r.t. Frama-C trunk
 (revamp-dynamic-allocation in Value)

---
 src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle     | 5 +++--
 src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle     | 5 +++--
 .../e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle     | 2 ++
 .../e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle     | 2 ++
 .../tests/e-acsl-runtime/oracle/linear_search.1.res.oracle   | 4 ++--
 .../e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle | 2 ++
 .../e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle | 2 ++
 .../e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle    | 5 +++--
 .../e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle    | 5 +++--
 .../tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle     | 5 +++--
 .../tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle     | 5 +++--
 .../e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle   | 5 +++--
 .../e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle   | 5 +++--
 13 files changed, 34 insertions(+), 18 deletions(-)

diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index 3d7d5310785..4773e0b0310 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -33,6 +33,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -48,8 +49,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index 97118b6b366..ff529ac753d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -25,6 +25,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -56,8 +57,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [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/call.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
index 8753ecac9cf..5b143f91676 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
@@ -25,9 +25,11 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [value] using specification for function __initialize
 tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
 [value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 4905c23b5c3..16b7e91901b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -21,9 +21,11 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [value] using specification for function __initialize
 tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
 [value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index feccbdb6ddb..17c82b48988 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -47,10 +47,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
index 87104bf62ca..2e97f3d935b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
@@ -25,6 +25,7 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -34,5 +35,6 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status 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 __initialize
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [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/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 50d22446a3c..7bcb0d29927 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -21,6 +21,7 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -30,5 +31,6 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status 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 __initialize
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [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/valid.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
index 91c1eca5dae..56aa4ebae24 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
@@ -40,6 +40,7 @@ tests/e-acsl-runtime/valid.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.
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -62,8 +63,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 0b1fb4930fb..e45b62a3e03 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -32,6 +32,7 @@ tests/e-acsl-runtime/valid.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.
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -54,8 +55,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
index 3abdd3f2958..e867ea1e46b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
@@ -37,6 +37,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status 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 valid.
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -51,8 +52,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 2fc23efb1a9..250286e8054 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -29,6 +29,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status 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 valid.
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -49,8 +50,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
index 2fa35f293f3..a4d6c584761 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
@@ -39,6 +39,7 @@ tests/e-acsl-runtime/vector.c:26:[value] Assertion got status 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 __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -51,8 +52,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [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/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 7d92075851e..449c89e8f5e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -31,6 +31,7 @@ tests/e-acsl-runtime/vector.c:26:[value] Assertion got status 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 __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -50,8 +51,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
-- 
GitLab