From 7dcc51f9f91416349a1a8de06be7ee2e6eb4b78e Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 16 Jan 2017 17:57:23 +0100
Subject: [PATCH] synchronize with frama-c/frama-c!1112
---
.../tests/bts/oracle/bts1304.res.oracle | 2 +-
.../tests/bts/oracle/bts1307.res.oracle | 2 +-
.../tests/bts/oracle/bts1324.res.oracle | 2 +-
.../tests/bts/oracle/bts1326.res.oracle | 2 +-
.../tests/bts/oracle/bts1390.res.oracle | 2 +-
.../tests/bts/oracle/bts1395.res.oracle | 2 +-
.../tests/bts/oracle/bts1398.res.oracle | 2 +-
.../tests/bts/oracle/bts1399.res.oracle | 2 +-
.../tests/bts/oracle/bts1478.res.oracle | 2 +-
.../tests/bts/oracle/bts1700.res.oracle | 2 +-
.../tests/bts/oracle/bts1717.res.oracle | 2 +-
.../tests/bts/oracle/bts1718.res.oracle | 2 +-
.../tests/bts/oracle/bts1837.res.oracle | 2 +-
.../tests/bts/oracle/bts2191.res.oracle | 2 +-
.../tests/bts/oracle/bts2192.res.oracle | 2 +-
.../tests/bts/oracle/bts2231.res.oracle | 2 +-
.../tests/bts/oracle/bts2252.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1304.c | 7 ++--
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 33 ++++++++++---------
.../e-acsl/tests/bts/oracle/gen_bts1324.c | 7 ++--
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 15 +++++----
.../e-acsl/tests/bts/oracle/gen_bts1390.c | 13 ++++----
.../e-acsl/tests/bts/oracle/gen_bts1395.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts1398.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1478.c | 7 ++--
.../e-acsl/tests/bts/oracle/gen_bts1700.c | 7 ++--
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 7 ++--
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 7 ++--
.../e-acsl/tests/bts/oracle/gen_bts1837.c | 11 ++++---
.../e-acsl/tests/bts/oracle/gen_bts2191.c | 5 +--
.../e-acsl/tests/bts/oracle/gen_bts2192.c | 5 +--
.../e-acsl/tests/bts/oracle/gen_bts2231.c | 1 +
.../e-acsl/tests/bts/oracle/gen_bts2252.c | 5 +--
.../full-mmodel/oracle/addrOf.0.res.oracle | 2 +-
.../full-mmodel/oracle/addrOf.1.res.oracle | 2 +-
.../tests/full-mmodel/oracle/gen_addrOf.c | 9 ++---
.../tests/full-mmodel/oracle/gen_addrOf2.c | 23 ++++++-------
.../tests/gmp/oracle/arith.0.res.oracle | 2 +-
.../tests/gmp/oracle/arith.1.res.oracle | 2 +-
.../tests/gmp/oracle/array.0.res.oracle | 2 +-
.../tests/gmp/oracle/array.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/at.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/at.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/cast.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/cast.1.res.oracle | 2 +-
.../tests/gmp/oracle/comparison.0.res.oracle | 2 +-
.../tests/gmp/oracle/comparison.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/gen_arith.c | 1 +
.../e-acsl/tests/gmp/oracle/gen_arith2.c | 1 +
src/plugins/e-acsl/tests/gmp/oracle/gen_at.c | 17 +++++-----
src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c | 17 +++++-----
.../e-acsl/tests/gmp/oracle/gen_comparison.c | 1 +
.../e-acsl/tests/gmp/oracle/gen_comparison2.c | 1 +
.../tests/gmp/oracle/gen_integer_constant.c | 1 +
.../tests/gmp/oracle/gen_integer_constant2.c | 1 +
src/plugins/e-acsl/tests/gmp/oracle/gen_not.c | 1 +
.../e-acsl/tests/gmp/oracle/gen_not2.c | 1 +
.../e-acsl/tests/gmp/oracle/gen_quantif.c | 1 +
.../e-acsl/tests/gmp/oracle/gen_quantif2.c | 1 +
.../gmp/oracle/integer_constant.0.res.oracle | 2 +-
.../gmp/oracle/integer_constant.1.res.oracle | 2 +-
.../tests/gmp/oracle/longlong.0.res.oracle | 2 +-
.../tests/gmp/oracle/longlong.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/not.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/not.1.res.oracle | 2 +-
.../tests/gmp/oracle/quantif.0.res.oracle | 2 +-
.../tests/gmp/oracle/quantif.1.res.oracle | 2 +-
.../tests/no-main/oracle/empty.res.oracle | 2 +-
.../tests/reject/oracle/quantif.res.oracle | 2 +-
.../tests/runtime/oracle/addrOf.res.oracle | 2 +-
.../tests/runtime/oracle/alias.res.oracle | 2 +-
.../tests/runtime/oracle/base_addr.res.oracle | 2 +-
.../runtime/oracle/block_length.res.oracle | 2 +-
.../tests/runtime/oracle/call.res.oracle | 2 +-
.../oracle/compound_initializers.res.oracle | 2 +-
.../runtime/oracle/ctype_macros.res.oracle | 8 ++---
.../tests/runtime/oracle/errno.res.oracle | 2 +-
.../tests/runtime/oracle/false.res.oracle | 2 +-
.../tests/runtime/oracle/freeable.res.oracle | 2 +-
.../oracle/function_contract.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/gen_addrOf.c | 9 ++---
.../e-acsl/tests/runtime/oracle/gen_alias.c | 9 ++---
.../tests/runtime/oracle/gen_base_addr.c | 25 +++++++-------
.../tests/runtime/oracle/gen_block_length.c | 25 +++++++-------
.../oracle/gen_compound_initializers.c | 17 +++++-----
.../tests/runtime/oracle/gen_ctype_macros.c | 8 +++--
.../e-acsl/tests/runtime/oracle/gen_errno.c | 9 +++--
.../e-acsl/tests/runtime/oracle/gen_false.c | 1 +
.../runtime/oracle/gen_function_contract.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_init.c | 11 ++++---
.../tests/runtime/oracle/gen_init_function.c | 3 +-
.../tests/runtime/oracle/gen_initialized.c | 21 ++++++------
.../tests/runtime/oracle/gen_labeled_stmt.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_lazy.c | 1 +
.../tests/runtime/oracle/gen_linear_search.c | 1 +
.../tests/runtime/oracle/gen_literal_string.c | 15 +++++----
.../tests/runtime/oracle/gen_mainargs.c | 8 +++--
.../tests/runtime/oracle/gen_memalign.c | 9 ++---
.../e-acsl/tests/runtime/oracle/gen_memsize.c | 4 ++-
.../runtime/oracle/gen_nested_code_annot.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_null.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_offset.c | 19 ++++++-----
.../runtime/oracle/gen_other_constants.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_ptr.c | 9 ++---
.../tests/runtime/oracle/gen_ptr_init.c | 13 ++++----
.../e-acsl/tests/runtime/oracle/gen_result.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_sizeof.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_stdout.c | 8 +++--
.../tests/runtime/oracle/gen_stmt_contract.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_true.c | 1 +
.../e-acsl/tests/runtime/oracle/gen_typedef.c | 1 +
.../tests/runtime/oracle/ghost.res.oracle | 2 +-
.../tests/runtime/oracle/init.res.oracle | 2 +-
.../runtime/oracle/init_function.res.oracle | 2 +-
.../runtime/oracle/initialized.res.oracle | 8 ++---
.../tests/runtime/oracle/invariant.res.oracle | 2 +-
.../runtime/oracle/labeled_stmt.res.oracle | 2 +-
.../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 +-
.../tests/runtime/oracle/loop.res.oracle | 2 +-
.../tests/runtime/oracle/mainargs.res.oracle | 14 ++++----
.../tests/runtime/oracle/memalign.res.oracle | 4 +--
.../tests/runtime/oracle/memsize.res.oracle | 2 +-
.../oracle/nested_code_annot.res.oracle | 2 +-
.../tests/runtime/oracle/null.res.oracle | 2 +-
.../tests/runtime/oracle/offset.res.oracle | 2 +-
.../runtime/oracle/other_constants.res.oracle | 2 +-
.../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 | 4 +--
.../runtime/oracle/stmt_contract.res.oracle | 2 +-
.../tests/runtime/oracle/true.res.oracle | 2 +-
.../tests/runtime/oracle/typedef.res.oracle | 2 +-
.../tests/runtime/oracle/valid.res.oracle | 2 +-
.../runtime/oracle/valid_alias.res.oracle | 2 +-
.../oracle/valid_in_contract.res.oracle | 2 +-
.../tests/runtime/oracle/vector.res.oracle | 2 +-
141 files changed, 350 insertions(+), 282 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..cee0e88b084 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:277:[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..d7e404049c5 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..fe811626ae5 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:277:[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..32524547d5a 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:277:[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..672ba3db925 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..a5cae9217c8 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:277:[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..a0a8836bb7a 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:277:[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..ed365527f42 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,6 @@
[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:277:[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..079242c9078 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:277:[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 3e7b66c55fa..a65de6cfc50 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,6 +1,6 @@
tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Old style K&R code?
[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:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, 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_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 9393af7ffa7..e6561a3073f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
struct msgA {
int type ;
int a[2] ;
@@ -17,7 +18,7 @@ union msg {
};
void read_sensor_4(unsigned int *m)
{
- __e_acsl_store_block((void *)(& m),8UL);
+ __e_acsl_store_block((void *)(& m),(size_t)8);
__e_acsl_initialize((void *)m,sizeof(unsigned int));
*m = (unsigned int)0;
__e_acsl_delete_block((void *)(& m));
@@ -29,8 +30,8 @@ int main(void)
int __retres;
unsigned char buf[sizeof(union msg)];
int i;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(buf),16UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(buf),(size_t)16);
i = 0;
while ((unsigned long)i < sizeof(buf) / (unsigned long)4) {
read_sensor_4((unsigned int *)(buf) + i);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index ab8e3d95afd..ccf51aabe3e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
requires \valid(Mtmax_out);
@@ -23,9 +24,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out);
*/
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
- __e_acsl_store_block((void *)(& Mtmax_in),8UL);
- __e_acsl_store_block((void *)(& Mwmax),8UL);
- __e_acsl_store_block((void *)(& Mtmax_out),8UL);
+ __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
__e_acsl_initialize((void *)Mtmax_out,sizeof(float));
*Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
5 / 80) * *Mwmax) * 0.4));
@@ -61,9 +62,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out);
*/
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
- __e_acsl_store_block((void *)(& Mtmin_in),8UL);
- __e_acsl_store_block((void *)(& Mwmin),8UL);
- __e_acsl_store_block((void *)(& Mtmin_out),8UL);
+ __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
__e_acsl_initialize((void *)Mtmin_out,sizeof(float));
*Mtmin_out = (float)(0.85 * (double)*Mwmin);
__e_acsl_delete_block((void *)(& Mtmin_in));
@@ -78,10 +79,10 @@ int main(void)
float f;
float g;
float h;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& h),4UL);
- __e_acsl_store_block((void *)(& g),4UL);
- __e_acsl_store_block((void *)(& f),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& h),(size_t)4);
+ __e_acsl_store_block((void *)(& g),(size_t)4);
+ __e_acsl_store_block((void *)(& f),(size_t)4);
__e_acsl_full_init((void *)(& f));
f = (float)1.0;
__e_acsl_full_init((void *)(& g));
@@ -119,9 +120,9 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
int __gen_e_acsl_valid_3;
- __e_acsl_store_block((void *)(& Mtmin_in),8UL);
- __e_acsl_store_block((void *)(& Mwmin),8UL);
- __e_acsl_store_block((void *)(& Mtmin_out),8UL);
+ __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"bar",
(char *)"\\valid(Mtmin_in)",17);
@@ -215,9 +216,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
int __gen_e_acsl_valid;
int __gen_e_acsl_valid_2;
int __gen_e_acsl_valid_3;
- __e_acsl_store_block((void *)(& Mtmax_in),8UL);
- __e_acsl_store_block((void *)(& Mwmax),8UL);
- __e_acsl_store_block((void *)(& Mtmax_out),8UL);
+ __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
+ __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
+ __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
(char *)"\\valid(Mtmax_in)",5);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index f9745849a2f..8a6f07863a3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
/*@ behavior yes:
assumes ∀ int i; 0 < i < n ⇒ *(t + (i - 1)) ≤ *(t + i);
ensures \result ≡ 1;
@@ -35,8 +36,8 @@ int main(void)
int __retres;
int t[7];
int n;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(t),28UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)28);
__e_acsl_initialize((void *)(t),sizeof(int));
t[0] = 1;
__e_acsl_initialize((void *)(& t[1]),sizeof(int));
@@ -69,7 +70,7 @@ int __gen_e_acsl_sorted(int *t, int n)
{
int __gen_e_acsl_at;
int __retres;
- __e_acsl_store_block((void *)(& t),8UL);
+ __e_acsl_store_block((void *)(& t),(size_t)8);
{
int __gen_e_acsl_forall;
int __gen_e_acsl_i;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index 3b83bd40373..eb341729c74 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
typedef int ArrayInt[5];
/*@ ensures
*\old(AverageAccel) ≡
@@ -19,8 +20,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
*/
void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
{
- __e_acsl_store_block((void *)(& Accel),8UL);
- __e_acsl_store_block((void *)(& AverageAccel),8UL);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
+ __e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
__e_acsl_initialize((void *)AverageAccel,sizeof(int));
*AverageAccel = (((((*Accel)[4] + (*Accel)[3]) + (*Accel)[2]) + (*Accel)[1]) + (*Accel)[0]) / 5;
__e_acsl_delete_block((void *)(& Accel));
@@ -33,9 +34,9 @@ int main(void)
int __retres;
ArrayInt Accel;
int av;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& av),4UL);
- __e_acsl_store_block((void *)(Accel),20UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& av),(size_t)4);
+ __e_acsl_store_block((void *)(Accel),(size_t)20);
__e_acsl_initialize((void *)(Accel),sizeof(int));
Accel[0] = 1;
__e_acsl_initialize((void *)(& Accel[1]),sizeof(int));
@@ -70,8 +71,8 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
ArrayInt *__gen_e_acsl_at_3;
ArrayInt *__gen_e_acsl_at_2;
int *__gen_e_acsl_at;
- __e_acsl_store_block((void *)(& Accel),8UL);
- __e_acsl_store_block((void *)(& AverageAccel),8UL);
+ __e_acsl_store_block((void *)(& Accel),(size_t)8);
+ __e_acsl_store_block((void *)(& AverageAccel),(size_t)8);
__gen_e_acsl_at_6 = Accel;
__gen_e_acsl_at_5 = Accel;
__gen_e_acsl_at_4 = Accel;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 54750d7081e..337f725608d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
/*@ behavior exists:
@@ -30,9 +31,9 @@ void *memchr(void const *buf, int c, size_t n)
void *__retres;
int i;
char *s;
- __e_acsl_store_block((void *)(& s),8UL);
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& buf),8UL);
+ __e_acsl_store_block((void *)(& s),(size_t)8);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_store_block((void *)(& buf),(size_t)8);
__e_acsl_full_init((void *)(& s));
s = (char *)buf;
i = 0;
@@ -74,8 +75,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
void const *__gen_e_acsl_at_2;
int __gen_e_acsl_at;
void *__retres;
- __e_acsl_store_block((void *)(& __retres),8UL);
- __e_acsl_store_block((void *)(& buf),8UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)8);
+ __e_acsl_store_block((void *)(& buf),(size_t)8);
{
int __gen_e_acsl_forall_2;
unsigned int __gen_e_acsl_k;
@@ -200,7 +201,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
__gen_e_acsl_memchr((void const *)__gen_e_acsl_literal_string,'o',
(unsigned long)4);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index a6bdcd87f66..d6b5a8fee18 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
/*@ requires n > 0; */
int __gen_e_acsl_fact(int n);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index e61c3232854..5fb9ec622ce 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 4e39439e16b..6b0fb4d512e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int global_i;
int *global_i_ptr = & global_i;
@@ -40,9 +41,9 @@ void __gen_e_acsl_loop(void)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& global_i_ptr),8UL);
+ __e_acsl_store_block((void *)(& global_i_ptr),(size_t)8);
__e_acsl_full_init((void *)(& global_i_ptr));
- __e_acsl_store_block((void *)(& global_i),4UL);
+ __e_acsl_store_block((void *)(& global_i),(size_t)4);
__e_acsl_full_init((void *)(& global_i));
return;
}
@@ -50,7 +51,7 @@ void __e_acsl_globals_init(void)
int main(void)
{
int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
__gen_e_acsl_loop();
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index ea16f514ee2..b9274f28d4d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
struct toto {
};
@@ -7,9 +8,9 @@ int main(void)
int __retres;
struct toto s;
struct toto *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& s),0UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& s),(size_t)0);
/*@ assert \valid(&s); */
{
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 0db5c8ad0f7..5cc71609808 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
int a;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
a = 10;
goto lbl_1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index d37ffae2b81..a4cb9936993 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
int a;
int *p;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
a = 10;
goto lbl_1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index c26af6b5ae3..991bdf1b6a6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
@@ -8,8 +9,8 @@ int f(void)
int __retres;
char *s1;
char *s2;
- __e_acsl_store_block((void *)(& s2),8UL);
- __e_acsl_store_block((void *)(& s1),8UL);
+ __e_acsl_store_block((void *)(& s2),(size_t)8);
+ __e_acsl_store_block((void *)(& s1),(size_t)8);
__e_acsl_full_init((void *)(& s1));
s1 = (char *)__gen_e_acsl_literal_string;
__e_acsl_full_init((void *)(& s2));
@@ -79,7 +80,7 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("bar"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_store_block((void *)(& S),8UL);
+ __e_acsl_store_block((void *)(& S),(size_t)8);
__e_acsl_full_init((void *)(& S));
return;
}
@@ -88,7 +89,7 @@ int main(void)
{
int __retres;
int i;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
i = 4;
while (1) {
@@ -102,7 +103,7 @@ int main(void)
if (! tmp) break;
{
char *s;
- __e_acsl_store_block((void *)(& s),8UL);
+ __e_acsl_store_block((void *)(& s),(size_t)8);
__e_acsl_full_init((void *)(& s));
s = (char *)__gen_e_acsl_literal_string_3;
/*@ assert \valid_read(s); */
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index 8d2fa61eada..89ea5ede7e2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
struct ST {
@@ -20,7 +21,7 @@ void __e_acsl_globals_init(void)
sizeof("Struct_G[0]"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_store_block((void *)(_G),32UL);
+ __e_acsl_store_block((void *)(_G),(size_t)32);
__e_acsl_full_init((void *)(& _G));
return;
}
@@ -28,7 +29,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
/*@ assert \valid_read(_G[0].str); */
{
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..f4dad2e66aa 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
int a;
char *n = (char *)"134";
@@ -8,7 +9,7 @@ void __e_acsl_globals_init(void)
__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_store_block((void *)(& n),(size_t)8);
__e_acsl_full_init((void *)(& n));
return;
}
@@ -16,7 +17,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
{ /* sequence */
argc = __gen_e_acsl_atoi((char const *)n);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
index 174ad1a7f1f..cdf0350057f 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
long A = (long)0;
int main(void)
{
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 17547beac1f..c6a8d88bbff 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string;
/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..));
assigns \result \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
@@ -25,9 +26,9 @@ int main(void)
int loc;
char *destbuf;
char ch;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& srcbuf),8UL);
+ __e_acsl_store_block((void *)(& srcbuf),(size_t)8);
__e_acsl_full_init((void *)(& srcbuf));
srcbuf = (char *)__gen_e_acsl_literal_string;
loc = 1;
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..aa44777703f 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:277:[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/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
index b95faa85434..aa44777703f 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:277:[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/full-mmodel/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
index 46d7ef3a5c1..44756314152 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(void)
{
int m;
int *u;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& u));
u = & m;
__e_acsl_full_init((void *)(& p));
@@ -32,7 +33,7 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
x = 0;
f();
/*@ assert &x ≡ &x; */
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..f966f94eb42 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
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(void)
{
int m;
int *u;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& u));
u = & m;
__e_acsl_full_init((void *)(& p));
@@ -30,15 +31,15 @@ void f(void)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& __fc_wctomb_state),4UL);
+ __e_acsl_store_block((void *)(& __fc_wctomb_state),(size_t)4);
__e_acsl_full_init((void *)(& __fc_wctomb_state));
- __e_acsl_store_block((void *)(& __fc_mbtowc_state),4UL);
+ __e_acsl_store_block((void *)(& __fc_mbtowc_state),(size_t)4);
__e_acsl_full_init((void *)(& __fc_mbtowc_state));
- __e_acsl_store_block((void *)(& __fc_mblen_state),4UL);
+ __e_acsl_store_block((void *)(& __fc_mblen_state),(size_t)4);
__e_acsl_full_init((void *)(& __fc_mblen_state));
- __e_acsl_store_block((void *)(& __fc_rand_max),8UL);
+ __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8);
__e_acsl_full_init((void *)(& __fc_rand_max));
- __e_acsl_store_block((void *)(& __fc_random_counter),4UL);
+ __e_acsl_store_block((void *)(& __fc_random_counter),(size_t)4);
__e_acsl_full_init((void *)(& __fc_random_counter));
return;
}
@@ -47,10 +48,10 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& x),4UL);
- __e_acsl_store_block((void *)(& __retres),4UL);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = 0;
f();
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..2e9ae22fd62 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:277:[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 7cd3588f92f..8af3084fa20 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:277:[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 1dc1420dc36..12c70c5e505 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:277:[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 abee4dc3c7a..a6f7a745874 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:277:[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 8a83d5c555e..630deaa6d7d 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:277:[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 6d02abba828..1e42f99d353 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:277:[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 6518cc1154c..62cf4517ec4 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:277:[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 9baa5e8c720..422f1d17fe8 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:277:[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 6518cc1154c..62cf4517ec4 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:277:[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 e8c6147cea1..9445ce1e9b9 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:277:[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/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index c73057d06af..907f90fb59e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
index b092d8e8ad9..353a05d7762 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
index ff2254d5466..51bb8fb04b6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);
@@ -37,8 +38,8 @@ void g(int *p, int *q)
int __gen_e_acsl_at_3;
int __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_initialize((void *)p,sizeof(int));
*p = 0;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
@@ -106,7 +107,7 @@ int __gen_e_acsl_h(int x);
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_delete_block((void *)(& x));
return x;
}
@@ -119,9 +120,9 @@ int main(void)
int __retres;
int x;
int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(t),8UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
@@ -158,8 +159,8 @@ int __gen_e_acsl_h(int x)
{
int __gen_e_acsl_at;
int __retres;
- __e_acsl_store_block((void *)(& __retres),4UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__gen_e_acsl_at = x;
__retres = h(x);
__e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
index 05325507dda..76f52e27256 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A = 0;
/*@ ensures \at(A,Post) ≡ 3; */
void __gen_e_acsl_f(void);
@@ -102,8 +103,8 @@ void g(int *p, int *q)
int __gen_e_acsl_at_3;
__e_acsl_mpz_t __gen_e_acsl_at_2;
int __gen_e_acsl_at;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
__e_acsl_initialize((void *)p,sizeof(int));
*p = 0;
__e_acsl_initialize((void *)(p + 1),sizeof(int));
@@ -189,7 +190,7 @@ int __gen_e_acsl_h(int x);
/*@ ensures \result ≡ \old(x); */
int h(int x)
{
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_delete_block((void *)(& x));
return x;
}
@@ -201,9 +202,9 @@ int main(void)
int __retres;
int x;
int t[2];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(t),8UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = __gen_e_acsl_h(0);
L:
@@ -318,8 +319,8 @@ int __gen_e_acsl_h(int x)
{
__e_acsl_mpz_t __gen_e_acsl_at;
int __retres;
- __e_acsl_store_block((void *)(& __retres),4UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_store_block((void *)(& __retres),(size_t)4);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
{
__e_acsl_mpz_t __gen_e_acsl_x;
__gmpz_init_set_si(__gen_e_acsl_x,(long)x);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
index 8b99036ca25..c6cd92bed36 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
index af5d4476e59..0011c66b85a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
index efc79833e3f..93d218442d3 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
index 66fe6e49946..16f7236bcb4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
index a41c3aa317a..a39e0d44f87 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
index 1d975679dd3..f870338038b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
index f4f995dc102..cd49f58f7fe 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
index 553c2671415..558fad0101c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
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..e8297cbb920 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:277:[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 7f54b3889e7..ae2a4fc2ad8 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:277:[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 e580bdf53e9..331bfe9e4a5 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:277:[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 0eee735afc3..264bea4cd8f 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:277:[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 6518cc1154c..62cf4517ec4 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:277:[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 1d4d29db802..6c8ef42ae5b 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:277:[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 774cd469f6c..ee86d9b6561 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:277:[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 1c7ba24682c..5621b649209 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:277:[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 af45ecaf0a3..d3fd34d75ba 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:277:[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..c161e46326a 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..4522e542c99 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:277:[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..23012dfcdd0 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..e4acdca2ce2 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,11 +2,11 @@
[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:277:[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".
-FRAMAC_SHARE/libc/ctype.h:163:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
+FRAMAC_SHARE/libc/ctype.h:164:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/libc/ctype.h:167:[value] warning: function __gen_e_acsl_isupper, behavior definitely_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/ctype.h:170:[value] warning: function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/ctype.h:168:[value] warning: function __gen_e_acsl_isupper, behavior definitely_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/ctype.h:171:[value] warning: function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
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..a0a8836bb7a 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:277:[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..672ba3db925 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:277:[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..90b97b057b4 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:277:[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..672ba3db925 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:277:[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/gen_addrOf.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
index 46d7ef3a5c1..44756314152 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
@@ -1,12 +1,13 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(void)
{
int m;
int *u;
int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& u),8UL);
- __e_acsl_store_block((void *)(& m),4UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& u),(size_t)8);
+ __e_acsl_store_block((void *)(& m),(size_t)4);
__e_acsl_full_init((void *)(& u));
u = & m;
__e_acsl_full_init((void *)(& p));
@@ -32,7 +33,7 @@ int main(void)
{
int __retres;
int x;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
x = 0;
f();
/*@ assert &x ≡ &x; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
index 4fabf481163..223753bbaf8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
@@ -1,9 +1,10 @@
/* Generated by Frama-C */
+#include "stdlib.h"
void f(int *dest, int val)
{
int *ptr;
- __e_acsl_store_block((void *)(& ptr),8UL);
- __e_acsl_store_block((void *)(& dest),8UL);
+ __e_acsl_store_block((void *)(& ptr),(size_t)8);
+ __e_acsl_store_block((void *)(& dest),(size_t)8);
__e_acsl_full_init((void *)(& ptr));
ptr = dest;
__e_acsl_initialize((void *)ptr,sizeof(int));
@@ -17,8 +18,8 @@ int main(void)
{
int __retres;
int i;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& i),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& i),(size_t)4);
f(& i,255);
/*@ assert \initialized(&i); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
index df7cd294634..6cbfcdb5c04 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A[4] = {1, 2, 3, 4};
int *PA;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& PA),8UL);
+ __e_acsl_store_block((void *)(& PA),(size_t)8);
__e_acsl_full_init((void *)(& PA));
- __e_acsl_store_block((void *)(A),16UL);
+ __e_acsl_store_block((void *)(A),(size_t)16);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -22,17 +23,17 @@ int main(void)
char *pd;
long *q;
long *qd;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& qd),8UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& pd),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& pi),8UL);
- __e_acsl_store_block((void *)(& pl),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(& pa),8UL);
- __e_acsl_store_block((void *)(a),16UL);
+ __e_acsl_store_block((void *)(& qd),(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& pd),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_store_block((void *)(& pa),(size_t)8);
+ __e_acsl_store_block((void *)(a),(size_t)16);
PA = (int *)(& A);
/*@ assert \base_addr((int *)A) ≡ \base_addr(PA); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
index dd82340cf0c..c39e410bde3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
struct Zero {
};
@@ -7,11 +8,11 @@ int *PA;
struct Zero ZERO;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& ZERO),0UL);
+ __e_acsl_store_block((void *)(& ZERO),(size_t)0);
__e_acsl_full_init((void *)(& ZERO));
- __e_acsl_store_block((void *)(& PA),8UL);
+ __e_acsl_store_block((void *)(& PA),(size_t)8);
__e_acsl_full_init((void *)(& PA));
- __e_acsl_store_block((void *)(A),16UL);
+ __e_acsl_store_block((void *)(A),(size_t)16);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -28,16 +29,16 @@ int main(void)
size_t size;
char *p;
long *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& pi),8UL);
- __e_acsl_store_block((void *)(& pl),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(& pa),8UL);
- __e_acsl_store_block((void *)(a),16UL);
- __e_acsl_store_block((void *)(& zero),0UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_store_block((void *)(& pa),(size_t)8);
+ __e_acsl_store_block((void *)(a),(size_t)16);
+ __e_acsl_store_block((void *)(& zero),(size_t)0);
/*@ assert \block_length(&ZERO) ≡ 0; */
{
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
index 146ccb703bc..036561f3870 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_3;
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
@@ -41,19 +42,19 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_5,sizeof("First"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_5);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_5);
- __e_acsl_store_block((void *)(_G),32UL);
+ __e_acsl_store_block((void *)(_G),(size_t)32);
__e_acsl_full_init((void *)(& _G));
- __e_acsl_store_block((void *)(& _E),4UL);
+ __e_acsl_store_block((void *)(& _E),(size_t)4);
__e_acsl_full_init((void *)(& _E));
- __e_acsl_store_block((void *)(_D),8UL);
+ __e_acsl_store_block((void *)(_D),(size_t)8);
__e_acsl_full_init((void *)(& _D));
- __e_acsl_store_block((void *)(& _C),8UL);
+ __e_acsl_store_block((void *)(& _C),(size_t)8);
__e_acsl_full_init((void *)(& _C));
- __e_acsl_store_block((void *)(& _B),8UL);
+ __e_acsl_store_block((void *)(& _B),(size_t)8);
__e_acsl_full_init((void *)(& _B));
- __e_acsl_store_block((void *)(_A),16UL);
+ __e_acsl_store_block((void *)(_A),(size_t)16);
__e_acsl_full_init((void *)(& _A));
- __e_acsl_store_block((void *)(& _F),4UL);
+ __e_acsl_store_block((void *)(& _F),(size_t)4);
__e_acsl_full_init((void *)(& _F));
return;
}
@@ -61,7 +62,7 @@ void __e_acsl_globals_init(void)
int main(int argc, char **argv)
{
int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
__e_acsl_globals_init();
/*@ assert \valid((char **)_A); */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
index ca1c9e181ae..28d6aaa604c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
@@ -1,13 +1,15 @@
/* Generated by Frama-C */
+#include "ctype.h"
+#include "stdlib.h"
int main(int argc, char const **argv)
{
int __retres;
char c;
int tmp;
char *d;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
- __e_acsl_store_block((void *)(& d),8UL);
- __e_acsl_store_block((void *)(& c),1UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ __e_acsl_store_block((void *)(& d),(size_t)8);
+ __e_acsl_store_block((void *)(& c),(size_t)1);
tmp = __gen_e_acsl_isupper(argc);
__e_acsl_full_init((void *)(& c));
c = (char)tmp;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
index 272da24e99b..33c2ae302dd 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
@@ -1,7 +1,10 @@
/* Generated by Frama-C */
+#include "errno.h"
+#include "stdio.h"
+#include "stdlib.h"
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& __FC_errno),4UL);
+ __e_acsl_store_block((void *)(& __FC_errno),(size_t)4);
__e_acsl_full_init((void *)(& __FC_errno));
return;
}
@@ -10,9 +13,9 @@ int main(int argc, char const **argv)
{
int __retres;
int *p;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & __FC_errno;
/*@ assert \valid(p); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
index 72116bfac3a..3a77144b85a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
index a27a3104873..7b7b067ff37 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int X = 0;
int Y = 2;
/*@ ensures X ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
index 536af661a41..2527bb61fec 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int a = 0;
int b;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& b),4UL);
+ __e_acsl_store_block((void *)(& b),(size_t)4);
__e_acsl_full_init((void *)(& b));
- __e_acsl_store_block((void *)(& a),4UL);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
__e_acsl_full_init((void *)(& a));
return;
}
@@ -15,10 +16,10 @@ int main(void)
int __retres;
int *p;
int *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & a;
__e_acsl_full_init((void *)(& q));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
index 95cbaf4ad32..4027e89c9a0 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
@@ -1,9 +1,10 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
char *a;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
a = (char *)malloc((unsigned long)7);
__retres = 0;
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
index b4827659ce9..1dd16e99a60 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A = 0;
int B;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& B),4UL);
+ __e_acsl_store_block((void *)(& B),(size_t)4);
__e_acsl_full_init((void *)(& B));
- __e_acsl_store_block((void *)(& A),4UL);
+ __e_acsl_store_block((void *)(& A),(size_t)4);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -24,15 +25,15 @@ int main(void)
char *partsc;
char *partsi;
int dup[2];
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(d),16UL);
- __e_acsl_store_block((void *)(c),16UL);
- __e_acsl_store_block((void *)(& r),8UL);
- __e_acsl_store_block((void *)(& b),4UL);
- __e_acsl_store_block((void *)(& a),4UL);
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(d),(size_t)16);
+ __e_acsl_store_block((void *)(c),(size_t)16);
+ __e_acsl_store_block((void *)(& r),(size_t)8);
+ __e_acsl_store_block((void *)(& b),(size_t)4);
+ __e_acsl_store_block((void *)(& a),(size_t)4);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
p = & A;
__e_acsl_full_init((void *)(& q));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
index 3b9f5a76361..93c05dc46f7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int X = 0;
/*@ ensures X ≡ 3; */
int main(void);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
index b672dc9cb33..8994337c5ba 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
index 3d22d25c102..40d9186eb2f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A[10];
/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i + 1];
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
index a0c21dc4490..7acb15a3d46 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_6;
char *__gen_e_acsl_literal_string_5;
char *__gen_e_acsl_literal_string;
@@ -62,15 +63,15 @@ void __e_acsl_globals_init(void)
__e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,sizeof("bar"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
- __e_acsl_store_block((void *)(& l_str),8UL);
+ __e_acsl_store_block((void *)(& l_str),(size_t)8);
__e_acsl_full_init((void *)(& l_str));
- __e_acsl_store_block((void *)(& s_str),8UL);
+ __e_acsl_store_block((void *)(& s_str),(size_t)8);
__e_acsl_full_init((void *)(& s_str));
- __e_acsl_store_block((void *)(& S2),8UL);
+ __e_acsl_store_block((void *)(& S2),(size_t)8);
__e_acsl_full_init((void *)(& S2));
- __e_acsl_store_block((void *)(& S),8UL);
+ __e_acsl_store_block((void *)(& S),(size_t)8);
__e_acsl_full_init((void *)(& S));
- __e_acsl_store_block((void *)(& T),8UL);
+ __e_acsl_store_block((void *)(& T),(size_t)8);
__e_acsl_full_init((void *)(& T));
return;
}
@@ -79,9 +80,9 @@ int main(void)
{
int __retres;
char *SS;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& SS),8UL);
+ __e_acsl_store_block((void *)(& SS),(size_t)8);
__e_acsl_full_init((void *)(& SS));
SS = (char *)__gen_e_acsl_literal_string;
/*@ assert *(S + G2) ≡ 'o'; */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index ba7bf4973a9..11048b4a563 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -1,15 +1,17 @@
/* Generated by Frama-C */
+#include "stdlib.h"
+#include "string.h"
int main(int argc, char **argv)
{
int __retres;
int i;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
/*@ assert \valid(&argc); */
{
{
int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& argc),4UL);
- __e_acsl_store_block((void *)(& argv),8UL);
+ __e_acsl_store_block((void *)(& argc),(size_t)4);
+ __e_acsl_store_block((void *)(& argv),(size_t)8);
__gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int));
__e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
(char *)"\\valid(&argc)",10);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index af96acce120..7d0cc5b8503 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(int argc, char const **argv)
{
int __retres;
@@ -6,10 +7,10 @@ int main(int argc, char const **argv)
int res2;
char *p;
char *a;
- __e_acsl_memory_init(& argc,(char ***)(& argv),8UL);
- __e_acsl_store_block((void *)(& a),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& memptr),8UL);
+ __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
+ __e_acsl_store_block((void *)(& a),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& memptr),(size_t)8);
__e_acsl_full_init((void *)(& memptr));
memptr = (char **)malloc(sizeof(void *));
res2 = posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
index c8dd172c956..c9146a3bbc6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
@@ -1,10 +1,12 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
int main(int argc, char **argv)
{
int __retres;
char *a;
char *b;
- __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
a = (char *)malloc((unsigned long)7);
/*@ assert __e_acsl_heap_allocation_size ≡ 7; */
__e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,(char *)"Assertion",
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
index 902a394a333..6a5bdd3bf97 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
index 884218a24a6..411d9156a84 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
index fd2d4ee168d..e5b27f8a5c0 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
@@ -1,11 +1,12 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int A[4] = {1, 2, 3, 4};
int *PA;
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& PA),8UL);
+ __e_acsl_store_block((void *)(& PA),(size_t)8);
__e_acsl_full_init((void *)(& PA));
- __e_acsl_store_block((void *)(A),16UL);
+ __e_acsl_store_block((void *)(A),(size_t)16);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -19,14 +20,14 @@ int main(void)
int *pi;
char *p;
long *q;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& q),8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(& pi),8UL);
- __e_acsl_store_block((void *)(& pl),8UL);
- __e_acsl_store_block((void *)(& l),8UL);
- __e_acsl_store_block((void *)(a),16UL);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(& pi),(size_t)8);
+ __e_acsl_store_block((void *)(& pl),(size_t)8);
+ __e_acsl_store_block((void *)(& l),(size_t)8);
+ __e_acsl_store_block((void *)(a),(size_t)16);
PA = (int *)(& A);
/*@ assert \offset((int *)A) ≡ 0; */
{
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
index 8189abbe6a2..64f20c88581 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
enum bool {
false = 0,
true = 1
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
index 1147d35f960..dbbbe9eb942 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
@@ -6,10 +7,10 @@ int main(void)
int t[3];
int *p;
int k;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- __e_acsl_store_block((void *)(& p),8UL);
- __e_acsl_store_block((void *)(t),12UL);
- __e_acsl_store_block((void *)(& x),4UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ __e_acsl_store_block((void *)(t),(size_t)12);
+ __e_acsl_store_block((void *)(& x),(size_t)4);
__e_acsl_full_init((void *)(& x));
x = 1;
__e_acsl_initialize((void *)(t),sizeof(int));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
index 50bc97ca19e..773aa7e4a8c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int *A;
int *B;
void f(void)
@@ -11,7 +12,7 @@ void g(int *C, int *D)
{
/*@ assert \initialized(&C); */
{
- __e_acsl_store_block((void *)(& C),8UL);
+ __e_acsl_store_block((void *)(& C),(size_t)8);
__e_acsl_assert(1,(char *)"Assertion",(char *)"g",
(char *)"\\initialized(&C)",16);
}
@@ -21,9 +22,9 @@ void g(int *C, int *D)
void __e_acsl_globals_init(void)
{
- __e_acsl_store_block((void *)(& B),8UL);
+ __e_acsl_store_block((void *)(& B),(size_t)8);
__e_acsl_full_init((void *)(& B));
- __e_acsl_store_block((void *)(& A),8UL);
+ __e_acsl_store_block((void *)(& A),(size_t)8);
__e_acsl_full_init((void *)(& A));
return;
}
@@ -33,10 +34,10 @@ int main(void)
int __retres;
int *x;
int *y;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& y),8UL);
- __e_acsl_store_block((void *)(& x),8UL);
+ __e_acsl_store_block((void *)(& y),(size_t)8);
+ __e_acsl_store_block((void *)(& x),(size_t)8);
B = (int *)malloc(sizeof(int));
__e_acsl_full_init((void *)(& y));
y = (int *)malloc(sizeof(int));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 4b706094131..3d0ab3670f7 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
/*@ ensures \result ≡ (int)(\old(x) - \old(x)); */
int __gen_e_acsl_f(int x);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
index 7f98cb9e792..f5f08230c81 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
index c37843ee2b6..b61258b90e2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
@@ -1,4 +1,6 @@
/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
char *__gen_e_acsl_literal_string_2;
char *__gen_e_acsl_literal_string;
void __e_acsl_globals_init(void)
@@ -12,7 +14,7 @@ void __e_acsl_globals_init(void)
sizeof("/tmp/foo"));
__e_acsl_full_init((void *)__gen_e_acsl_literal_string);
__e_acsl_readonly((void *)__gen_e_acsl_literal_string);
- __e_acsl_store_block((void *)(& stdout),8UL);
+ __e_acsl_store_block((void *)(& stdout),(size_t)8);
__e_acsl_full_init((void *)(& stdout));
return;
}
@@ -22,9 +24,9 @@ int main(void)
int __retres;
FILE *f;
FILE *f2;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- __e_acsl_store_block((void *)(& f),8UL);
+ __e_acsl_store_block((void *)(& f),(size_t)8);
__e_acsl_full_init((void *)(& f));
f = stdout;
f2 = __gen_e_acsl_fopen(__gen_e_acsl_literal_string,
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
index 820ed8e2571..8f08c272ea1 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
index 18e197aaa6e..15d2e284227 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
int main(void)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
index d8f9bac5ef1..fcab2ee8a3f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
@@ -1,4 +1,5 @@
/* Generated by Frama-C */
+#include "stdlib.h"
typedef unsigned char uint8;
int main(void)
{
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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..672ba3db925 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:277:[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..d12021ab09a 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:277:[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:322:[value] warning: function realloc: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:337:[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:309:[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..672ba3db925 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:277:[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..672ba3db925 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:277:[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..672ba3db925 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:277:[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..9c737631c48 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:277:[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..a0a8836bb7a 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:277:[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..a0a8836bb7a 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:277:[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..ecb6e4154f0 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:277:[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..8992dcf45c9 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -2,12 +2,12 @@
[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/string.h:91:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/string.h:92:[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.
+FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
+FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
[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.
@@ -17,8 +17,8 @@ tests/runtime/mainargs.c:15:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_read(argv + argc);
tests/runtime/mainargs.c:16:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv + argc);
-FRAMAC_SHARE/libc/string.h:91:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:91:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
-FRAMAC_SHARE/libc/string.h:93:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:92:[value] warning: function strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
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..17ffda3bffd 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:277:[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:309:[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..9d3a78ec407 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:277:[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..672ba3db925 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:277:[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..672ba3db925 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:277:[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..5ca2406e948 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:277:[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..672ba3db925 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:277:[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..5ad5fd174a0 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:277:[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..a0a8836bb7a 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:277:[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..672ba3db925 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:277:[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..672ba3db925 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:277:[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..53d24663ffc 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:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+FRAMAC_SHARE/libc/stdlib.h:277:[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.
+FRAMAC_SHARE/libc/stdio.h:109:[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:10:[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 c33737e3cac..672ba3db925 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:277:[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..672ba3db925 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:277:[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..672ba3db925 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:277:[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..ed9c8d00310 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:277:[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..740a1e676f5 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:277:[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..bfca2174f9a 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:277:[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..e9ae42d4081 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:277:[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