From b0d6a40b5ab4142c7bbd3cecf719796e3791c839 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 18 Nov 2021 11:33:20 +0100
Subject: [PATCH] [eacsl] Add test for issue e-acsl#166
---
.../e-acsl/tests/bts/issue-eacsl-166.i | 23 +++++++++++++++++++
.../bts/oracle/issue-eacsl-166.res.oracle | 6 +++++
2 files changed, 29 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/bts/issue-eacsl-166.i
create mode 100644 src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-166.i b/src/plugins/e-acsl/tests/bts/issue-eacsl-166.i
new file mode 100644
index 00000000000..94f943aee10
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-166.i
@@ -0,0 +1,23 @@
+/* run.config
+ COMMENT: Change order of options to run Eva before E-ACSL so that the ensures
+ COMMENT: clause is proven invalid before running E-ACSL. Eva will prove the
+ COMMENT: ensures invalid under hypotheses of reachability, this test shows
+ COMMENT: that when we duplicate the invalid property statuses, we remove the
+ COMMENT: hypotheses to satisfy kernel invariants.
+ OPT: @GLOBAL@ @EVA@ -then @EACSL@ -then-last @EVENTUALLY@
+*/
+/* run.config_dev
+ COMMENT: No need to compile and execute the test since we know the property
+ COMMENT: will be invalid.
+ DONTRUN:
+*/
+
+/*@ ensures \result == 1; */
+int f() {
+ return 0;
+}
+
+int main() {
+ f();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle
new file mode 100644
index 00000000000..efd60b0c451
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-166.res.oracle
@@ -0,0 +1,6 @@
+[eva:alarm] tests/bts/issue-eacsl-166.i:15: Warning:
+ function f: postcondition got status invalid.
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-166.i:15: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status invalid.
--
GitLab