Merge branch 'fix/755/wp/recursive-predicate-generation' into 'stable/calcium'

[WP] Fixes recursive predicate generation in Why3

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

src/plugins/wp/ProverWhy3.ml

@@ -914,9 +914,8 @@ class visitor (ctx:context) c =
                 let t = share cnv Prop (Lang.F.e_prop p) in
                 let t =
                   Why3.Term.t_forall_close vars []
-                    (Why3.Term.t_equ
-                       (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result)
-                       t)
+                    (Why3.Term.t_iff t
+                       (Why3.Term.t_app id (List.map Why3.Term.t_var vars) result))
                 in
                 let decl =
                   Why3.Decl.create_prop_decl Why3.Decl.Paxiom

src/plugins/wp/tests/wp_acsl/oracle/predicates_functions.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/predicates_functions.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 1 goal scheduled
+[wp:print-generated] 
+  theory WP
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    predicate P_P (i:int) = i = 42
+    
+    predicate P_RP int
+    
+    axiom P_RP_def :
+      forall i:int. i <= 0 \/ P_P i /\ P_RP ((- 1) + i) <-> P_RP i
+    
+    function L_F (i:int) : int = 2 * i
+    
+    function L_RF int : int
+    
+    axiom L_RF_def :
+      forall i:int. L_RF i = (if i <= 0 then 0 else L_F i + L_RF ((- 1) + i))
+    
+    goal wp_goal : forall i:int. 0 < i -> P_RP (L_RF i)
+  end
+[wp] 1 goal generated
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Lemma foo:
+Prove: (0<i_0) -> (P_RP (L_RF i_0))
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/predicates_functions.i

+/* run.config
+   OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/*@ predicate P(integer i) = i == 42 ; */
+/*@ predicate RP(integer i) = (i <= 0) || ( P(i) && RP(i-1) ) ; */
+
+/*@ logic integer F(integer i) = i * 2 ; */
+/*@ logic integer RF(integer i) = (i <= 0) ? 0 : F(i) + RF(i-1) ; */
+
+/*@ lemma foo: \forall integer i ; i > 0 ==> RP(RF(i)) ; */
\ No newline at end of file