Merge branch 'fix/wp/pac-any' into 'master'

[wp] fix AC-any pattern matching in strategies

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

src/plugins/wp/Pattern.ml

@@ -423,11 +423,9 @@ and ptry env p e =
 and pany env op rs es =
   match rs , es with
   | [] , [] -> ()
-  | rs , [] ->
-    let e = op [] in
-    List.iter (fun r -> pmatch env r e) rs
+  | [] , _ | _ , [] -> raise Not_found
+  | [r] , _ -> pmatch env r (op es)
   | r::rs , e::es -> pmatch env r e ; pany env op rs es
-  | [] , _::_ -> raise Not_found
 
 (* Pairwise matching *)
 and pargs env ps trail es =

src/plugins/wp/tests/wp_tip/oracle_qualif/pac.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing pac.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal target3_no_match_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target3_no_match_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal target4_exact_match_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target4_exact_match_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal target5_extra_match_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target5_extra_match_terminates (Cfg) (Trivial)
+[wp] 6 goals scheduled
+[wp] [NoResult] typed_target3_no_match_ensures_post (Qed)
+[wp] [Valid] typed_target3_no_match_assigns (Qed)
+[wp] [Valid] typed_target4_exact_match_assigns (Qed)
+[wp] [Valid] typed_target5_extra_match_assigns (Qed)
+[wp] [Unsuccess] typed_target4_exact_match_ensures_post (Tactic) (Qed)
+[wp] [Unsuccess] typed_target5_extra_match_ensures_post (Tactic) (Qed)
+[wp] Proved goals:    9 / 12
+  Terminating:     3
+  Unreachable:     3
+  Qed:             3
+  Unsuccess:       3
+  Missing:         1
+------------------------------------------------------------
+  Function target3_no_match
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target3_no_match':
+Assume {
+  Type: is_sint32(x) /\ is_sint32(y) /\ is_sint32(z).
+  (* Pre-condition *)
+  Have: (x != 0) \/ (y != 0) \/ (z != 0).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function target4_exact_match
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target4_exact_match':
+Assume {
+  Type: is_sint32(r) /\ is_sint32(x) /\ is_sint32(y) /\ is_sint32(z).
+  (* Pre-condition *)
+  Have: (r != 0) \/ (x != 0) \/ (y != 0) \/ (z != 0).
+}
+Prove: false.
+Prover Script returns Unsuccess
+
+------------------------------------------------------------
+Subgoal 1/4:
+ - Post-condition 'post'
+ - Split (Case 1/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-0 (generated):
+Assume { Type: is_sint32(r). (* Case 1/4 *) When: r != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 2/4:
+ - Post-condition 'post'
+ - Split (Case 2/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-1 (generated):
+Assume { Type: is_sint32(x). (* Case 2/4 *) When: x != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 3/4:
+ - Post-condition 'post'
+ - Split (Case 3/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-2 (generated):
+Assume { Type: is_sint32(y). (* Case 3/4 *) When: y != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 4/4:
+ - Post-condition 'post'
+ - Split (Case 4/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-3 (generated):
+Assume { Type: is_sint32(z). (* Case 4/4 *) When: z != 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function target5_extra_match
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target5_extra_match':
+Assume {
+  Type: is_sint32(r) /\ is_sint32(s) /\ is_sint32(x) /\ is_sint32(y) /\
+      is_sint32(z).
+  (* Pre-condition *)
+  Have: (r != 0) \/ (s != 0) \/ (x != 0) \/ (y != 0) \/ (z != 0).
+}
+Prove: false.
+Prover Script returns Unsuccess
+
+------------------------------------------------------------
+Subgoal 1/5:
+ - Post-condition 'post'
+ - Split (Case 1/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-0 (generated):
+Assume { Type: is_sint32(r). (* Case 1/5 *) When: r != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 2/5:
+ - Post-condition 'post'
+ - Split (Case 2/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-1 (generated):
+Assume { Type: is_sint32(s). (* Case 2/5 *) When: s != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 3/5:
+ - Post-condition 'post'
+ - Split (Case 3/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-2 (generated):
+Assume { Type: is_sint32(x). (* Case 3/5 *) When: x != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 4/5:
+ - Post-condition 'post'
+ - Split (Case 4/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-3 (generated):
+Assume { Type: is_sint32(y). (* Case 4/5 *) When: y != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 5/5:
+ - Post-condition 'post'
+ - Split (Case 5/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-4 (generated):
+Assume { Type: is_sint32(z). (* Case 5/5 *) When: z != 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  target3_no_match          1        -        2      50.0%
+  target4_exact_match       1        -        2      50.0%
+  target5_extra_match       1        -        2      50.0%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/pac.i

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   OPT: -wp-status -wp-prover tip -wp-script dry
+ */
+
+/*@
+  strategy Split4:
+    \tactic("Wp.split"
+      ,\pattern( _ || _ || _ || _ )
+    );
+  proof Split4: post;
+*/
+
+/*@
+  requires x || y || z;
+  ensures post: \false;
+  assigns \nothing;
+*/
+void target3_no_match(int x, int y, int z) { return; }
+
+/*@
+  requires x || y || z || r;
+  ensures post: \false;
+  assigns \nothing;
+*/
+void target4_exact_match(int x, int y, int z, int r) { return; }
+
+/*@
+  requires x || y || z || r || s;
+  ensures post: \false;
+  assigns \nothing;
+*/
+void target5_extra_match(int x, int y, int z, int r, int s) { return; }