From ca081f74ee7d07a0e6195987d3969f467cf2c148 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Jan 2024 11:32:31 +0100
Subject: [PATCH] [wp] test with cvc4
---
src/plugins/wp/tests/wp_plugin/cvc4_ce.i | 8 ++++
.../tests/wp_plugin/oracle/cvc4_ce.res.oracle | 28 ++++++++++++
.../oracle_qualif/cvc4_ce.res.oracle | 44 +++++++++++++++++++
3 files changed, 80 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_plugin/cvc4_ce.i
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/cvc4_ce.i b/src/plugins/wp/tests/wp_plugin/cvc4_ce.i
new file mode 100644
index 00000000000..853f90943c0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/cvc4_ce.i
@@ -0,0 +1,8 @@
+/* run.config_qualif
+ OPT: -wp -wp-counter-examples -wp-prover cvc4 -wp-status
+ */
+
+//@ check lemma wrong: \forall integer x; \abs(x) == x;
+
+//@ ensures \result == \abs(x); assigns \nothing;
+int wrong(int x) { return x; }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle
new file mode 100644
index 00000000000..2832c47376f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cvc4_ce.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp [...]
+[kernel] Parsing cvc4_ce.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal wrong_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Check Lemma 'wrong':
+Prove: IAbs.abs(x) = x.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function wrong
+------------------------------------------------------------
+
+Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Assume { Type: is_sint32(wrong_0). }
+Prove: IAbs.abs(wrong_0) = wrong_0.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'wrong':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle
new file mode 100644
index 00000000000..ca0d3106e81
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cvc4_ce.res.oracle
@@ -0,0 +1,44 @@
+# frama-c -wp [...]
+[kernel] Parsing cvc4_ce.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal wrong_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal wrong_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Unsuccess] typed_check_lemma_wrong (CVC4) (No Cache) (Model)
+[wp] [Unsuccess] typed_wrong_ensures (CVC4) (No Cache) (Model)
+[wp] [Valid] typed_wrong_assigns (Qed)
+[wp] Proved goals: 3 / 5
+ Terminating: 1
+ Unreachable: 1
+ Qed: 1
+ Unsuccess: 2
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Check Lemma 'wrong':
+Assume { Probe x = x. }
+Prove: IAbs.abs(x) = x.
+Prover CVC4 returns Unsuccess (Model)
+Model x = -1
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function wrong
+------------------------------------------------------------
+
+Goal Post-condition (file cvc4_ce.i, line 7) in 'wrong':
+Assume { Type: is_sint32(wrong_0). Probe x = wrong_0. }
+Prove: IAbs.abs(wrong_0) = wrong_0.
+Prover CVC4 returns Unsuccess (Model)
+Model x = -1
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - - 1 0.0%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ wrong 1 - 2 50.0%
+------------------------------------------------------------
--
GitLab