From efebd7aec36656f4bd8cce2dd4847d24bc0b6000 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 4 Mar 2019 14:51:13 +0100
Subject: [PATCH] [WP,EVA] adds a test related to property dependencies
---
src/plugins/wp/tests/wp_acsl/checks.i | 19 +++++
.../tests/wp_acsl/oracle/checks.0.res.oracle | 75 +++++++++++++++++++
.../tests/wp_acsl/oracle/checks.1.res.oracle | 18 +++++
.../tests/wp_acsl/oracle/checks.2.res.oracle | 28 +++++++
.../wp_acsl/oracle_qualif/checks.res.oracle | 50 +++++++++++++
5 files changed, 190 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/checks.i
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
new file mode 100644
index 00000000000..1a1174504f7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -0,0 +1,19 @@
+/* run.config
+ OPT: -eva -load-module scope,eva,report -then -report
+ OPT: -wp-prop=@check
+ OPT: -wp-prop=@assert
+*/
+/* run.config_qualif
+ OPT: -load-module report -wp-steps 5 -then -report
+*/
+
+// note: eva and wp gives the same reporting
+
+//@ axiomatic A { predicate P reads \nothing ; }
+void main() {
+ //@check c1: P;
+ //@assert a1: P;
+ //@check c2: P;
+ //@assert a2: P;
+ ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
new file mode 100644
index 00000000000..a99ec33e26d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
@@ -0,0 +1,75 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] tests/wp_acsl/checks.i:14: Warning: check 'c1' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:15: Warning:
+ assertion 'a1' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:16: Warning: check 'c2' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:17: Warning:
+ assertion 'a2' got status unknown.
+[eva] done for function main
+[scope:rm_asserts] removing 2 assertion(s)
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+
+[report] Computing properties status...
+--------------------------------------------------------------------------------
+--- Global Properties
+--------------------------------------------------------------------------------
+
+[ Valid ] Axiomatic 'A'
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Check 'c1' (file tests/wp_acsl/checks.i, line 14)
+ tried with Eva.
+[ - ] Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+ tried with Eva.
+[ Partial ] Check 'c2' (file tests/wp_acsl/checks.i, line 16)
+ By RedundantAlarms, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+[ Partial ] Assertion 'a2' (file tests/wp_acsl/checks.i, line 17)
+ By RedundantAlarms, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 1 Completely validated
+ 2 Locally validated
+ 2 To be validated
+ 5 Total
+--------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
new file mode 100644
index 00000000000..6de4c095087
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
new file mode 100644
index 00000000000..669139a5ea8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
new file mode 100644
index 00000000000..7f27fd0f13f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
@@ -0,0 +1,50 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 5 [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Alt-Ergo] Goal typed_main_check_c1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_assert_a1 : Unsuccess
+[wp] [Qed] Goal typed_main_check_c2 : Valid
+[wp] [Qed] Goal typed_main_assert_a2 : Valid
+[wp] Proved goals: 2 / 4
+ Qed: 2
+ Alt-Ergo: 0 (unsuccess: 2)
+[wp] Report in: 'tests/wp_acsl/oracle_qualif/checks.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/checks.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+main 2 - 4 50.0%
+-------------------------------------------------------------
+[report] Computing properties status...
+--------------------------------------------------------------------------------
+--- Global Properties
+--------------------------------------------------------------------------------
+
+[ Valid ] Axiomatic 'A'
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Check 'c1' (file tests/wp_acsl/checks.i, line 14)
+ tried with Wp.typed.
+[ - ] Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+ tried with Wp.typed.
+[ Partial ] Check 'c2' (file tests/wp_acsl/checks.i, line 16)
+ By Wp.typed, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+[ Partial ] Assertion 'a2' (file tests/wp_acsl/checks.i, line 17)
+ By Wp.typed, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 1 Completely validated
+ 2 Locally validated
+ 2 To be validated
+ 5 Total
+--------------------------------------------------------------------------------
--
GitLab