From f8865717058fe9b9ab9eb36fcbe7c074023b0219 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 30 Oct 2019 17:45:45 +0100
Subject: [PATCH] [wp] update qualif tests
---
.../wp_bts/oracle_qualif/bts_2471.1.res.oracle | 1 +
.../wp_bts/oracle_qualif/bts_2471.2.res.oracle | 1 +
.../wp_typed/oracle_qualif/mvar.0.report.json | 16 ++++++----------
.../tests/wp_typed/oracle_qualif/mvar.res.oracle | 2 +-
4 files changed, 9 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
index 68dc1319cde..d1bac58fc49 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
@@ -3,6 +3,7 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
[wp] 1 goal scheduled
[wp] [Alt-Ergo (Native)] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
index 6c44b75068c..c83a6e29b18 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
@@ -3,6 +3,7 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
[wp] [Coq] Goal typed_foo_assert_ko : Default tactic
[wp] [Coq (Native)] Goal typed_foo_assert_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
index 5d34a2aa148..174835a1aa1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
@@ -1,14 +1,10 @@
-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 1 },
- "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
"wp:functions": { "Job": { "Job_ensures": { "why3:Alt-Ergo,2.0.0":
- { "total": 1, "valid": 1,
- "rank": 1 },
+ { "total": 1, "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } },
+ "valid": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
- "valid": 1,
- "rank": 1 },
+ "valid": 1 },
"wp:main": { "total": 1,
- "valid": 1,
- "rank": 1 } } } } }
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index 48f19a88154..487049986e2 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -14,5 +14,5 @@
[wp] Report out: 'tests/wp_typed/result_qualif/mvar.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-Job - 1 (1..12) 1 100%
+Job - 1 1 100%
-------------------------------------------------------------
--
GitLab