From a45a5957f2cd485f13215397b256eb9649ab2353 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Jun 2021 12:33:28 +0200
Subject: [PATCH] WP now supports terminates
---
tests/bugs/oracle/term.res.oracle | 5 -----
tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json | 2 ++
tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json | 1 +
3 files changed, 3 insertions(+), 5 deletions(-)
create mode 100644 tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json
create mode 100644 tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json
diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index 75a043ab..4b93bf2c 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -3,11 +3,6 @@
Now output intermediate result
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/bugs/term.cpp:11: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:17: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:43: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:26: Warning: Terminates not implemented yet (skipped).
-[wp] tests/bugs/term.cpp:34: Warning: Terminates not implemented yet (skipped).
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_Z2m2_ensures : Valid
[wp] [Qed] Goal typed_Z2m3_c_ensures : Valid
diff --git a/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json b/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json
new file mode 100644
index 00000000..ffb25c4b
--- /dev/null
+++ b/tests/wp-cache/cache/037ca0030a34338e8f4f70326e9548a2.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0194,
+ "steps": 14 }
diff --git a/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json b/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json
new file mode 100644
index 00000000..8256dcea
--- /dev/null
+++ b/tests/wp-cache/cache/0e7fd5a62a27e32132a8aadc6de1bc5e.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" }
--
GitLab