diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index ce8540e29b5026a60d3f4aa8683386902f612e59..1e20d4073b31635a76f08fe062d01ad23e966d37 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -168,32 +168,35 @@ class split =
~params:[]
method select feedback (s : Tactical.selection) =
+ let split_cmp at title x y =
+ feedback#set_title title ;
+ feedback#set_descr
+ "Decompose into three comparisons (lt, eq, gt)" ;
+ let cases = [
+ "Lt",F.p_bool (e_lt x y);
+ "Eq",F.p_bool (e_eq x y);
+ "Gt",F.p_bool (e_lt y x);
+ ] in
+ Applicable (Tactical.insert ?at cases)
+ in
+ let split_leq at x y = split_cmp at "Split (<=)" x y in
+ let split_eq at x y = split_cmp at "Split (=)" x y in
+ let split_neq at x y = split_cmp at "Split (<>)" x y in
+ let split_lt at x y =
+ let x = if F.is_int x then F.(e_add x e_one) else x in
+ split_cmp at "Split (<)" x y
+ in
match s with
| Empty | Compose _ -> Not_applicable
| Inside(_,e) ->
begin
- let split_cmp title x y =
- feedback#set_title title ;
- feedback#set_descr
- "Decompose into three comparisons (lt, eq, gt)" ;
- let cases = [
- "Lt",F.p_bool (e_lt x y);
- "Eq",F.p_bool (e_eq x y);
- "Gt",F.p_bool (e_lt y x);
- ] in
- let at = Tactical.at s in
- Applicable (Tactical.insert ?at cases)
- in
+ let at = Tactical.at s in
let open Qed.Logic in
match Lang.F.repr e with
- | Leq(x,y) -> split_cmp "Split (comp.)" x y
- | Lt(x,y) ->
- let x = if F.is_int x then F.(e_add x e_one) else x in
- split_cmp "Split (comp.)" x y
- | Eq(x,y) when not (is_prop x || is_prop y) ->
- split_cmp "Split (eq.)" x y
- | Neq(x,y) when not (is_prop x || is_prop y) ->
- split_cmp "Split (neq.)" x y
+ | Leq(x,y) -> split_leq at x y
+ | Lt(x,y) -> split_lt at x y
+ | Eq(x,y) when not (is_prop x || is_prop y) -> split_eq at x y
+ | Neq(x,y) when not (is_prop x || is_prop y) -> split_neq at x y
| _ when F.is_prop e ->
feedback#set_title "Split (true,false)" ;
feedback#set_descr "Decompose between True and False values" ;
@@ -384,17 +387,13 @@ class split =
] in
Applicable (Tactical.replace ~at:step.id cases)
| Neq(x,y) when not (is_prop x || is_prop y) ->
- feedback#set_title "Split (<>)";
- feedback#set_descr "Decompose into two comparisons (<, >)" ;
- let cases = ["Lt", When F.(p_bool (e_lt x y));
- "Gt", When F.(p_bool (e_lt y x))] in
- Applicable (Tactical.replace ~at:step.id cases)
- | Leq(x,y) when not (is_prop x || is_prop y) ->
- feedback#set_title "Split (<=)";
- feedback#set_descr "Decompose into two comparisons (<, =)" ;
- let cases = ["Lt", When F.(p_bool (e_lt x y));
- "Eq", When F.(p_bool (e_eq y x))] in
- Applicable (Tactical.replace ~at:step.id cases)
+ split_neq (Some step.id) x y
+ | Eq(x,y) when not (is_prop x || is_prop y) ->
+ split_eq (Some step.id) x y
+ | Lt(x,y) ->
+ split_lt (Some step.id) x y
+ | Leq(x,y) ->
+ split_leq (Some step.id) x y
| If(c,p,q) ->
feedback#set_title "Split (if)" ;
feedback#set_descr "Split Conditional into Branches" ;
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 8817de6750fb29b00a6d21a64b57919693e55f19..5288564504e27708caa522f6c8bba6394589ea17 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_tip/split.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 20 goals scheduled
+[wp] 23 goals scheduled
[wp:script:allgoals]
Goal Post-condition (file tests/wp_tip/split.i, line 36) in 'test_step_branch':
Assume {
@@ -27,19 +27,46 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 54) in 'test_step_eq':
+ Goal Post-condition (file tests/wp_tip/split.i, line 54) in 'test_step_peq':
Assume { (* Pre-condition *) Have: L_LQ = L_LP. }
Prove: P_S.
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 58) in 'test_step_neq':
+ Goal Post-condition (file tests/wp_tip/split.i, line 58) in 'test_step_pneq':
Assume { (* Pre-condition *) Have: L_LQ != L_LP. }
Prove: P_S.
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 62) in 'test_step_if':
+ Goal Post-condition (file tests/wp_tip/split.i, line 62) in 'test_step_neq':
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(b).
+ (* Pre-condition *)
+ Have: b != a.
+ }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Goal Post-condition (file tests/wp_tip/split.i, line 66) in 'test_step_leq':
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(b).
+ (* Pre-condition *)
+ Have: a <= b.
+ }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Goal Post-condition (file tests/wp_tip/split.i, line 70) in 'test_step_lt':
+ Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: a < b.
+ }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Goal Post-condition (file tests/wp_tip/split.i, line 74) in 'test_step_if':
Assume {
Type: is_sint32(a) /\ is_sint32(b).
(* Pre-condition *)
@@ -49,7 +76,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 66) in 'test_step_fa_if':
+ Goal Post-condition (file tests/wp_tip/split.i, line 78) in 'test_step_fa_if':
Assume {
(* Heap *)
Type: is_sint32(a) /\ is_sint32(b).
@@ -60,7 +87,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 70) in 'test_step_fa_or':
+ Goal Post-condition (file tests/wp_tip/split.i, line 82) in 'test_step_fa_or':
Assume {
(* Pre-condition *)
Have: forall i : Z. P_P \/ P_Q \/ P_R \/ P_Pi(i) \/ P_Qi(i).
@@ -69,7 +96,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 75) in 'test_step_fa_and':
+ Goal Post-condition (file tests/wp_tip/split.i, line 86) in 'test_step_fa_and':
Assume {
(* Pre-condition *)
Have: forall i : Z. P_P /\ P_Q /\ P_R /\ P_Pi(i) /\ P_Qi(i).
@@ -78,7 +105,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 79) in 'test_inside_leq':
+ Goal Post-condition (file tests/wp_tip/split.i, line 90) in 'test_inside_leq':
Assume {
Type: is_sint32(a) /\ is_sint32(b).
(* Pre-condition *)
@@ -88,7 +115,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 83) in 'test_inside_lt':
+ Goal Post-condition (file tests/wp_tip/split.i, line 94) in 'test_inside_lt':
Assume {
Type: is_sint32(a) /\ is_sint32(b).
(* Pre-condition *)
@@ -98,7 +125,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 87) in 'test_inside_neq':
+ Goal Post-condition (file tests/wp_tip/split.i, line 98) in 'test_inside_neq':
Assume {
Type: is_sint32(a) /\ is_sint32(b).
(* Pre-condition *)
@@ -108,43 +135,43 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 91) in 'test_goal_and':
+ Goal Post-condition (file tests/wp_tip/split.i, line 102) in 'test_goal_and':
Assume { (* Pre-condition *) Have: P_S. }
Prove: P_P /\ P_Q /\ P_R.
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 95) in 'test_goal_eq':
+ Goal Post-condition (file tests/wp_tip/split.i, line 106) in 'test_goal_eq':
Assume { (* Pre-condition *) Have: P_S. }
Prove: L_LQ = L_LP.
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 99) in 'test_goal_neq':
+ Goal Post-condition (file tests/wp_tip/split.i, line 110) in 'test_goal_neq':
Assume { (* Pre-condition *) Have: P_S. }
Prove: L_LQ != L_LP.
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 103) in 'test_goal_if':
+ Goal Post-condition (file tests/wp_tip/split.i, line 114) in 'test_goal_if':
Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_S. }
Prove: if (a < b) then P_P else P_Q.
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 107) in 'test_goal_ex_and':
+ Goal Post-condition (file tests/wp_tip/split.i, line 118) in 'test_goal_ex_and':
Assume { (* Pre-condition *) Have: P_S. }
Prove: exists i : Z. P_P /\ P_Q /\ P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 111) in 'test_goal_ex_or':
+ Goal Post-condition (file tests/wp_tip/split.i, line 122) in 'test_goal_ex_or':
Assume { (* Pre-condition *) Have: P_S. }
Prove: exists i : Z. P_P \/ P_Q \/ P_Pi(i) \/ P_Qi(i).
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 115) in 'test_goal_ex_if':
+ Goal Post-condition (file tests/wp_tip/split.i, line 126) in 'test_goal_ex_if':
Assume {
(* Heap *)
Type: is_sint32(a) /\ is_sint32(b).
@@ -155,7 +182,7 @@
------------------------------------------------------------
[wp:script:allgoals]
- Goal Post-condition (file tests/wp_tip/split.i, line 119) in 'test_goal_ex_imply':
+ Goal Post-condition (file tests/wp_tip/split.i, line 130) in 'test_goal_ex_imply':
Assume { (* Pre-condition *) Have: P_S. }
Prove: exists i : Z. (P_Q -> (P_Pi(i) -> P_Qi(i))).
@@ -231,27 +258,44 @@
------------------------------------------------------------
[wp] [Script] Goal typed_test_step_and_ensures : Unsuccess
[wp:script:allgoals]
- typed_test_step_eq_ensures subgoal:
+ typed_test_step_peq_ensures subgoal:
- Goal Wp.Tactical.typed_test_step_eq_ensures-0 (generated):
+ Goal Wp.Tactical.typed_test_step_peq_ensures-0 (generated):
Assume { (* Both True *) When: (L_LP=true) /\ (L_LQ=true). }
Prove: P_S.
------------------------------------------------------------
-[wp] [Script] Goal typed_test_step_eq_ensures : Unsuccess
+[wp] [Script] Goal typed_test_step_peq_ensures : Unsuccess
[wp:script:allgoals]
- typed_test_step_eq_ensures subgoal:
+ typed_test_step_peq_ensures subgoal:
- Goal Wp.Tactical.typed_test_step_eq_ensures-1 (generated):
+ Goal Wp.Tactical.typed_test_step_peq_ensures-1 (generated):
Assume { (* Both False *) When: (L_LP=false) /\ (L_LQ=false). }
Prove: P_S.
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_test_step_pneq_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_pneq_ensures-0 (generated):
+ Assume { (* True/False *) When: (L_LQ=true) /\ (L_LP=false). }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_pneq_ensures : Unsuccess
+[wp:script:allgoals]
+ typed_test_step_pneq_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_pneq_ensures-1 (generated):
+ Assume { (* False/True *) When: (L_LP=true) /\ (L_LQ=false). }
+ Prove: P_S.
+
------------------------------------------------------------
[wp:script:allgoals]
typed_test_step_neq_ensures subgoal:
Goal Wp.Tactical.typed_test_step_neq_ensures-0 (generated):
- Assume { (* True/False *) When: (L_LQ=true) /\ (L_LP=false). }
+ Assume { Type: is_sint32(a) /\ is_sint32(b). (* Lt *) When: b < a. }
Prove: P_S.
------------------------------------------------------------
@@ -260,9 +304,71 @@
typed_test_step_neq_ensures subgoal:
Goal Wp.Tactical.typed_test_step_neq_ensures-1 (generated):
- Assume { (* False/True *) When: (L_LP=true) /\ (L_LQ=false). }
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_test_step_neq_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_neq_ensures-2 (generated):
+ Assume { Type: is_sint32(a) /\ is_sint32(b). (* Gt *) When: a < b. }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_test_step_leq_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_leq_ensures-0 (generated):
+ Assume { Type: is_sint32(a) /\ is_sint32(b). (* Lt *) When: a < b. }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_leq_ensures : Unsuccess
+[wp:script:allgoals]
+ typed_test_step_leq_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_leq_ensures-1 (generated):
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_test_step_leq_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_leq_ensures-2 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_test_step_lt_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_lt_ensures-0 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(b).
+ (* Lt *)
+ When: (2 + a) <= b.
+ (* Pre-condition *)
+ Have: a < b.
+ }
+ Prove: P_S.
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_lt_ensures : Unsuccess
+[wp:script:allgoals]
+ typed_test_step_lt_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_lt_ensures-1 (generated):
Prove: P_S.
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_test_step_lt_ensures subgoal:
+
+ Goal Wp.Tactical.typed_test_step_lt_ensures-2 (generated):
+ Prove: true.
+ Prover Qed returns Valid
+
------------------------------------------------------------
[wp:script:allgoals]
typed_test_step_if_ensures subgoal:
@@ -597,5 +703,5 @@
------------------------------------------------------------
[wp] [Script] Goal typed_test_goal_ex_imply_ensures : Unsuccess
-[wp] Proved goals: 0 / 20
+[wp] Proved goals: 0 / 23
[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..cb1d6260cf6a597c14203c7472f4d1be45a07ef2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-step", "at": 2, "kind": "have",
+ "target": "a_0<=b_0", "pattern": "<=$a$b" },
+ "children": { "Lt": [], "Eq": [],
+ "Gt": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..4347aa1946c8d615ebf0ba21139395638c4d1bef
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-step", "at": 2, "kind": "have",
+ "target": "a_0<b_0", "pattern": "<$a$b" },
+ "children": { "Lt": [], "Eq": [],
+ "Gt": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json
index d57b97bec5d685d7488355c13124afcb50562bd8..8c70aaa2bdeb00c6e9a595aa761fa1580f3d0725 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json
@@ -1,4 +1,6 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
- "select": { "select": "clause-step", "at": 1, "kind": "have",
- "target": "L_LQ!=L_LP", "pattern": "~L_LQL_LP" },
- "children": { "True/False": [], "False/True": [] } } ]
+ "select": { "select": "clause-step", "at": 2, "kind": "have",
+ "target": "b_0!=a_0", "pattern": "~$b$a" },
+ "children": { "Lt": [],
+ "Eq": [ { "prover": "qed", "verdict": "valid" } ],
+ "Gt": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_eq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json
similarity index 100%
rename from src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_eq_ensures.json
rename to src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..d57b97bec5d685d7488355c13124afcb50562bd8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+ "select": { "select": "clause-step", "at": 1, "kind": "have",
+ "target": "L_LQ!=L_LP", "pattern": "~L_LQL_LP" },
+ "children": { "True/False": [], "False/True": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i
index 636387aad7269a8142801360d1d6893981fe84d3..3f7b2dff0491ebc8acbf0a2a923be601a46810d2 100644
--- a/src/plugins/wp/tests/wp_tip/split.i
+++ b/src/plugins/wp/tests/wp_tip/split.i
@@ -52,12 +52,24 @@ void test_step_and(void) {}
/*@ requires LP == LQ ;
@ ensures S ; */
-void test_step_eq(void) {}
+void test_step_peq(void) {}
/*@ requires LP != LQ ;
@ ensures S ; */
+void test_step_pneq(void) {}
+
+/*@ requires a != b ;
+ @ ensures S ; */
void test_step_neq(void) {}
+/*@ requires a <= b ;
+ @ ensures S ; */
+void test_step_leq(void) {}
+
+/*@ requires a < b ;
+ @ ensures S ; */
+void test_step_lt(void) {}
+
/*@ requires (a < b) ? P : Q ;
@ ensures S ; */
void test_step_if(void) {}
@@ -70,7 +82,6 @@ void test_step_fa_if(void) {}
@ ensures S ; */
void test_step_fa_or(void) {}
-
/*@ requires \forall integer i ; Pi(i) && P && Qi(i) && Q && R ;
@ ensures S ; */
void test_step_fa_and(void) {}