From c57b6a7df0a7ddf11c7006298812a972f96d964a Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 8 Feb 2016 11:25:10 +0100
Subject: [PATCH] Fix test failures due to changes of frama-c output
---
.../tests/bts/oracle/bts1304.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1304.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1307.0.res.oracle | 12 +---
.../tests/bts/oracle/bts1307.1.res.oracle | 31 +----------
.../tests/bts/oracle/bts1324.0.res.oracle | 6 +-
.../tests/bts/oracle/bts1324.1.res.oracle | 19 +------
.../tests/bts/oracle/bts1326.0.res.oracle | 5 +-
.../tests/bts/oracle/bts1326.1.res.oracle | 16 +-----
.../tests/bts/oracle/bts1390.0.res.oracle | 11 +---
.../tests/bts/oracle/bts1390.1.res.oracle | 23 +-------
.../tests/bts/oracle/bts1399.0.res.oracle | 12 ++--
.../tests/bts/oracle/bts1399.1.res.oracle | 22 ++------
.../tests/bts/oracle/bts1478.0.res.oracle | 9 +--
.../tests/bts/oracle/bts1478.1.res.oracle | 13 +----
.../tests/bts/oracle/bts1700.0.res.oracle | 4 +-
.../tests/bts/oracle/bts1700.1.res.oracle | 4 +-
.../tests/bts/oracle/bts1717.0.res.oracle | 3 +-
.../tests/bts/oracle/bts1717.1.res.oracle | 3 +-
.../tests/bts/oracle/bts1718.0.res.oracle | 3 +-
.../tests/bts/oracle/bts1718.1.res.oracle | 3 +-
.../tests/bts/oracle/bts1837.0.res.oracle | 7 +--
.../tests/bts/oracle/bts1837.1.res.oracle | 7 +--
.../e-acsl-runtime/oracle/addrOf.0.res.oracle | 5 +-
.../e-acsl-runtime/oracle/addrOf.1.res.oracle | 5 +-
.../e-acsl-runtime/oracle/alias.0.res.oracle | 3 +-
.../e-acsl-runtime/oracle/alias.1.res.oracle | 3 +-
.../e-acsl-runtime/oracle/arith.0.res.oracle | 19 -------
.../e-acsl-runtime/oracle/arith.1.res.oracle | 51 +----------------
.../e-acsl-runtime/oracle/array.0.res.oracle | 6 +-
.../e-acsl-runtime/oracle/array.1.res.oracle | 10 +---
.../e-acsl-runtime/oracle/at.0.res.oracle | 23 +++-----
.../e-acsl-runtime/oracle/at.1.res.oracle | 32 +++--------
.../e-acsl-runtime/oracle/call.0.res.oracle | 8 +--
.../e-acsl-runtime/oracle/call.1.res.oracle | 8 +--
.../e-acsl-runtime/oracle/cast.0.res.oracle | 7 ---
.../e-acsl-runtime/oracle/cast.1.res.oracle | 15 +----
.../oracle/comparison.0.res.oracle | 18 ------
.../oracle/comparison.1.res.oracle | 27 +--------
.../oracle/compound_initializers.0.res.oracle | 14 +----
.../oracle/compound_initializers.1.res.oracle | 17 +-----
.../oracle/freeable.0.res.oracle | 2 +-
.../oracle/freeable.1.res.oracle | 2 +-
.../oracle/function_contract.0.res.oracle | 46 ----------------
.../oracle/function_contract.1.res.oracle | 55 +------------------
.../e-acsl-runtime/oracle/ghost.0.res.oracle | 4 +-
.../e-acsl-runtime/oracle/ghost.1.res.oracle | 7 +--
.../e-acsl-runtime/oracle/init.0.res.oracle | 6 +-
.../e-acsl-runtime/oracle/init.1.res.oracle | 6 +-
.../oracle/integer_constant.0.res.oracle | 11 +---
.../oracle/integer_constant.1.res.oracle | 11 +---
.../oracle/invariant.0.res.oracle | 3 +-
.../oracle/invariant.1.res.oracle | 6 +-
.../oracle/labeled_stmt.0.res.oracle | 4 --
.../oracle/labeled_stmt.1.res.oracle | 9 +--
.../e-acsl-runtime/oracle/lazy.0.res.oracle | 20 +------
.../e-acsl-runtime/oracle/lazy.1.res.oracle | 35 +++---------
.../oracle/linear_search.0.res.oracle | 24 ++++----
.../oracle/linear_search.1.res.oracle | 34 ++++--------
.../oracle/literal_string.0.res.oracle | 8 +--
.../oracle/literal_string.1.res.oracle | 11 +---
.../oracle/localvar.0.res.oracle | 7 +--
.../oracle/localvar.1.res.oracle | 7 +--
.../oracle/longlong.0.res.oracle | 21 +------
.../oracle/longlong.1.res.oracle | 20 +------
.../e-acsl-runtime/oracle/loop.0.res.oracle | 9 +--
.../e-acsl-runtime/oracle/loop.1.res.oracle | 25 +--------
.../oracle/mainargs.0.res.oracle | 22 ++++----
.../oracle/mainargs.1.res.oracle | 37 ++++---------
.../oracle/memsize.0.res.oracle | 9 ++-
.../oracle/memsize.1.res.oracle | 15 ++---
.../oracle/nested_code_annot.0.res.oracle | 2 -
.../oracle/nested_code_annot.1.res.oracle | 7 +--
.../e-acsl-runtime/oracle/not.0.res.oracle | 2 -
.../e-acsl-runtime/oracle/not.1.res.oracle | 7 +--
.../e-acsl-runtime/oracle/null.0.res.oracle | 2 -
.../e-acsl-runtime/oracle/null.1.res.oracle | 2 -
.../oracle/other_constants.0.res.oracle | 3 -
.../oracle/other_constants.1.res.oracle | 8 +--
.../e-acsl-runtime/oracle/ptr.0.res.oracle | 17 ++----
.../e-acsl-runtime/oracle/ptr.1.res.oracle | 35 ++----------
.../oracle/ptr_init.0.res.oracle | 10 +---
.../oracle/ptr_init.1.res.oracle | 10 +---
.../oracle/quantif.0.res.oracle | 17 +++---
.../oracle/quantif.1.res.oracle | 37 +++----------
.../e-acsl-runtime/oracle/result.0.res.oracle | 7 ---
.../e-acsl-runtime/oracle/result.1.res.oracle | 17 +-----
.../e-acsl-runtime/oracle/sizeof.0.res.oracle | 2 -
.../e-acsl-runtime/oracle/sizeof.1.res.oracle | 7 +--
.../e-acsl-runtime/oracle/stdout.0.res.oracle | 5 +-
.../e-acsl-runtime/oracle/stdout.1.res.oracle | 5 +-
.../oracle/stmt_contract.0.res.oracle | 1 -
.../oracle/stmt_contract.1.res.oracle | 10 +---
.../e-acsl-runtime/oracle/true.0.res.oracle | 2 -
.../e-acsl-runtime/oracle/true.1.res.oracle | 2 -
.../oracle/typedef.0.res.oracle | 2 -
.../oracle/typedef.1.res.oracle | 8 +--
.../e-acsl-runtime/oracle/valid.0.res.oracle | 27 ++-------
.../e-acsl-runtime/oracle/valid.1.res.oracle | 27 ++-------
.../oracle/valid_alias.0.res.oracle | 15 ++---
.../oracle/valid_alias.1.res.oracle | 19 ++-----
.../oracle/valid_in_contract.0.res.oracle | 7 +--
.../oracle/valid_in_contract.1.res.oracle | 7 +--
.../e-acsl-runtime/oracle/vector.0.res.oracle | 15 +++--
.../e-acsl-runtime/oracle/vector.1.res.oracle | 19 +++----
104 files changed, 239 insertions(+), 1092 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
index 6c989f972cd..c9fe27e8b98 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
@@ -14,9 +14,9 @@
tests/bts/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/bts/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
index 6c989f972cd..c9fe27e8b98 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
@@ -14,9 +14,9 @@
tests/bts/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/bts/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] warning: assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
index ec68e5b9442..c7d6f581b9c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
@@ -16,20 +16,12 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] using specification for function __valid_read
[value] user error: type long double not implemented. Using double instead
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
index 6291429ab43..3f9e8609612 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
@@ -16,45 +16,20 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/bts/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
[value] using specification for function __valid_read
[value] user error: type long double not implemented. Using double instead
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
-tests/bts/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
-tests/bts/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
-tests/bts/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid.
-tests/bts/bts1307.i:19:[value] Function bar: precondition got status valid.
-tests/bts/bts1307.i:20:[value] Function bar: precondition got status valid.
-tests/bts/bts1307.i:21:[value] Function bar: precondition got status valid.
-tests/bts/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/bts/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:25:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:25:[value] warning: function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
index 77eafde3d46..aab4aebb68a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
@@ -15,12 +15,8 @@
tests/bts/bts1324.i:8:[value] entering loop for the first time
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/bts/bts1324.i:15:[value] entering loop for the first time
-tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __delete_block
-tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
index 9d10a4d5f85..1b06bc092ff 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
@@ -13,36 +13,19 @@
[value] using specification for function __store_block
[value] using specification for function __initialize
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
tests/bts/bts1324.i:8:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_sub
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
tests/bts/bts1324.i:15:[value] entering loop for the first time
-tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
-tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
index ec79b9e70c9..dd5cc416639 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
@@ -13,11 +13,8 @@
[value] using specification for function __store_block
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
index 7b216576b83..3920964dc2c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
@@ -13,27 +13,13 @@
[value] using specification for function __store_block
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-tests/bts/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
index c24855a7c94..07aa4ab20e4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
@@ -18,19 +18,14 @@
tests/bts/bts1390.c:15:[value] entering loop for the first time
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/bts/bts1390.c:11:[value] entering loop for the first time
tests/bts/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
index 0dc7fb06cc0..4167be2b141 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
@@ -16,43 +16,26 @@
[value] using specification for function __full_init
[value] using specification for function __literal_string
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
tests/bts/bts1390.c:15:[value] entering loop for the first time
[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
tests/bts/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
tests/bts/bts1390.c:11:[value] entering loop for the first time
tests/bts/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
tests/bts/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
tests/bts/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+tests/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index 4773e0b0310..815257536b6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -35,22 +35,20 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
-tests/bts/bts1399.c:24:[value] Assertion got status valid.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialized
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index ff529ac753d..0e90a522d2c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -27,38 +27,26 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
-tests/bts/bts1399.c:24:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/bts/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
[value] using specification for function __initialized
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
index 615a1182b18..45f26ef331a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
@@ -14,16 +14,9 @@
global_i_ptr ∈ {{ &global_i }}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
-tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
-tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __valid
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid.
-tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid.
-tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
index ca69d07a0e9..3be1a2aeb0d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
@@ -14,23 +14,12 @@
global_i_ptr ∈ {{ &global_i }}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
-tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
-tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid.
-tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid.
-tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
index 983b2ddb8e8..b323b857618 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
@@ -11,12 +11,10 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/bts/bts1700.i:10:[value] Assertion got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
-tests/bts/bts1700.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
index 983b2ddb8e8..b323b857618 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
@@ -11,12 +11,10 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/bts/bts1700.i:10:[value] Assertion got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
-tests/bts/bts1700.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
index eb2f883c086..2c04f4eb44e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
@@ -12,11 +12,10 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1717.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
index eb2f883c086..2c04f4eb44e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
@@ -12,11 +12,10 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1717.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
index a4617af6a66..2c04f4eb44e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
@@ -12,11 +12,10 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1718.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
index a4617af6a66..2c04f4eb44e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
@@ -12,11 +12,10 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/bts/bts1718.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
index cefeb276e61..82924e5df2d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
@@ -18,17 +18,12 @@
[value] using specification for function __full_init
[value] using specification for function __literal_string
tests/bts/bts1837.i:19:[value] entering loop for the first time
-tests/bts/bts1837.i:21:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1837.i:22:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid
[value] using specification for function __delete_block
tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
-tests/bts/bts1837.i:11:[value] Assertion got status valid.
-tests/bts/bts1837.i:12:[value] Assertion got status valid.
-tests/bts/bts1837.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
index cefeb276e61..82924e5df2d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
@@ -18,17 +18,12 @@
[value] using specification for function __full_init
[value] using specification for function __literal_string
tests/bts/bts1837.i:19:[value] entering loop for the first time
-tests/bts/bts1837.i:21:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/bts/bts1837.i:22:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid
[value] using specification for function __delete_block
tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1;
-tests/bts/bts1837.i:11:[value] Assertion got status valid.
-tests/bts/bts1837.i:12:[value] Assertion got status valid.
-tests/bts/bts1837.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle
index 4bcd25d2c38..49684ab1126 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle
@@ -12,12 +12,9 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
-tests/e-acsl-runtime/addrOf.i:18:[value] Assertion got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index 4bcd25d2c38..49684ab1126 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -12,12 +12,9 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
-tests/e-acsl-runtime/addrOf.i:18:[value] Assertion got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle
index e16771bba8f..0c77241ff78 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle
@@ -14,9 +14,8 @@
[value] using specification for function __full_init
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/alias.i:16:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
index e16771bba8f..0c77241ff78 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle
@@ -14,9 +14,8 @@
[value] using specification for function __full_init
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/alias.i:16:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle
index 9e13e05e51d..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle
@@ -10,24 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/arith.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:17:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:18:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:20:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:22:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:23:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:25:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:27:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:28:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index 1f09cb63b6e..ffd0bd8013c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -10,67 +10,18 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_neg
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:137:[value] Function __gmpz_neg: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:138:[value] Function __gmpz_neg: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/arith.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:14:[value] Assertion got status valid.
[value] using specification for function __gmpz_com
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:182:[value] Function __gmpz_com: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:183:[value] Function __gmpz_com: precondition got status valid.
-tests/e-acsl-runtime/arith.i:16:[value] Assertion got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/arith.i:17:[value] Assertion got status valid.
[value] using specification for function __gmpz_sub
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
-tests/e-acsl-runtime/arith.i:18:[value] Assertion got status valid.
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
-tests/e-acsl-runtime/arith.i:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:19:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
-tests/e-acsl-runtime/arith.i:20:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_str
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid.
-tests/e-acsl-runtime/arith.i:20:[value] Assertion 'E_ACSL' got status valid.
-tests/e-acsl-runtime/arith.i:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:21:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_r
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid.
-tests/e-acsl-runtime/arith.i:22:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:22:[value] Assertion 'E_ACSL' got status valid.
-tests/e-acsl-runtime/arith.i:23:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:23:[value] Assertion 'E_ACSL' got status valid.
-tests/e-acsl-runtime/arith.i:25:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:27:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:28:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
-tests/e-acsl-runtime/arith.i:33:[value] Assertion 'E_ACSL' got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle
index ee1253b86e5..8f4a3d3b726 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle
@@ -14,8 +14,8 @@
T2[0..3] ∈ {0}
tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time
tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/array.i:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/array.i:15:[value] warning: assertion got status unknown.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/array.i:16:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index f776ff5e949..eb2477f723c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -14,15 +14,11 @@
T2[0..3] ∈ {0}
tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time
tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/array.i:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/array.i:15:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
+tests/e-acsl-runtime/array.i:16:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle
index 96720f05fdb..2f339588463 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle
@@ -14,30 +14,21 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __delete_block
-tests/e-acsl-runtime/at.i:40:[value] Function h: postcondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/at.i:40:[value] Function __e_acsl_h: postcondition got status valid.
-tests/e-acsl-runtime/at.i:48:[value] Assertion got status valid.
-tests/e-acsl-runtime/at.i:13:[value] Assertion got status valid.
tests/e-acsl-runtime/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:14:[value] Assertion got status unknown.
-tests/e-acsl-runtime/at.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/at.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/at.i:9:[value] Function f: postcondition got status valid.
-tests/e-acsl-runtime/at.i:9:[value] Function __e_acsl_f: postcondition got status valid.
+tests/e-acsl-runtime/at.i:14:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:53:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:53:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:53:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:54:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:54:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:54:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:55:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:55:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:55:[value] warning: assertion got status unknown.
[value] using specification for function __initialize
[value] using specification for function __valid_read
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:32:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:34:[value] warning: assertion got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index 6ba9bf6d9e7..05a4c55b977 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -14,45 +14,27 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __delete_block
-tests/e-acsl-runtime/at.i:40:[value] Function h: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/at.i:40:[value] Function __e_acsl_h: postcondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] using specification for function __gmpz_init_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:46:[value] Function __gmpz_init_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:47:[value] Function __gmpz_init_set: precondition got status valid.
-tests/e-acsl-runtime/at.i:48:[value] Assertion got status valid.
-tests/e-acsl-runtime/at.i:13:[value] Assertion got status valid.
tests/e-acsl-runtime/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:14:[value] Assertion got status unknown.
-tests/e-acsl-runtime/at.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/at.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/at.i:9:[value] Function f: postcondition got status valid.
-tests/e-acsl-runtime/at.i:9:[value] Function __e_acsl_f: postcondition got status valid.
+tests/e-acsl-runtime/at.i:14:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:53:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:53:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:53:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:54:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:54:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:54:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:55:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:55:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:55:[value] warning: assertion got status unknown.
[value] using specification for function __initialize
[value] using specification for function __valid_read
tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:32:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
+tests/e-acsl-runtime/at.i:34:[value] warning: assertion got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
index 5b143f91676..faed34d88a8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
@@ -27,14 +27,12 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
[value] using specification for function __initialize
-tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 16b7e91901b..67d328ebf2e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -23,14 +23,12 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
[value] using specification for function __initialize
-tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle
index 61fa2dd0ad7..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle
@@ -10,12 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/cast.i:12:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/cast.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/cast.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/cast.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index ec9a3771068..1b00f8980af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -10,25 +10,12 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/cast.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/cast.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/cast.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/cast.i:16:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
-tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_str
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle
index f25ea08678e..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle
@@ -10,23 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/comparison.i:9:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/comparison.i:10:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:11:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:12:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:17:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:18:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:20:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:22:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:24:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:25:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:26:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:27:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index 738cbde7a5c..7f46b34e22a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -10,36 +10,11 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/comparison.i:9:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/comparison.i:10:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:11:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:12:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:14:[value] Assertion got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/comparison.i:17:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:18:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:20:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:22:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:24:[value] Assertion got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_neg
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:137:[value] Function __gmpz_neg: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:138:[value] Function __gmpz_neg: precondition got status valid.
-tests/e-acsl-runtime/comparison.i:25:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:26:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:27:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
-tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
index f8184dd9d7f..22916af593b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle
@@ -30,23 +30,11 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-tests/e-acsl-runtime/compound_initializers.c:35:[value] Assertion got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/compound_initializers.c:36:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialized
[value] using specification for function __valid_read
-tests/e-acsl-runtime/compound_initializers.c:37:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:38:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:39:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:40:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:41:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:42:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:43:[value] Assertion got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/compound_initializers.c:44:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:45:[value] Assertion got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle
index f170948d04d..033d0a1dab0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle
@@ -30,29 +30,14 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-tests/e-acsl-runtime/compound_initializers.c:35:[value] Assertion got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/compound_initializers.c:36:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialized
[value] using specification for function __valid_read
-tests/e-acsl-runtime/compound_initializers.c:37:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:38:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:39:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:40:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:41:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:42:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:43:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/compound_initializers.c:44:[value] Assertion got status valid.
-tests/e-acsl-runtime/compound_initializers.c:45:[value] Assertion got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
index 690693003a4..dfd6c7dcbab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle
@@ -32,7 +32,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of
argument (void *)p
tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
index 2f31a65647b..48a19d4a6d1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle
@@ -24,7 +24,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of
argument (void *)p
tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle
index 1bbc0c9654d..1e2b88ff34e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle
@@ -12,51 +12,5 @@
__memory_size ∈ [--..--]
X ∈ {0}
Y ∈ {2}
-tests/e-acsl-runtime/function_contract.i:10:[value] Function f: postcondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:10:[value] Function __e_acsl_f: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:14:[value] Function g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:15:[value] Function g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:14:[value] Function __e_acsl_g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:15:[value] Function __e_acsl_g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:19:[value] Function __e_acsl_h: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:19:[value] Function h: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:23:[value] Function __e_acsl_i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:24:[value] Function __e_acsl_i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:23:[value] Function i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:24:[value] Function i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:29:[value] Function __e_acsl_j, behavior b1: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:32:[value] Function __e_acsl_j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:33:[value] Function __e_acsl_j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:29:[value] Function j, behavior b1: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:32:[value] Function j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:33:[value] Function j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumes got status invalid; precondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumes got status invalid; precondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid.
-tests/e-acsl-runtime/function_contract.i:49:[value] Function l: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:49:[value] Function __e_acsl_l: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; postcondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:62:[value] Function m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:63:[value] Function m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; postcondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:62:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:63:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:67:[value] Function __e_acsl_n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:68:[value] Function __e_acsl_n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:67:[value] Function n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:68:[value] Function n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index 2cc6f18177e..a5904b43663 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -12,64 +12,11 @@
__memory_size ∈ [--..--]
X ∈ {0}
Y ∈ {2}
-tests/e-acsl-runtime/function_contract.i:10:[value] Function f: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:10:[value] Function __e_acsl_f: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:14:[value] Function g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:15:[value] Function g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:14:[value] Function __e_acsl_g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:15:[value] Function __e_acsl_g: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:19:[value] Function __e_acsl_h: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:19:[value] Function h: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:23:[value] Function __e_acsl_i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:24:[value] Function __e_acsl_i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:23:[value] Function i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:24:[value] Function i: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:29:[value] Function __e_acsl_j, behavior b1: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:32:[value] Function __e_acsl_j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:33:[value] Function __e_acsl_j, behavior b2: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:29:[value] Function j, behavior b1: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:32:[value] Function j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:33:[value] Function j, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumes got status invalid; precondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumes got status invalid; precondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid.
-tests/e-acsl-runtime/function_contract.i:49:[value] Function l: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:49:[value] Function __e_acsl_l: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; postcondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:62:[value] Function m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:63:[value] Function m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; postcondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:62:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:63:[value] Function __e_acsl_m, behavior b2: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:67:[value] Function __e_acsl_n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:68:[value] Function __e_acsl_n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:67:[value] Function n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:68:[value] Function n: precondition got status valid.
-tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated.
-tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid.
-tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle
index 97bb0712a03..7cff290b275 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle
@@ -17,11 +17,9 @@
[value] using specification for function __initialize
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid
-tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid.
[value] using specification for function __initialized
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
index 2cee1d69b38..91c132e3a5a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -17,16 +17,11 @@
[value] using specification for function __initialize
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid
-tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle
index d0c22cc84bc..d19125c9928 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle
@@ -14,13 +14,9 @@
b ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid.
[value] using specification for function __initialized
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
index d0c22cc84bc..d19125c9928 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
@@ -14,13 +14,9 @@
b ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid.
[value] using specification for function __initialized
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle
index f7340321cd0..294e77a267c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle
@@ -10,18 +10,9 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid.
-tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
-tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_str
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index db4cb25cd18..dd977035dae 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -10,19 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid.
-tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_str
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid.
-tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle
index ada60090903..c23dbf0116b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle
@@ -12,7 +12,6 @@
__memory_size ∈ [--..--]
tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index adb93500ead..097c17aa47d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -12,13 +12,9 @@
__memory_size ∈ [--..--]
tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle
index ea82cb27ffb..6dce2057d11 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle
@@ -11,9 +11,5 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
X ∈ {0}
-tests/e-acsl-runtime/labeled_stmt.i:12:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondition got status valid.
-tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index 34d08a38a82..1e90496d9c4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -11,16 +11,9 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
X ∈ {0}
-tests/e-acsl-runtime/labeled_stmt.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondition got status valid.
-tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle
index 67f5d8e0435..044d08c5d63 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle
@@ -10,22 +10,8 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/lazy.i:11:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/lazy.i:12:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:17:[value] Assertion got status unknown.
-tests/e-acsl-runtime/lazy.i:18:[value] Assertion got status unknown.
-tests/e-acsl-runtime/lazy.i:19:[value] Assertion got status unknown.
-tests/e-acsl-runtime/lazy.i:22:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:23:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:26:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:27:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:28:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
+tests/e-acsl-runtime/lazy.i:17:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/lazy.i:18:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/lazy.i:19:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index 55a6dc8a5ed..9be75f5ecfa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -10,38 +10,17 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/lazy.i:11:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/lazy.i:12:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/e-acsl-runtime/lazy.i:12:[value] Assertion 'E_ACSL' got status invalid (stopping propagation).
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/lazy.i:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:14:[value] Assertion 'E_ACSL' got status invalid (stopping propagation).
-tests/e-acsl-runtime/lazy.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:16:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:16:[value] Assertion 'E_ACSL' got status invalid (stopping propagation).
-tests/e-acsl-runtime/lazy.i:17:[value] Assertion got status unknown.
-tests/e-acsl-runtime/lazy.i:18:[value] Assertion got status unknown.
-tests/e-acsl-runtime/lazy.i:19:[value] Assertion got status unknown.
-tests/e-acsl-runtime/lazy.i:22:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:23:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:26:[value] Assertion got status valid.
+tests/e-acsl-runtime/lazy.i:12:[value] warning: assertion 'E_ACSL' got status invalid (stopping propagation).
+tests/e-acsl-runtime/lazy.i:14:[value] warning: assertion 'E_ACSL' got status invalid (stopping propagation).
+tests/e-acsl-runtime/lazy.i:16:[value] warning: assertion 'E_ACSL' got status invalid (stopping propagation).
+tests/e-acsl-runtime/lazy.i:17:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/lazy.i:18:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/lazy.i:19:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:46:[value] Function __gmpz_init_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:47:[value] Function __gmpz_init_set: precondition got status valid.
-tests/e-acsl-runtime/lazy.i:27:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:28:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
-tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
index 7b2aac32b7a..0c2754d6b55 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
@@ -12,24 +12,20 @@
__memory_size ∈ [--..--]
A[0..9] ∈ {0}
tests/e-acsl-runtime/linear_search.i:30:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:9:[value] Function __e_acsl_search: precondition got status unknown.
+tests/e-acsl-runtime/linear_search.i:9:[value] warning: function __e_acsl_search: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
+tests/e-acsl-runtime/linear_search.i:9:[value] warning: function search: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
+tests/e-acsl-runtime/linear_search.i:20:[value] warning: loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
-tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
+tests/e-acsl-runtime/linear_search.i:12:[value] warning: function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] warning: function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] warning: function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] warning: function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:33:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/linear_search.i:36:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index feccbdb6ddb..3fc3a773adc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -12,47 +12,33 @@
__memory_size ∈ [--..--]
A[0..9] ∈ {0}
tests/e-acsl-runtime/linear_search.i:30:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:9:[value] Function __e_acsl_search: precondition got status unknown.
+tests/e-acsl-runtime/linear_search.i:9:[value] warning: function __e_acsl_search: precondition got status unknown.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_2 < 10;
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index. assert __e_acsl_3 < 10;
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index. assert __e_acsl_j_4 < 10;
tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index. assert __e_acsl_j_2 < 10;
-tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown.
+tests/e-acsl-runtime/linear_search.i:9:[value] warning: function search: precondition got status unknown.
tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_2 < 10;
-tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
+tests/e-acsl-runtime/linear_search.i:20:[value] warning: loop invariant got status unknown.
tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
-tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
+tests/e-acsl-runtime/linear_search.i:12:[value] warning: function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] warning: function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] warning: function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] warning: function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:33:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/linear_search.i:36:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
index c04d9a8f696..db70db6e090 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle
@@ -24,17 +24,11 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialized
-tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
-tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
[value] using specification for function __valid
-tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index dcdcf9a030e..dcc82287939 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -24,23 +24,14 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
[value] using specification for function __initialized
-tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
[value] using specification for function __valid_read
-tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
[value] using specification for function __valid
-tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
index 2e97f3d935b..512eccd64de 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
@@ -27,13 +27,12 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialize
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 7bcb0d29927..954b596c456 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -23,13 +23,12 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __initialize
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
index 62d88b89151..05f59d98e5e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle
@@ -18,35 +18,18 @@ tests/e-acsl-runtime/longlong.i:11:[value] warning: recursive call during value
[value] using specification for function my_pow
tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
-tests/e-acsl-runtime/longlong.i:19:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_import
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] Function __gmpz_import: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown.
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-tests/e-acsl-runtime/longlong.i:19:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison.
assert \pointer_comparable((void *)__e_acsl_4, (void *)1);
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
index 5fd7d5e29db..382e1ff4d99 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
@@ -18,33 +18,17 @@ tests/e-acsl-runtime/longlong.i:11:[value] warning: recursive call during value
[value] using specification for function my_pow
tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp;
tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647;
-tests/e-acsl-runtime/longlong.i:19:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_import
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] Function __gmpz_import: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown.
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-tests/e-acsl-runtime/longlong.i:19:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid.
tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison.
assert \pointer_comparable((void *)__e_acsl_eq, (void *)0);
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle
index 37df3cbad2f..34f20cf19c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle
@@ -11,15 +11,10 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/loop.i:10:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/loop.i:17:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/loop.i:19:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/loop.i:21:[value] Loop invariant got status unknown.
+tests/e-acsl-runtime/loop.i:21:[value] warning: loop invariant got status unknown.
[value] Semantic level unrolling superposing up to 100 states
tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value.
assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
-tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
index 671b142c038..2a9a74a05aa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
@@ -11,24 +11,14 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/loop.i:10:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/loop.i:17:[value] Loop invariant got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
tests/e-acsl-runtime/loop.i:21:[value] completely invalid value in evaluation of
argument (long)t[__e_acsl_k_2][__e_acsl_l_2]
tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_k_2 < 10;
@@ -36,21 +26,12 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index.
tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value.
assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]);
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/loop.i:19:[value] Loop invariant got status valid.
-tests/e-acsl-runtime/loop.i:21:[value] Loop invariant got status unknown.
+tests/e-acsl-runtime/loop.i:21:[value] warning: loop invariant got status unknown.
tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_k_4 < 10;
tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_l_4 < 15;
tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value.
assert \initialized(&t[__e_acsl_k_4][__e_acsl_l_4]);
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
[value] Semantic level unrolling superposing up to 100 states
tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
index db7d99e671c..570e5a2cd7d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle
@@ -20,31 +20,29 @@ FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __init_args
-tests/e-acsl-runtime/mainargs.c:12:[value] Assertion got status valid.
[value] using specification for function __store_block
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/mainargs.c:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/mainargs.c:14:[value] Assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/mainargs.c:14:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:14:[value] entering loop for the first time
-tests/e-acsl-runtime/mainargs.c:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown.
[value] using specification for function __block_length
-tests/e-acsl-runtime/mainargs.c:17:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:17:[value] warning: assertion got status unknown.
[value] using specification for function __valid_read
tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
-tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:18:[value] warning: assertion got status unknown.
[value] using specification for function __initialized
tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc);
tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
-FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:91:[value] warning: function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
[value] using specification for function strlen
-FRAMAC_SHARE/libc/string.h:91:[value] Function 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:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown.
-tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
+FRAMAC_SHARE/libc/string.h:93:[value] warning: function __e_acsl_strlen: postcondition got status unknown.
+tests/e-acsl-runtime/mainargs.c:21:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:22:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
index d3b2a7b1d26..2a1ee9c62a4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle
@@ -20,55 +20,38 @@ FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __init_args
-tests/e-acsl-runtime/mainargs.c:12:[value] Assertion got status valid.
[value] using specification for function __store_block
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/mainargs.c:13:[value] Assertion got status valid.
-tests/e-acsl-runtime/mainargs.c:14:[value] Assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/mainargs.c:14:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/mainargs.c:14:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/mainargs.c:15:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown.
[value] using specification for function __block_length
[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
-tests/e-acsl-runtime/mainargs.c:17:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:17:[value] warning: assertion got status unknown.
[value] using specification for function __valid_read
tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
-tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:18:[value] warning: assertion got status unknown.
[value] using specification for function __initialized
tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc);
tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time
-FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
+FRAMAC_SHARE/libc/string.h:91:[value] warning: function __e_acsl_strlen: precondition 'valid_string_src' got status unknown.
[value] using specification for function strlen
-FRAMAC_SHARE/libc/string.h:91:[value] Function 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:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown.
-tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown.
-tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown.
+FRAMAC_SHARE/libc/string.h:93:[value] warning: function __e_acsl_strlen: postcondition got status unknown.
+tests/e-acsl-runtime/mainargs.c:21:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/mainargs.c:22:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle
index 4769e9abc32..615aab08721 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle
@@ -55,10 +55,9 @@ FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification
[value] using specification for function __full_init
[value] using specification for function __malloc
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/memsize.c:24:[value] Assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/memsize.c:24:[value] warning: assertion got status unknown.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/memsize.c:26:[value] Assertion got status invalid (stopping propagation).
+tests/e-acsl-runtime/memsize.c:26:[value] warning: assertion got status invalid (stopping propagation).
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle
index b5e711cfb61..d832fd1ab14 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle
@@ -43,19 +43,14 @@ FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification
[value] using specification for function __full_init
[value] using specification for function __malloc
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/memsize.c:24:[value] Assertion got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/memsize.c:24:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/memsize.c:26:[value] Assertion got status invalid (stopping propagation).
+tests/e-acsl-runtime/memsize.c:26:[value] warning: assertion got status invalid (stopping propagation).
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle
index 151f864ecdd..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index 8a822252367..af524ffc3d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -10,14 +10,9 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle
index c4513a0cf3e..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index 57e6831e42f..af524ffc3d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -10,14 +10,9 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle
index 6d317b9c751..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
index 6d317b9c751..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle
index dec8067549f..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle
@@ -10,8 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/other_constants.i:12:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 4c6b098dd08..af524ffc3d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -10,15 +10,9 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/other_constants.i:12:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle
index 3815dcb62e0..b71f628f999 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle
@@ -13,23 +13,14 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __initialize
-tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:16:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/ptr.i:18:[value] entering loop for the first time
-tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown.
-tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
-tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status unknown.
-tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr.i:19:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/ptr.i:20:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/ptr.i:21:[value] warning: assertion got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index c2049ced1b9..f70ee1b37e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -13,50 +13,23 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __initialize
-tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:14:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:15:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:16:[value] Assertion got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:16:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
tests/e-acsl-runtime/ptr.i:16:[kernel] warning: accessing out of bounds index. assert __e_acsl_9 < 3;
tests/e-acsl-runtime/ptr.i:18:[value] entering loop for the first time
-tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status valid.
[value] using specification for function __gmpz_sub
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
tests/e-acsl-runtime/ptr.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_15 < 3;
-tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown.
-tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
-tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status unknown.
-tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr.i:19:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/ptr.i:20:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/ptr.i:21:[value] warning: assertion got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle
index f4305944774..21b5d6c647f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle
@@ -29,14 +29,10 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
[value] using specification for function __full_init
[value] using specification for function __malloc
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
[value] using specification for function __initialized
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index c4219110595..2e95ba4b034 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -25,14 +25,10 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
[value] using specification for function __full_init
[value] using specification for function __malloc
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
[value] using specification for function __initialized
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle
index 953488ee27e..e0ebf45e128 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle
@@ -10,22 +10,21 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/quantif.i:11:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:11:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:11:[value] entering loop for the first time
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/quantif.i:12:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:12:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:12:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:13:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:13:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:14:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:14:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:14:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:18:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:18:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:18:[value] entering loop for the first time
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/quantif.i:23:[value] Assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/quantif.i:23:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:27:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:27:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index f57dd54e53f..5f380012785 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -10,51 +10,30 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/quantif.i:11:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:11:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_set
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
tests/e-acsl-runtime/quantif.i:11:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/quantif.i:12:[value] Assertion got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/quantif.i:12:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:12:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:13:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:13:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:13:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:14:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:14:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:14:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:18:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:18:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:18:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:23:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:23:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:27:[value] Assertion got status unknown.
+tests/e-acsl-runtime/quantif.i:27:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:28:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_r
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid.
tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
-tests/e-acsl-runtime/quantif.i:28:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_mul
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle
index 7ffb06bab75..053606fa32a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle
@@ -11,12 +11,5 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
Y ∈ {1}
-tests/e-acsl-runtime/result.i:7:[value] Function f: postcondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/result.i:7:[value] Function __e_acsl_f: postcondition got status valid.
-tests/e-acsl-runtime/result.i:18:[value] Function g: postcondition got status valid.
-tests/e-acsl-runtime/result.i:18:[value] Function __e_acsl_g: postcondition got status valid.
-tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status valid.
-tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index 768f090efb6..f17905f024e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -11,27 +11,12 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
Y ∈ {1}
-tests/e-acsl-runtime/result.i:7:[value] Function f: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_sub
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
[value] using specification for function __gmpz_get_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/result.i:7:[value] Function __e_acsl_f: postcondition got status valid.
-tests/e-acsl-runtime/result.i:18:[value] Function g: postcondition got status valid.
-tests/e-acsl-runtime/result.i:18:[value] Function __e_acsl_g: postcondition got status valid.
-tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status valid.
-tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle
index 3d936884430..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index 505160e67de..af524ffc3d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -10,14 +10,9 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
index fb49c3698c3..a0141f070c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
@@ -47,10 +47,9 @@ FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function
[value] using specification for function __full_init
[value] using specification for function __literal_string
[value] using specification for function fopen
-FRAMAC_SHARE/libc/stdio.h:106:[value] Function __e_acsl_fopen: postcondition got status valid.
-tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown.
+tests/e-acsl-runtime/stdout.c:13:[value] warning: assertion got status unknown.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
index c0cb27bc5fd..764e042f2f3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -47,10 +47,9 @@ FRAMAC_SHARE/libc/stdio.h:106:[e-acsl] warning: E-ACSL construct `logic function
[value] using specification for function __full_init
[value] using specification for function __literal_string
[value] using specification for function fopen
-FRAMAC_SHARE/libc/stdio.h:106:[value] Function __e_acsl_fopen: postcondition got status valid.
-tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown.
+tests/e-acsl-runtime/stdout.c:13:[value] warning: assertion got status unknown.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle
index 7e1ef6d4aa6..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle
@@ -11,5 +11,4 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index c59e20f10fd..ffdab4d2252 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -11,18 +11,10 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
[value] using specification for function __gmpz_add
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle
index 549d5a145b5..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
index 549d5a145b5..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle
index 3e13beeb9f8..f0d9dbf6c71 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle
@@ -10,7 +10,5 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index eff640e073c..b6b4bb04ed9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -10,16 +10,10 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
-tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_ui
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
index 56aa4ebae24..444b435a3dc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
@@ -35,43 +35,26 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
Z ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
-tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid.
-tests/e-acsl-runtime/valid.c:19:[value] Assertion got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
-tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
-tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __valid_read
-tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
argument (void *)a
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index e45b62a3e03..15bf91ef5f0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -27,43 +27,26 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
Z ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid.
-tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid.
-tests/e-acsl-runtime/valid.c:19:[value] Assertion got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid.
-tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid.
-tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __valid_read
-tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
argument (void *)a
tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
-tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid.
-tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
index e867ea1e46b..ee78cd2f531 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
@@ -32,30 +32,25 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
-tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
[value] using specification for function __valid
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __valid_read
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
argument (void *)a
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 250286e8054..abe5975be18 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -24,36 +24,27 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
-tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
[value] using specification for function __valid
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
-tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
argument (void *)a
tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle
index 47b252b6e28..3ae32e3ef4f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle
@@ -15,16 +15,11 @@
[value] using specification for function __initialized
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of
argument (void *)l->next
tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
[value] using specification for function __full_init
[value] using specification for function __delete_block
-tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 47b252b6e28..3ae32e3ef4f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -15,16 +15,11 @@
[value] using specification for function __initialized
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of
argument (void *)l->next
tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
[value] using specification for function __full_init
[value] using specification for function __delete_block
-tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
-tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
index a4d6c584761..e1d8fe9f804 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
@@ -34,26 +34,25 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
LAST ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __initialize
-tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
-tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:29:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/vector.c:30:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 449c89e8f5e..0055ceb37e7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -26,33 +26,28 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
LAST ∈ {0}
[value] using specification for function __store_block
[value] using specification for function __initialize
-tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
[value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time
-tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:29:[value] warning: assertion got status unknown.
+tests/e-acsl-runtime/vector.c:30:[value] warning: assertion got status unknown.
tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST);
[value] using specification for function __gmpz_init_set_si
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_clear
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown.
[value] using specification for function __freeable
:0:[value] Assigning imprecise value to __e_acsl_implies.
The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
-FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
--
GitLab