From 98149ef13b339c67a7b2d69b98c7ccedfe251c78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 11 Sep 2019 11:26:08 +0200
Subject: [PATCH] [wp/cache] move test using scripts in qualif
---
.../tests/wp_plugin/oracle/unroll.res.oracle | 6 ------
.../typed_unrolled_loop_ensures_zero.json | 0
.../wp_plugin/oracle_qualif/unroll.res.oracle | 18 ++++++++++++++++++
src/plugins/wp/tests/wp_plugin/unroll.i | 4 ++--
4 files changed, 20 insertions(+), 8 deletions(-)
rename src/plugins/wp/tests/wp_plugin/{unroll/wp => oracle_qualif/unroll.0.session}/typed/typed_unrolled_loop_ensures_zero.json (100%)
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
index 77e0cc1a55c..a47827c25dd 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/unroll.res.oracle
@@ -5,11 +5,6 @@
[wp] Warning: Missing RTE guards
[wp] tests/wp_plugin/unroll.i:20: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] 1 goal scheduled
-[wp] [Tactical] Goal typed_unrolled_loop_ensures_zero : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
- Script: 1
------------------------------------------------------------
Function unrolled_loop
------------------------------------------------------------
@@ -30,6 +25,5 @@ Prove: P_zeroed(Mint_0[a <- 0][shift_uint32(t, 1) <- 0][shift_uint32(t, 2)
[shift_uint32(t, 11) <- 0][shift_uint32(t, 12) <- 0]
[shift_uint32(t, 13) <- 0][shift_uint32(t, 14) <- 0]
[shift_uint32(t, 15) <- 0], t, 0, 15).
-Prover Tactical returns Valid
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/unroll/wp/typed/typed_unrolled_loop_ensures_zero.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/typed/typed_unrolled_loop_ensures_zero.json
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/unroll/wp/typed/typed_unrolled_loop_ensures_zero.json
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/typed/typed_unrolled_loop_ensures_zero.json
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
new file mode 100644
index 00000000000..bf1a7e953c7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_plugin/unroll.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/unroll.i:20: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 1 goal scheduled
+[wp] [Tactical] Goal typed_unrolled_loop_ensures_zero : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Script: 1
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/unroll.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/unroll.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+unrolled_loop - - 1 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index 5ac917b0ddb..8e34f8f66ed 100644
--- a/src/plugins/wp/tests/wp_plugin/unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/unroll.i
@@ -1,9 +1,9 @@
/* run.config
- OPT: -ulevel=1 -wp -wp-prop=@ensures -wp-prover script -session tests/wp_plugin/unroll -wp-msg-key no-time-info,no-step-info
+ OPT: -ulevel=1 -wp-prop=@ensures
*/
/* run.config_qualif
- DONTRUN:
+ OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script
*/
enum {Max = 16};
--
GitLab