diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index dbac98aa3b37c9a69e66930475ddb900743c2a38..4e035d9a7643032e1504dda74955f1e355b1fe0d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -6,8 +6,17 @@
 [kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [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/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index d731b1b8de194d74a04f41a31d3f00814af24fdc..e67c07e6cc14ef837236c0dbc8bce7ea4b2151e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -6,8 +6,13 @@
 [kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
 [e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
-tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating type `real' by `long double'
+tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
 [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/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index d85b2df5421b45857919c25cbbd0f1ac9d2feaa0..4eb0732f08ea29a4f976c95a4e10d447d3969abb 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint b
                   Ignoring annotation.
 tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 06b169791c4882229128f3f9436eb6ca8c947518..559617682a26eaf8b85b388e8438d2120876d2ab 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
@@ -17,8 +17,10 @@ tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns cl
                   Ignoring annotation.
 tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 5d253de0e95420e3600f93c7ab0d9224e606839a..637bbe7691099326d62d95493d559b078db8cba5 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
@@ -13,7 +13,11 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `disjoint beha
                   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.
-tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[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
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 0c526698fa8433879a70c5325eb0d2fe6ca406fb..30e78595460e1a1de36c6f2cb03c2e813f74b0bc 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
@@ -13,7 +13,11 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `disjoint
                   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.
-tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[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
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 329eb373e485a3cbccbf175513c496b5d4e3ea10..b1f418a638d18a9dec240e11a9ae00a3a07ee181 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
@@ -13,7 +13,11 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint
                   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.
-tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[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
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 19712b1068eb35f72fe48a5dcd1d6cbc596b26f3..8a86bcbbb7c192d96cf3f1ef63c5267ace047f96 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `disjoint beh
                   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.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 19712b1068eb35f72fe48a5dcd1d6cbc596b26f3..5bd8feeb8680ec13f050c547b24c8ee09c0a70bc 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
@@ -17,8 +17,10 @@ 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.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 6e31a3954673f1728229e6263ec1e06bdafe8eb6..53dc62141a38d29630081e933470fafccf8552ba 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `disjoi
                   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.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index ddf93884ad62d205f1cab205968f57dcf9ce8707..9c16ed4acb6ab3b87ddb2d6fd7d09f98794b3236 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
@@ -17,8 +17,10 @@ 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.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 9b558f7f59e25466f098814ce7a766606c82c69f..8709e2eece6b7852c0f8fd8cb5b0676feda33850 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
@@ -15,10 +15,20 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `disjoint be
                   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.
-tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index 8c9800244d134d92e8d7ab6642ec4efbd23335f4..35d750d9442728f5126654b915666bee30d3128a 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
@@ -17,8 +17,10 @@ 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.
-tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+                  Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:161:[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