From 729d5da53665bc424f7690526e97a86fc9d35dff Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 17 Mar 2020 11:13:55 +0100
Subject: [PATCH] [WP] some more tests
---
src/plugins/wp/tests/wp_bts/issue_825.i | 5 +++++
.../wp/tests/wp_bts/oracle/issue_825.res.oracle | 14 ++++++++++++++
.../cache/2e52caad3f8b8552be7c703a245947cf.json | 1 +
.../cache/7da8f94d00d90464616019326ebbc808.json | 1 +
.../wp_bts/oracle_qualif/issue_825.res.oracle | 9 ++++++---
5 files changed, 27 insertions(+), 3 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json
diff --git a/src/plugins/wp/tests/wp_bts/issue_825.i b/src/plugins/wp/tests/wp_bts/issue_825.i
index b4c514fccc8..3810f22f258 100644
--- a/src/plugins/wp/tests/wp_bts/issue_825.i
+++ b/src/plugins/wp/tests/wp_bts/issue_825.i
@@ -14,3 +14,8 @@ void job(void)
i ++;
}
}
+void issue(int a) {
+ //@ check ko: \exists integer j; 0 < j < 0;
+ //@ check ko: (\forall integer j; 0 < j < 0 ==> \false) ==> (a == 0);
+ ;
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
index c6a5972a861..65c234448ba 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
@@ -3,6 +3,20 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function issue
+------------------------------------------------------------
+
+Goal Check 'ko' (file tests/wp_bts/issue_825.i, line 18):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'ko' (file tests/wp_bts/issue_825.i, line 19):
+Assume { Type: is_sint32(a). }
+Prove: a = 0.
+
+------------------------------------------------------------
------------------------------------------------------------
Function job
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
new file mode 100644
index 00000000000..56c39550428
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json
new file mode 100644
index 00000000000..b8e36e2803f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
index 84d7a31b97c..35895046c31 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
@@ -3,17 +3,20 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
+[wp] 8 goals scheduled
+[wp] [Alt-Ergo] Goal typed_issue_check_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_issue_check_ko_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_ensures : Unsuccess
[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
[wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_job_loop_assigns_part2 : Unsuccess
[wp] [Qed] Goal typed_job_assigns : Valid
-[wp] Proved goals: 4 / 6
+[wp] Proved goals: 4 / 8
Qed: 4
- Alt-Ergo: 0 (unsuccess: 2)
+ Alt-Ergo: 0 (unsuccess: 4)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 4 - 6 66.7%
+ issue - - 2 0.0%
------------------------------------------------------------
--
GitLab