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 4e61f70824a6f00644b83b2c698a6f5f84566b49..3d7d53107850aa94a02d58c623c27e413be03c38 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
@@ -1,25 +1,25 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -34,8 +34,8 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 [value] using specification for function __initialize
 tests/bts/bts1399.c:24:[value] Assertion got status valid.
 [value] using specification for function __valid_read
@@ -43,13 +43,13 @@ tests/bts/bts1399.c:24:[value] Assertion got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __initialized
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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 41d37202e1a2364377ea88bf76532baf6918eb09..97118b6b366ae36a2de0da6a1e7fbba00070cc2e 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
@@ -1,6 +1,6 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -9,9 +9,9 @@ tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in beh
                   Ignoring annotation.
 tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 [value] using specification for function __initialize
 tests/bts/bts1399.c:24:[value] Assertion got status valid.
 [value] using specification for function __gmpz_init_set_ui
@@ -51,13 +51,13 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
 [value] using specification for function __initialized
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index 01d3b783fc56c1667b3c24cbe3aad8cdcc7912ef..871363e9725ef97786a5f99702d67492a9f25e99 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -150,7 +150,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4U);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
index 22adeadaf337860713521be9c19ff340196b9803..a348cbfc041a3708214b3710565446adcd11192d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
@@ -197,7 +197,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4U);
     __e_acsl_at = p != (void *)0;
     __free(p);
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 a46b458e10340fa024b8a191b7182e6c88e90a69..8753ecac9cfde95f929c1100ba135fa644f94f84 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
@@ -1,16 +1,16 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic functio
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 [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 27b861d05e49ba7d98d23b03c03006597f1a74c2..4905c23b5c3158687a6e34a1aae7e206eb81e639 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
@@ -1,5 +1,5 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -22,8 +22,8 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 [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/freeable.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
index 1fd71344f0524cd97e4576973179306832d58b1c..19e00442d13e9c982f0137f0ad040c8c22bddbbc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
@@ -1,25 +1,25 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
index 23809a9f749e448e651d882452f6846a0984d71e..516efe5ad151cf98f9125e5d09804f3fad5dbf94 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
@@ -1,6 +1,6 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -9,9 +9,9 @@ tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `assigns c
                   Ignoring annotation.
 tests/e-acsl-runtime/freeable.c:13:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
index 6663b24b9c945279c62ba5cb5c54f545fde4acb5..a0f898886369d8a7f219edc1c72767a2d653b952 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable.c
@@ -122,7 +122,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4UL);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c
index 057f2dc23acf663dcebd6e5a1899bcf53cb543d4..a2f9948ec8b2b8d915f8cddab60a0e6038fcae2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_freeable2.c
@@ -122,7 +122,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4UL);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index e12f0483d9db710f0cc76ed0ce3141ee44465f74..aeef2091f8929b09f759b0997fed1aa7b0980417 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -147,7 +147,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4UL);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index e12f0483d9db710f0cc76ed0ce3141ee44465f74..aeef2091f8929b09f759b0997fed1aa7b0980417 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -147,7 +147,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4UL);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 6a21c2b0fdc1a35bb3e2616691ed72acd2a5152f..9298497a1ff5db75741a00f45d3d769bf9f69bd1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -151,7 +151,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4U);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 02a86bbfc5b473640e690e0c1f6d812ebf5c79a5..74650f013f2d505d7b3962151d85a55cbacdb41d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -165,7 +165,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4U);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 29c90249380ed4acc9dcb95b33eb09625df49d6f..a26c08d266e91ab8a0978b18714f50348a7a2480 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -135,7 +135,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4U);
     __e_acsl_at = p != (void *)0;
     __free(p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index 26735ad303626362343dbb7766776a0023843194..43a45615da21bc5072da755ca69bfe80abdf789d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -158,7 +158,7 @@ void __e_acsl_free(void *p)
       __e_acsl_implies = __e_acsl_freeable;
     }
     e_acsl_assert(__e_acsl_implies,(char *)"Precondition",(char *)"free",
-                  (char *)"p != \\null ==> \\freeable(p)",177);
+                  (char *)"p != \\null ==> \\freeable(p)",178);
     __store_block((void *)(& __e_acsl_at),4U);
     __e_acsl_at = p != (void *)0;
     __free(p);
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 ecffec2a355f22edce828ece9c8aa96dae5f00bf..87104bf62ca34972a0952356156cb3f2dd9add59 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
@@ -1,16 +1,16 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -26,8 +26,8 @@ FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic functio
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function __initialized
 [value] using specification for function __valid
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 3c03d16237033404d08d7c94d0d843b466d92e7d..50d22446a3ca7d28710ae0fa2b70ea3fca0a0d17 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
@@ -1,5 +1,5 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -22,8 +22,8 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
 [value] using specification for function __store_block
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function __initialized
 [value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle
index 47d5eca05259756fcb3c5c9e498e56cb015fc657..f43059447740071878c53a8503137c8d87361289 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle
@@ -1,16 +1,16 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -29,8 +29,8 @@ FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic functio
 [value] using specification for function __full_init
 [value] using specification for function __malloc
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+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 unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/ptr_init.c:28:[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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 94c9f4833c496f842033af0e7c299332aadd8b57..c4219110595d31982ec8e4ddd3249c573b6e6e48 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -1,5 +1,5 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -25,8 +25,8 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
 [value] using specification for function __full_init
 [value] using specification for function __malloc
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+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 unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/ptr_init.c:28:[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.
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 f01e69e5f86e1dd89184c7ecfc682896c30604b2..aa0c31766fccb7ac5c5184b95e0bfa375744b28a 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
@@ -1,25 +1,25 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -41,8 +41,8 @@ tests/e-acsl-runtime/valid.c:35:[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 __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
@@ -57,14 +57,14 @@ tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
 [value] using specification for function __valid_read
 tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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:[kernel] warning: accessing left-value that contains escaping addresses:
                   assert ¬\dangling(&a);
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 86217cc65455a1ec847418186c65173ef2922963..4fb8f5932fda561c87754b0966b9a3d6ec7057a1 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
@@ -1,6 +1,6 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -9,9 +9,9 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `assigns clau
                   Ignoring annotation.
 tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -33,8 +33,8 @@ tests/e-acsl-runtime/valid.c:35:[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 __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
@@ -49,14 +49,14 @@ tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
 [value] using specification for function __valid_read
 tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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:[kernel] warning: accessing left-value that contains escaping addresses:
                   assert ¬\dangling(&a);
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 db2c36636361940020b0252b0603e6d562f5768a..410221074b308e05f965faa37ef8fcfa78fc6a5e 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
@@ -1,25 +1,25 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -38,22 +38,22 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 [value] using specification for function __initialize
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 [value] using specification for function __valid
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
 [value] using specification for function __valid_read
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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:[kernel] warning: accessing left-value that contains escaping addresses:
                   assert ¬\dangling(&a);
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 19562f0d282d2c4d0dbcc5a4931b8b0bf43837f3..178c3cb0cfab37c460c49c44f0eb6d512511f7ef 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
@@ -1,6 +1,6 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -9,9 +9,9 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `assign
                   Ignoring annotation.
 tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -30,8 +30,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 [value] using specification for function __initialize
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 [value] using specification for function __valid
@@ -44,14 +44,14 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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:[kernel] warning: accessing left-value that contains escaping addresses:
                   assert ¬\dangling(&a);
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 7a659870d1b546125c1b21c222fbcca085a08535..6f71759d5db5019c2d5d398579d5549896408528 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
@@ -1,25 +1,25 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:160:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:164:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -40,19 +40,19 @@ tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
 tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
 tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
 tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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 be983fa8f53e2255d4396ae30f5be4e158f20c2d..2937859c630bd772d52d272d3fcdb358b8af8036 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
@@ -1,6 +1,6 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:155:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:174:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -9,9 +9,9 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `assigns cla
                   Ignoring annotation.
 tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -32,8 +32,8 @@ tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __full_init
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+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.)
 tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
 tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
 tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
@@ -45,13 +45,13 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_clear
 FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 [value] using specification for function __freeable
 :0:[value] Assigning imprecise value to __e_acsl_implies.
-        The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:177}
-FRAMAC_SHARE/libc/stdlib.h:177:[value] Reading left-value __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:177}.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+        {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