From f58bc707f5d043324091e1aa6c77d5ece1555e19 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 13 May 2020 09:23:16 +0200
Subject: [PATCH] [wp] remove useless match-bool from why3 driver
---
src/plugins/wp/share/why3/frama_c_wp/qed.mlw | 12 +-----------
src/plugins/wp/tests/wp_bts/issue_81.i | 4 ++++
.../tests/wp_bts/oracle/issue_81.res.oracle | 19 +++++++++++++++++++
.../wp_bts/oracle_qualif/issue_81.res.oracle | 14 ++++++++++++++
4 files changed, 38 insertions(+), 11 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_bts/issue_81.i
create mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
diff --git a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
index 845fbeab407..8992dc01542 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/qed.mlw
@@ -28,18 +28,8 @@ theory Qed
use real.FromInt
use int.ComputerDivision as CD
- (** to be used only for the ACSL ite generation.
- Something is wrong with "wp/share/ergo/bool.Bool.mlw" (coming from why3),
- the function match_bool is undefined.
- An hack is to give a definition here. *)
- function match_bool (x : bool) (y z:'a ) : 'a
- axiom match_bool: forall p:bool, x:'a, y:'a [match_bool p x y].
- ( p=True /\ match_bool p x y=x ) ||
- ( p=False /\ match_bool p x y=y )
- meta "remove_for_why3" axiom match_bool
-
(** The definitions are in comment because its not useful for coq
- (no if-then-else on formula) and not tested on automatic provers *)
+ (no if-then-else on formula) and not tested on automatic provers *)
function eqb (x y : 'a) : bool (*= if x = y then True else False*)
axiom eqb : forall x:'a, y:'a. eqb x y = True <-> x = y
diff --git a/src/plugins/wp/tests/wp_bts/issue_81.i b/src/plugins/wp/tests/wp_bts/issue_81.i
new file mode 100644
index 00000000000..50f0a51b005
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_81.i
@@ -0,0 +1,4 @@
+/*@ predicate isMax( integer x, integer y, integer z ) = x < y ? x == z : y == z ; */
+
+/*@ ensures isMax(a,b,\result); */
+int getMax(int a,int b) { return a <= b ? a : b; }
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
new file mode 100644
index 00000000000..3c3d2d46a68
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function getMax
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_81.i, line 3) in 'getMax':
+Assume {
+ Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(getMax_0).
+ If a <= b
+ Then { Have: getMax_0 = a. }
+ Else { Have: getMax_0 = b. }
+}
+Prove: P_isMax(a, b, getMax_0).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
new file mode 100644
index 00000000000..9486ece4ecc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_81.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_getMax_ensures : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ getMax - 1 1 100%
+------------------------------------------------------------
--
GitLab