From 3b60c570b028e6da5e6a0240b421dbfc5c6b3620 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 25 Apr 2019 16:48:02 +0200
Subject: [PATCH] [WP/test] compliant oracles with OCI
---
.../wp/tests/wp_plugin/oracle_qualif/config.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index c205459c40e..64c74fa7554 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -2,6 +2,6 @@
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
1. The Alt-Ergo theorem prover, version 2.0.0
-2. The Why3 platform, version 1.2.0
+2. The Why3 platform, version 1.1.1
3. The Coq Proof Assistant, version 8.9.0
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json
index 910cff1aa78..47905d279b0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json
@@ -36,12 +36,12 @@
"memcpy_loop_assigns": { "alt-ergo":
{ "total": 1,
"valid": 1,
- "rank": 40 },
+ "rank": 43 },
"qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 3,
"valid": 3,
- "rank": 40 } },
+ "rank": 43 } },
"memcpy_ensures_result_ptr": { "qed":
{ "total": 1,
"valid": 1 },
--
GitLab