From 82d0fbc74262bef6ffa7c83a509d07f433a425b1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 28 Jul 2016 19:26:02 +0200
Subject: [PATCH] [tests] update oracles from frama-c (stdio.h and stdlib.h)
---
src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/comparison.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/comparison.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle | 2 +-
src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/base_addr.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/block_length.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle | 2 +-
.../tests/runtime/oracle/compound_initializers.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/freeable.res.oracle | 2 +-
.../tests/runtime/oracle/function_contract.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/init_function.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/initialized.res.oracle | 8 ++++----
.../e-acsl/tests/runtime/oracle/invariant.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/linear_search.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/literal_string.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/localvar.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/mainargs.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/memalign.res.oracle | 4 ++--
.../e-acsl/tests/runtime/oracle/memsize.res.oracle | 2 +-
.../tests/runtime/oracle/nested_code_annot.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle | 2 +-
.../tests/runtime/oracle/other_constants.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/ptr_init.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle | 4 ++--
.../e-acsl/tests/runtime/oracle/stmt_contract.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/typedef.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/valid_alias.res.oracle | 2 +-
.../tests/runtime/oracle/valid_in_contract.res.oracle | 2 +-
src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle | 2 +-
73 files changed, 78 insertions(+), 78 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
index a1efff663ec..c0f60bb9332 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index 1ac7d08f321..3c0445eaa65 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -1,6 +1,6 @@
tests/bts/bts1307.i:14:[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.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index bf9bb319fee..cac71008425 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] warning: function __gmpz_add: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
index 3c4f6da5ee6..bacee170702 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1395.i:8:[value] warning: detected recursive call
(__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:6 <-
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
index 9e71ef5cd9c..af14e0bb0a5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i-1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index cd1061a6ab1..3c37f649684 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
index a5145b00d02..9a6cf569c07 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
index 87c6dcd6ce8..52a817d7f56 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
index a50e00db108..5c33bc4b378 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
index 79d4431b134..9b5fed74883 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
index 8dac346dd07..bfbd1c07d7b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index fd93b0ef8be..0fcdc2fb63f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index da6644fbce8..69d5e43631b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
index fd93b0ef8be..0fcdc2fb63f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index 96d01b65408..55a0202e8be 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
index 9cdbecccc2d..96f40bbff21 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index 90dd845029a..d1d67e426db 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 49b8bd9c91e..a3d49ff1d50 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 943165c8e66..e8da235b245 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
index fd93b0ef8be..0fcdc2fb63f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index b80b1b94ba9..11247c857c5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index dd4d5f56994..36eb75bd7e2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index 4eb52e87cc8..815cc1ea71a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[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/no-main/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
index 78ab0fdc7a3..06bc862bfdf 100644
--- a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
@@ -9,5 +9,5 @@
Please use option `-main' for specifying a valid entry point.
The generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
index b6be2205fa2..e97466df14f 100644
--- a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
@@ -4,7 +4,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing tests/reject/quantif.i (no preprocessing)
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
tests/reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
Ignoring annotation.
tests/reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
index f036e67ecf2..4411a244081 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/base_addr.c:44:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
index 0e1c1b7836b..3ca9eaf93f6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/block_length.c:45:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
index 3f2a8ce62f8..87264725da0 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/freeable.c:15:[value] warning: assertion got status unknown.
tests/runtime/freeable.c:15:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index a03bd604222..21cc0500b6d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -1,14 +1,14 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:65:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:69:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:192:[value] warning: function realloc: precondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:207:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:205:[value] warning: function realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:220:[value] warning: function realloc, behavior dealloc: precondition got status unknown.
tests/runtime/initialized.c:74:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:76:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:192:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
tests/runtime/initialized.c:84:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:85:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:93:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
index 6371555500e..482793c4695 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/lazy.i:15:[value] warning: assertion got status unknown.
tests/runtime/lazy.i:16:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
index 3d4852c2ca0..2a1ab61c5d2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/linear_search.i:7:[value] warning: function __gen_e_acsl_search: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
index bf69e33caf1..014ec9e0c35 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/loop.i:19:[value] warning: loop invariant got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status invalid.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index 9aae85b0e44..d21b22db685 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -2,7 +2,7 @@
[e-acsl] warning: annotating undefined function `strlen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/string.h:91:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
index 67d1f2024f0..16feb4243e7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/memalign.c:12:[kernel] warning: Neither code nor specification for function posix_memalign, generating default assigns from the prototype
tests/runtime/memalign.c:14:[value] warning: out of bounds read. assert \valid_read(memptr);
@@ -7,7 +7,7 @@ tests/runtime/memalign.c:15:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/memalign.c:16:[value] warning: assertion got status unknown.
tests/runtime/memalign.c:17:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:192:[value] warning: function free, behavior deallocation: precondition 'freeable' got status unknown.
tests/runtime/memalign.c:19:[value] warning: assertion got status unknown.
tests/runtime/memalign.c:22:[kernel] warning: Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
tests/runtime/memalign.c:23:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
index 1b98eb7e1f5..c2c058a09c8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/memsize.c:14:[value] warning: assertion got status unknown.
tests/runtime/memsize.c:16:[value] warning: assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
index 5c2952ccf21..ff276a5661e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/offset.c:39:[value] warning: assertion got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
index 984d463a3f4..076b78405db 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/ptr.i:17:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
index ca55ee70fe8..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
index 44291ede341..b5e5c01abd8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
@@ -2,10 +2,10 @@
[e-acsl] warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
tests/runtime/stdout.c:11:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdio.h:108:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/stdout.c:11:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
index 7f905326836..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
index d228ea8b234..e349b465623 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid.c:47:[value] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
index f71def74dfd..0ad7e030f9c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
index 005fc4c5690..d64f446a6ee 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid_in_contract.c:19:[value] warning: out of bounds read. assert \valid_read(&l->next);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
index a7dc1372f5b..e086562b64a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:147:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/vector.c:27:[value] warning: assertion got status unknown.
--
GitLab