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 a3f6fce5b351d8f0e472089c7b5f8bc8319d18cb..5815cb1a61a5ca27578fd306824218f07cc48de4 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 03deca8538462c23d094a70ef4a5468661841577..86f84d89e21dffd565e7876659912b5e2595211f 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 7233cd574b3dda6ef10e5e679a2c14cfbd5b1905..a46b458e10340fa024b8a191b7182e6c88e90a69 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,5 +1,5 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' 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.
 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.
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 a3bddc9c6cfb94fc293ee441360a982a55522685..27b861d05e49ba7d98d23b03c03006597f1a74c2 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:171:[e-acsl] warning: E-ACSL construct `\fresh' 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.
 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.
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 24204d3696570d663fe91468eb10ccf1318626a6..ecffec2a355f22edce828ece9c8aa96dae5f00bf 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,5 +1,5 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' 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.
 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.
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 f6b1be90188648454eee189114f61b83a3a30c51..3c03d16237033404d08d7c94d0d843b466d92e7d 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:171:[e-acsl] warning: E-ACSL construct `\fresh' 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.
 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.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
index 84d1209b38b0ac153104e88b32b5f8d8980461f3..bd90eaf199bc57cab2f4b64fea7a1d14bd12f043 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
@@ -40,7 +40,7 @@ tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
 FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
 [value] using specification for function strlen
 FRAMAC_SHARE/libc/string.h:88:[value] Function strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:92:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
+FRAMAC_SHARE/libc/string.h:88:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/string.h:90:[value] Function __e_acsl_strlen: postcondition got status unknown.
 tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
index 1459bc8aff58d72151e15982bdbad03d99b04d51..52e0b30ccc7e7884bcbb52285cceec21b63bb0cf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -64,7 +64,7 @@ tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
 FRAMAC_SHARE/libc/string.h:88:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
 [value] using specification for function strlen
 FRAMAC_SHARE/libc/string.h:88:[value] Function strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:92:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
+FRAMAC_SHARE/libc/string.h:88:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/string.h:90:[value] Function __e_acsl_strlen: postcondition got status unknown.
 tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
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 e6d0c0f33841d3525795aaaeec7f09f5c3a0a3de..47d5eca05259756fcb3c5c9e498e56cb015fc657 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,5 +1,5 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' 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.
 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.
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 f85f20935f8a80d74646b70ad2c8bde1e9bd6950..94c9f4833c496f842033af0e7c299332aadd8b57 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:171:[e-acsl] warning: E-ACSL construct `\fresh' 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.
 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.
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 6e89320751e2912421f59bb21ecf039e16870c56..c292e7da4aa6959b31bf16306e81c4bbb7cccc2e 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 21903d00cdde6da9c086fcaebc1e414f5a584675..b2510e830643b83751994851213f6b5522daf457 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 a39d9db3f6dc491cfa8b5bdfaffbc4691d6b3404..6ac96615ec8ce6c2c375c4beca003434a22687e0 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 2311c786b8fad16d519737bb1ff74cf67dfb3bcd..e17b9826f4f82da61cf058f034ad2c9d86745948 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 1e8be1274020a4b0f81d7698773ca08cca7fa0e6..e63dff47ba26ef47c5264f376ba7b09a5b6905a4 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.
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 99134fd7a3472f89b8f037c26a408cae23d2695b..e46a99bed937bea2afe6718f0dc9e413d355b65e 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,7 +1,7 @@
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:173:[e-acsl] warning: E-ACSL construct `\freeable' 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.
 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.