diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 633eebb1b80ea1119336d7b0cc1631e23f88073a..2a4d0d22d4269303158098e4d3ec090393ce2221 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -41,7 +41,7 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function memchr:
   i ∈ {0; 1; 2; 3; 4}
-  s ∈ {{ "toto" + {0; 1} ; "toto" + [0..15] }}
+  s ∈ {{ "toto" + {0; 1} ; "toto" + [0..--] }}
   __retres ∈ {{ NULL ; "toto" + {1} }}
 [value] Values at end of function __e_acsl_memchr:
   __retres ∈ {{ NULL ; "toto" + {1} }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index 121482b595467ab9284ea2b4d3d5a8c1d50ee839..985d45972db02b5373140220eba88cdfd4c38c22 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -71,7 +71,7 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function memchr:
   i ∈ {0; 1; 2; 3; 4}
-  s ∈ {{ "toto" + {0; 1} ; "toto" + [0..15] }}
+  s ∈ {{ "toto" + {0; 1} ; "toto" + [0..--] }}
   __retres ∈ {{ NULL ; "toto" + {1} }}
 [value] Values at end of function __e_acsl_memchr:
   __retres ∈ {{ NULL ; "toto" + {1} }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index 26fdbdf56a1cfd6d37c1e948e1aa681304125764..e448dafe1d0a6874b99a23cebb1438249f32d0dc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -40,7 +40,7 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
 share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
 [value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 2ae61370575a804ec92a4b34001934ab76fa7aac..ff089a32e687b756550eb9531f3c530378f94c14 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -62,7 +62,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: po
 share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
 [value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index 6a5b3db26ea212d6c65653fb9d78356f92baa2f2..1080142ed784e5b3eee561d26cced737bfb98462 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -65,7 +65,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -146,7 +146,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 81e2086b6cceb0cb557103e870920d6d07f167e6..acea4fddfbdd92c8443128260af343245f62fbac 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -65,7 +65,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -193,7 +193,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
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 24c1900f45f315ad526cc24143da48e874df6306..000231885aeaef578f4b46c0315e6336b399b54d 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -139,7 +139,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
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 24c1900f45f315ad526cc24143da48e874df6306..000231885aeaef578f4b46c0315e6336b399b54d 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -139,7 +139,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
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 9029158b5ae4ff2ead62e2b6b0a3d77d56678614..e7016652779a3eedf1882efbda47a90887b8c1be 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -143,7 +143,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
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 b3a6ea3eefb8503d1d10a1d42248effca7487f51..53c782d139425e02df5615b6762e59fd3f8e084b 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -159,7 +159,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
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 30361464f2f18ef8745927a71598aa367b8d2d4c..2705a2df7ac2f081f167c0747605700ba9df6c21 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -136,7 +136,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
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 f2a1b12677decf117d79bbff05f458873460e45f..569d289872a9fd5c46112bcd751bdb29cb0f52de 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
@@ -59,7 +59,7 @@ extern void *__malloc(size_t size);
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
@@ -156,7 +156,7 @@ void *__e_acsl_malloc(size_t size)
     
     behavior deallocation:
       assumes p ≢ \null;
-      requires \freeable(p);
+      requires freeable: \freeable(p);
       ensures \allocable(\old(p));
       assigns __fc_heap_status;
       assigns __fc_heap_status \from __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 98c9c6605c9572dd91b9af80031bd5bd2170bb99..e1dd3b1281f2f414f79d33ad4661164cf67c425f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -31,5 +31,5 @@ tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
-  x ∈ [--..--]
+  x ∈ [0..2147483647]
   __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index 9c7cd1c0da7ffbcbe1ba1dc38e3743a56ce5a0e6..61bdef82340fdaa120f855f859c7d84d19ac5522 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -22,5 +22,5 @@ tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function main:
-  x ∈ [--..--]
+  x ∈ [0..2147483647]
   __retres ∈ {0}
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 a611a50644342ff77774003c701ad9020f4c6a08..a283dc7d54866f4c5de654839c3a95067f049af3 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
@@ -75,7 +75,7 @@ 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:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[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(\defined(&a))
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index a611a50644342ff77774003c701ad9020f4c6a08..a283dc7d54866f4c5de654839c3a95067f049af3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -75,7 +75,7 @@ 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:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[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(\defined(&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 56f011916a1cee7646cfba9a69895e8eff2ab957..948d6ce7ca8c7ef49b4aa43896c13eb354180817 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
@@ -52,7 +52,7 @@ share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: po
 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:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[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(\defined(&a))
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 6bbb1e532ed881130eb726d8db9c225f1e5a5727..23e4a547c91ea0284a1cc99f1aa4b53c6efcd3db 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -60,7 +60,7 @@ share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[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(\defined(&a))
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 3a62b0c363a2d01227d31e2af8591aa097d87785..6f80ef172d8a797c18fe071ecce523977e410ad8 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
@@ -43,7 +43,7 @@ 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:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
 [value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index d1cf5ba1df8769be7a6f17cef5e15b3f928d900f..2ef572ab80734475f89fceae4a3434132495bda8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -52,7 +52,7 @@ share/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got stat
 share/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
 [value] using specification for function __e_acsl_memory_clean