From 6306695fe8aa214fc3f9521e1ada104684a783dd Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 2 Aug 2017 10:59:36 +0200
Subject: [PATCH] Update test oracle output as per renamed files in RTL
---
.../e-acsl/tests/bts/oracle/bts1304.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1307.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1324.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1326.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1390.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1399.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1478.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1700.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1717.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1718.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1740.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts1837.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2191.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2192.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2231.res.oracle | 2 +-
.../e-acsl/tests/bts/oracle/bts2252.res.oracle | 2 +-
.../tests/full-mmodel/oracle/addrOf.0.res.oracle | 2 +-
.../tests/full-mmodel/oracle/addrOf.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/arith.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/arith.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/array.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/array.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/at.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/at.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/cast.1.res.oracle | 2 +-
.../tests/gmp/oracle/comparison.1.res.oracle | 2 +-
.../gmp/oracle/integer_constant.0.res.oracle | 2 +-
.../gmp/oracle/integer_constant.1.res.oracle | 2 +-
.../tests/gmp/oracle/longlong.0.res.oracle | 2 +-
.../tests/gmp/oracle/longlong.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/not.1.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/quantif.0.res.oracle | 2 +-
.../e-acsl/tests/gmp/oracle/quantif.1.res.oracle | 2 +-
.../e-acsl/tests/no-main/oracle/empty.res.oracle | 2 +-
.../tests/reject/oracle/quantif.res.oracle | 2 +-
.../tests/runtime/oracle/addrOf.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/alias.res.oracle | 2 +-
.../tests/runtime/oracle/base_addr.res.oracle | 2 +-
.../tests/runtime/oracle/block_length.res.oracle | 2 +-
.../tests/runtime/oracle/block_valid.res.oracle | 2 +-
.../tests/runtime/oracle/bypassed_var.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/call.res.oracle | 2 +-
.../oracle/compound_initializers.res.oracle | 2 +-
.../tests/runtime/oracle/ctype_macros.res.oracle | 2 +-
.../tests/runtime/oracle/early_exit.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/errno.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/ghost.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/goto.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/init.res.oracle | 2 +-
.../tests/runtime/oracle/initialized.res.oracle | 2 +-
.../runtime/oracle/linear_search.res.oracle | 2 +-
.../runtime/oracle/literal_string.res.oracle | 2 +-
.../tests/runtime/oracle/local_goto.res.oracle | 2 +-
.../tests/runtime/oracle/local_init.res.oracle | 2 +-
.../tests/runtime/oracle/localvar.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/loop.res.oracle | 2 +-
.../tests/runtime/oracle/mainargs.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/ptr.res.oracle | 2 +-
.../tests/runtime/oracle/ptr_init.res.oracle | 2 +-
.../tests/runtime/oracle/stdout.res.oracle | 2 +-
.../e-acsl/tests/runtime/oracle/valid.res.oracle | 2 +-
.../tests/runtime/oracle/valid_alias.res.oracle | 2 +-
.../runtime/oracle/valid_in_contract.res.oracle | 2 +-
.../tests/runtime/oracle/vector.res.oracle | 2 +-
.../tests/special/oracle/builtin.0.res.oracle | 2 +-
.../tests/special/oracle/builtin.1.res.oracle | 2 +-
.../tests/temporal/oracle/gen_t_global_init.c | 16 ++++++++--------
.../tests/temporal/oracle/gen_t_local_init.c | 14 +++++++-------
68 files changed, 81 insertions(+), 81 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
index e55627d2104..43a3d2ec488 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index 20c42f8719d..b829e722be5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -4,5 +4,5 @@ tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
tests/bts/bts1307.i:23:[e-acsl] warning: approximating a real number by a float
tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] user error: type long double not implemented. Using double instead
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
index be6837d8201..44f7f5d0c9e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
index 6aad1d366cd..46b779f7c6a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
tests/bts/bts1740.i:16:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
index 1cf61110037..ebb02534e87 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i - 1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
index fb7dff04362..133c3ba4e22 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
@@ -3,4 +3,4 @@
the generated program may miss memory instrumentation
if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
index 0853a547f98..991489b0c93 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts2231.i:8:[value] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index 1ca67523161..5d7898ca10e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -2,5 +2,5 @@ tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Ol
[e-acsl] beginning translation.
tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
index 170fe608aec..08feacb630f 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
@@ -21,7 +21,7 @@
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_initialized
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
index 170fe608aec..08feacb630f 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
@@ -21,7 +21,7 @@
[value] using specification for function __e_acsl_full_init
[value] using specification for function __e_acsl_initialized
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
index c9563f7451d..7a7fac17de4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
@@ -22,7 +22,7 @@
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __gmpz_init
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
[value] using specification for function __gmpz_get_si
[value] using specification for function __gmpz_clear
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
index 2c81b49856d..d71a528c82c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
@@ -22,7 +22,7 @@
[value] using specification for function __gmpz_neg
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_com
[value] using specification for function __gmpz_add
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
index f4b8cafb168..5220932a166 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
@@ -23,6 +23,6 @@ tests/gmp/array.i:10:[value] entering loop for the first time
tests/gmp/array.i:11:[value] entering loop for the first time
tests/gmp/array.i:13:[value] warning: assertion got status unknown.
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/gmp/array.i:14:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
index 3262967c94e..89d29cade4e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
@@ -25,7 +25,7 @@ tests/gmp/array.i:13:[value] warning: assertion got status unknown.
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
tests/gmp/array.i:14:[value] warning: assertion got status unknown.
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
index 1050b224c44..f9eb09f32b6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
@@ -32,7 +32,7 @@ tests/gmp/at.i:50:[value] cannot evaluate ACSL term, \at() on a C label is unsup
tests/gmp/at.i:50:[value] warning: assertion got status unknown.
[value] using specification for function __e_acsl_initialize
[value] using specification for function __e_acsl_valid_read
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/gmp/at.i:26:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
tests/gmp/at.i:26:[value] warning: assertion got status unknown.
tests/gmp/at.i:28:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
index 0964f02fd4a..00935cdbceb 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
@@ -26,7 +26,7 @@
[value] using specification for function __e_acsl_delete_block
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_add
FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h:65:[value] warning: function __gmpz_init_set: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index ce40f710602..9f712c261f8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -23,7 +23,7 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
[value] using specification for function __gmpz_get_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_init_set_ui
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
index 93e489236af..79c6428f815 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
@@ -20,7 +20,7 @@
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_init
[value] using specification for function __gmpz_neg
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
index 7ec731f67c3..728aaa6eb83 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
@@ -20,6 +20,6 @@
[value] using specification for function __e_acsl_assert
[value] using specification for function __gmpz_init_set_str
[value] using specification for function __gmpz_cmp
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
index 8df9baa9800..5378a45bc88 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
@@ -20,7 +20,7 @@
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] using specification for function __gmpz_init_set_ui
[value] using specification for function __gmpz_init_set_str
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
index 0b7409abafd..b686a7f8196 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
@@ -31,7 +31,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h:100:[value] warning: function __gmpz_import
[value] using specification for function __gmpz_add
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
[value] using specification for function __gmpz_get_si
tests/gmp/longlong.i:17:[value] Assigning imprecise value to __gen_e_acsl__4.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
index 9a0831c3c67..9ee43edefef 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
@@ -31,7 +31,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h:100:[value] warning: function __gmpz_import
[value] using specification for function __gmpz_add
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
tests/gmp/longlong.i:17:[value] Assigning imprecise value to __gen_e_acsl_eq.
The imprecision originates from Library function
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
index 2cef8c5b666..354a68bdcd8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
@@ -20,6 +20,6 @@
[value] using specification for function __gmpz_init_set_si
[value] using specification for function __gmpz_cmp
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_clear
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
index c49be496dce..dbe7f04a981 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
@@ -28,7 +28,7 @@ tests/gmp/quantif.i:12:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:12:[value] entering loop for the first time
tests/gmp/quantif.i:16:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:16:[value] entering loop for the first time
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/gmp/quantif.i:21:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:21:[value] entering loop for the first time
tests/gmp/quantif.i:25:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
index b5ad6c721e1..2d7d54f28bf 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
@@ -27,7 +27,7 @@ tests/gmp/quantif.i:9:[value] entering loop for the first time
[value] using specification for function __gmpz_init_set_str
[value] using specification for function __gmpz_add
[value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/gmp/quantif.i:10:[value] warning: assertion got status unknown.
tests/gmp/quantif.i:10:[value] entering loop for the first time
tests/gmp/quantif.i:11:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
index 6bc38c6ff03..80488f4bb31 100644
--- a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/no-main/empty.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
diff --git a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
index c5793567fa8..eb06d443b20 100644
--- a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/reject/quantif.i (no preprocessing)
tests/reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
index 1edaea2e362..6bc437e615c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/base_addr.c:44:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/base_addr.c:45:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:46:[value] warning: assertion got status unknown.
tests/runtime/base_addr.c:48:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
index bb5669fc510..4d3ffdc238b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/block_length.c:50:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/block_length.c:51:[value] warning: assertion got status unknown.
tests/runtime/block_length.c:53:[value] warning: assertion got status unknown.
tests/runtime/block_length.c:59:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
index ec3984a7aaa..d5ff5da8822 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/block_valid.c:39:[value] warning: pointer comparison. assert \pointer_comparable((void *)pmin, (void *)pmax);
tests/runtime/block_valid.c:45:[value] warning: out of bounds write. assert \valid(pmin);
tests/runtime/block_valid.c:46:[value] warning: out of bounds write. assert \valid(pmax);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
index aa50ea1c788..729d83e4e81 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
@@ -6,6 +6,6 @@ tests/runtime/ctype_macros.c:39:[e-acsl] warning: E-ACSL construct `disjoint beh
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/ctype.h:164:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/libc/ctype.h:168:[value] warning: function __gen_e_acsl_isupper, behavior definitely_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/ctype.h:171:[value] warning: function __gen_e_acsl_isupper, behavior definitely_not_match: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
index c36693c74fa..b37801b0973 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p
tests/runtime/early_exit.c:18:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
index a3131ccba19..468779b708f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/initialized.c:66:[value] warning: assertion got status unknown.
tests/runtime/initialized.c:70:[value] warning: assertion got status unknown.
FRAMAC_SHARE/libc/stdlib.h:348:[value] warning: function realloc: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
index 083880b4a84..535deea6a82 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/linear_search.i:7:[value] warning: function __gen_e_acsl_search: precondition got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/linear_search.i:7:[value] warning: function search: precondition got status unknown.
tests/runtime/linear_search.i:18:[value] warning: loop invariant got status unknown.
tests/runtime/linear_search.i:10:[value] warning: function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
index 14ef073849c..9e397cceed8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
@@ -16,4 +16,4 @@ tests/runtime/local_goto.c:28:[e-acsl] warning: E-ACSL construct `logic function
tests/runtime/local_goto.c:16:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
index 5d407b6f8c2..fd269ac1aff 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/runtime/local_init.c (with preprocessing)
[value] Analyzing an incomplete application starting at main
[value] Computing initial state
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
index a9580faa7d6..6797f763201 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/loop.i:19:[value] warning: loop invariant got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status invalid.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status invalid.
tests/runtime/loop.i:19:[value] warning: accessing uninitialized left-value.
assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index 3bc3521f1cf..3454430c79c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -9,7 +9,7 @@ FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause
FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/mainargs.c:12:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:13:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:15:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
index 00f3bf3dd0d..93842ddfe2e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/ptr.i:17:[value] warning: assertion got status unknown.
tests/runtime/ptr.i:18:[value] warning: assertion got status unknown.
tests/runtime/ptr.i:19:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
index 5871a45bd46..d0b8cccb129 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
@@ -1,3 +1,3 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
index 55035821d07..96f5d222a14 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/runtime/stdout.c:8:[value] warning: assertion got status unknown.
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/stdout.c:9:[value] warning: assertion got status unknown.
tests/runtime/stdout.c:10:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
index da57006d0ad..3489e4d7c7e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid.c:47:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
index fb329abb2c9..5855c1110d6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
tests/runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
index 7505bf79bc5..c91bbe57488 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid_in_contract.c:19:[value] warning: out of bounds read. assert \valid_read(&l->next);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
index 21342a2e5ec..1f55238645f 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/vector.c:26:[value] warning: accessing uninitialized left-value. assert \initialized(v2 + 2);
tests/runtime/vector.c:28:[value] warning: assertion got status unknown.
[scope:rm_asserts] removing 1 assertion(s)
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
index f9c713fab34..44e9bd78698 100644
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/special/builtin.i (no preprocessing)
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
index f9c713fab34..44e9bd78698 100644
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/special/builtin.i (no preprocessing)
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
index ecf75b4202e..7b2e58440d9 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
@@ -82,14 +82,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& extra_lbits));
__e_acsl_store_block((void *)(strings),(size_t)32);
__e_acsl_full_init((void *)(& strings));
- __e_acsl_temporal_store_nblock((void *)(& l_desc2.desc.extra_bits),
- (void *)(extra_lbits));
- __e_acsl_temporal_store_nblock((void *)(& descs[0].extra_bits),
- (void *)(extra_lbits));
- __e_acsl_temporal_store_nblock((void *)(& descs[1].extra_bits),
- (void *)(extra_lbits));
- __e_acsl_temporal_store_nblock((void *)(& l_desc.extra_bits),
- (void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
(void *)__gen_e_acsl_literal_string_4);
__e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
@@ -102,6 +94,14 @@ void __e_acsl_globals_init(void)
(void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& descs2[1].desc.extra_bits),
(void *)(extra_lbits));
+ __e_acsl_temporal_store_nblock((void *)(& l_desc2.desc.extra_bits),
+ (void *)(extra_lbits));
+ __e_acsl_temporal_store_nblock((void *)(& descs[0].extra_bits),
+ (void *)(extra_lbits));
+ __e_acsl_temporal_store_nblock((void *)(& descs[1].extra_bits),
+ (void *)(extra_lbits));
+ __e_acsl_temporal_store_nblock((void *)(& l_desc.extra_bits),
+ (void *)(extra_lbits));
return;
}
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
index bf1c1935443..274b6b9ec54 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
@@ -84,6 +84,13 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& Str));
__e_acsl_store_block((void *)(Strings),(size_t)32);
__e_acsl_full_init((void *)(& Strings));
+ __e_acsl_temporal_store_nblock((void *)(Str),
+ (void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_temporal_store_nblock((void *)(& Str[1]),
+ (void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_temporal_store_nblock((void *)(& Str[2]),
+ (void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_temporal_store_nblock((void *)(& Str[3]),(void *)0);
__e_acsl_temporal_store_nblock((void *)(& Strings[0][0]),
(void *)__gen_e_acsl_literal_string);
__e_acsl_temporal_store_nblock((void *)(& Strings[0][1]),
@@ -92,13 +99,6 @@ void __e_acsl_globals_init(void)
(void *)__gen_e_acsl_literal_string_3);
__e_acsl_temporal_store_nblock((void *)(& Strings[1][1]),
(void *)__gen_e_acsl_literal_string_4);
- __e_acsl_temporal_store_nblock((void *)(Str),
- (void *)__gen_e_acsl_literal_string_5);
- __e_acsl_temporal_store_nblock((void *)(& Str[1]),
- (void *)__gen_e_acsl_literal_string_6);
- __e_acsl_temporal_store_nblock((void *)(& Str[2]),
- (void *)__gen_e_acsl_literal_string_7);
- __e_acsl_temporal_store_nblock((void *)(& Str[3]),(void *)0);
return;
}
--
GitLab