From caa195bcb8670dbe7b53ad23019b69dec5a06003 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 8 Dec 2016 13:32:05 +0100
Subject: [PATCH] Synchronize with Frama-C stable/silicium
---
.../e-acsl/tests/bts/oracle/bts1304.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1307.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1324.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1326.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1390.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1395.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1398.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1399.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1478.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1700.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1717.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1718.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1837.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2191.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2192.res.oracle | 3 +--
.../e-acsl/tests/bts/oracle/bts2231.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2252.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts2192.c | 16 ----------------
.../tests/full-mmodel/oracle/addrOf.0.res.oracle | 5 +----
.../tests/full-mmodel/oracle/addrOf.1.res.oracle | 5 +----
.../tests/full-mmodel/oracle/gen_addrOf2.c | 9 ---------
.../e-acsl/tests/gmp/oracle/arith.0.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/arith.1.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/array.0.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/array.1.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/at.0.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/at.1.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/cast.0.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/cast.1.res.oracle | 5 +----
.../tests/gmp/oracle/comparison.0.res.oracle | 5 +----
.../tests/gmp/oracle/comparison.1.res.oracle | 5 +----
.../gmp/oracle/integer_constant.0.res.oracle | 5 +----
.../gmp/oracle/integer_constant.1.res.oracle | 5 +----
.../tests/gmp/oracle/longlong.0.res.oracle | 5 +----
.../tests/gmp/oracle/longlong.1.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/not.0.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/not.1.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/quantif.0.res.oracle | 5 +----
.../e-acsl/tests/gmp/oracle/quantif.1.res.oracle | 5 +----
.../e-acsl/tests/no-main/oracle/empty.res.oracle | 2 +-
.../tests/reject/oracle/quantif.res.oracle | 2 +-
.../tests/runtime/oracle/addrOf.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/alias.res.oracle | 2 +-
.../tests/runtime/oracle/base_addr.res.oracle | 2 +-
.../tests/runtime/oracle/block_length.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/call.res.oracle | 2 +-
.../oracle/compound_initializers.res.oracle | 2 +-
.../tests/runtime/oracle/ctype_macros.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/errno.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/false.res.oracle | 2 +-
.../tests/runtime/oracle/freeable.res.oracle | 2 +-
.../runtime/oracle/function_contract.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/ghost.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/init.res.oracle | 2 +-
.../runtime/oracle/init_function.res.oracle | 2 +-
.../tests/runtime/oracle/initialized.res.oracle | 8 ++++----
.../tests/runtime/oracle/invariant.res.oracle | 2 +-
.../tests/runtime/oracle/labeled_stmt.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/lazy.res.oracle | 2 +-
.../runtime/oracle/linear_search.res.oracle | 2 +-
.../runtime/oracle/literal_string.res.oracle | 2 +-
.../tests/runtime/oracle/localvar.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/loop.res.oracle | 2 +-
.../tests/runtime/oracle/mainargs.res.oracle | 2 +-
.../tests/runtime/oracle/memalign.res.oracle | 4 ++--
.../tests/runtime/oracle/memsize.res.oracle | 2 +-
.../runtime/oracle/nested_code_annot.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/null.res.oracle | 2 +-
.../tests/runtime/oracle/offset.res.oracle | 2 +-
.../runtime/oracle/other_constants.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/ptr.res.oracle | 2 +-
.../tests/runtime/oracle/ptr_init.res.oracle | 2 +-
.../tests/runtime/oracle/result.res.oracle | 2 +-
.../tests/runtime/oracle/sizeof.res.oracle | 2 +-
.../tests/runtime/oracle/stdout.res.oracle | 2 +-
.../runtime/oracle/stmt_contract.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/true.res.oracle | 2 +-
.../tests/runtime/oracle/typedef.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/valid.res.oracle | 2 +-
.../tests/runtime/oracle/valid_alias.res.oracle | 2 +-
.../runtime/oracle/valid_in_contract.res.oracle | 2 +-
.../tests/runtime/oracle/vector.res.oracle | 2 +-
82 files changed, 84 insertions(+), 170 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 ec3e89c44a7..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:276:[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 f2bae8ef88f..8150df6c916 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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 881eb5ae793..655291e225a 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:276:[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/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
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 4e70dabff69..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:276:[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 c33737e3cac..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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 d6789472784..679195365be 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:276:[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 74b2c0f8866..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:276:[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/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
index f949e40637a..d122567f658 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
@@ -2,6 +2,5 @@
[e-acsl] warning: annotating undefined function `atoi':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:276:[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/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
index 4346efc85c3..472d35b1f8e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[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/bts2231.i:8:[value] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
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/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index 74b2c0f8866..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[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/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
index 36fd0bd46ca..85c23235916 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -1,30 +1,14 @@
/* Generated by Frama-C */
-char *__gen_e_acsl_literal_string;
int a;
char *n = (char *)"134";
-void __e_acsl_globals_init(void)
-{
- __gen_e_acsl_literal_string = "134";
- __e_acsl_store_block((void *)__gen_e_acsl_literal_string,sizeof("134"));
- __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
- __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
- __e_acsl_store_block((void *)(& n),8UL);
- __e_acsl_full_init((void *)(& n));
- return;
-}
-
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
- __e_acsl_globals_init();
{ /* sequence */
argc = __gen_e_acsl_atoi((char const *)n);
a = argc;
}
__retres = 0;
- __e_acsl_delete_block((void *)(& n));
- __e_acsl_memory_clean();
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
index b95faa85434..c67fe7c0127 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
index b95faa85434..c67fe7c0127 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
index 1b114dc836d..3dd31d81396 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
@@ -30,12 +30,6 @@ void f(void)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& __fc_wctomb_state),4UL);
- __e_acsl_full_init((void *)(& __fc_wctomb_state));
- __e_acsl_store_block((void *)(& __fc_mbtowc_state),4UL);
- __e_acsl_full_init((void *)(& __fc_mbtowc_state));
- __e_acsl_store_block((void *)(& __fc_mblen_state),4UL);
- __e_acsl_full_init((void *)(& __fc_mblen_state));
__e_acsl_store_block((void *)(& __fc_rand_max),8UL);
__e_acsl_full_init((void *)(& __fc_rand_max));
__e_acsl_store_block((void *)(& __fc_random_counter),4UL);
@@ -59,9 +53,6 @@ int main(void)
(char *)"&x == &x",16);
__e_acsl_full_init((void *)(& __retres));
__retres = 0;
- __e_acsl_delete_block((void *)(& __fc_wctomb_state));
- __e_acsl_delete_block((void *)(& __fc_mbtowc_state));
- __e_acsl_delete_block((void *)(& __fc_mblen_state));
__e_acsl_delete_block((void *)(& __fc_rand_max));
__e_acsl_delete_block((void *)(& __fc_random_counter));
__e_acsl_delete_block((void *)(& x));
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 ef42a641f62..5a51cdb6b63 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 7cd3588f92f..4c83e20b132 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 1dc1420dc36..8259006cb1d 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 abee4dc3c7a..a660cbc95ac 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 8a83d5c555e..50ced3dbf56 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 6d02abba828..5b962789227 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 6518cc1154c..f313e3eaa34 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 9baa5e8c720..832b3b0b926 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 6518cc1154c..f313e3eaa34 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 e8c6147cea1..a32dcb9ff6d 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 772dc0983f6..e59dca7d9f6 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 7f54b3889e7..15b62b8c39c 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 e580bdf53e9..2d65b16d279 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 0eee735afc3..c0224815b72 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 6518cc1154c..f313e3eaa34 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 1d4d29db802..98e25700fac 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 774cd469f6c..9a36d534ebe 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 1c7ba24682c..12085056af1 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:276:[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
@@ -8,9 +8,6 @@ FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns cl
__fc_random_counter ∈ {0}
__fc_rand_max ∈ {32767}
__fc_heap_status ∈ [--..--]
- __fc_mblen_state ∈ {0}
- __fc_mbtowc_state ∈ {0}
- __fc_wctomb_state ∈ {0}
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__e_acsl_heap_allocation_size ∈ [--..--]
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 af45ecaf0a3..6acb61c013b 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
@@ -8,5 +8,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:276:[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 b73b059804c..d6d67211119 100644
--- a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
@@ -3,7 +3,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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 6b6527342b0..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:276:[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 48772f01703..61ec66632fb 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:276:[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:50:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
index ae7eacf4a88..893f06f38dc 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
@@ -2,7 +2,7 @@
[e-acsl] warning: annotating undefined function `isupper':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-FRAMAC_SHARE/libc/stdlib.h:276:[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/ctype_macros.c:39:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
index 74b2c0f8866..73a14510c9f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[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 c33737e3cac..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:276:[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 4c983b90f43..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:276:[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 c33737e3cac..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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 c33737e3cac..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:276:[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 cb69e859fa5..7051e9b0576 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:276:[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:321:[value] warning: function realloc: precondition got status unknown.
-FRAMAC_SHARE/libc/stdlib.h:336:[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:308:[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 c33737e3cac..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:276:[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 c33737e3cac..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:276:[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 c33737e3cac..b9986aac775 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:276:[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/linear_search.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
index 71d668555df..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:276:[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 74b2c0f8866..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:276:[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 74b2c0f8866..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:276:[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 5d8e5b79f1f..b823f477b67 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:276:[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 c20a1a7faab..0c616783fb0 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:276:[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 591e95a1f19..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:276:[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:308:[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 f4e55dd11dc..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:276:[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 c33737e3cac..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:276:[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 c33737e3cac..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:276:[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 225bdd10c27..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:276:[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 c33737e3cac..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:276:[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 ee58349831c..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:276:[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 74b2c0f8866..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:276:[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 c33737e3cac..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:276:[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 c33737e3cac..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:276:[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 8a5949c1d1c..557f25d0da0 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
@@ -2,7 +2,7 @@
[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:276:[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:10:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdio.h:108:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
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 c33737e3cac..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:276:[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 c33737e3cac..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:276:[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 c33737e3cac..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:276:[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 82dfbcc3f10..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:276:[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 c9f6e2aa111..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:276:[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 2e0f0d71753..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:276:[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 5cbb1b197fe..19904c3a451 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:276:[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:26:[value] warning: accessing uninitialized left-value. assert \initialized(v2 + 2);
--
GitLab