Merge branch '81-wp-share-enlever-le-hack-de-qed-why-relativement-a-match_bool' into 'master'

Resolve "[WP/Share] enlever le hack de qed.why relativement à match_bool"

Closes #81

See merge request frama-c/frama-c!2654

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

src/plugins/wp/tests/wp_bts/issue_81.i

+/*@ 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; }

src/plugins/wp/tests/wp_bts/oracle/issue_81.res.oracle

+# 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).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_81.res.oracle

+# 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%
+------------------------------------------------------------