diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 194a94cddf0af0ce47f46109f26b99e79052974a..bfb81802ef8ea8ae06508e9c51c5504ccc8ee483 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1736,6 +1736,8 @@ src/plugins/wp/TacBittest.ml: CEA_WP
src/plugins/wp/TacBittest.mli: CEA_WP
src/plugins/wp/TacChoice.ml: CEA_WP
src/plugins/wp/TacChoice.mli: CEA_WP
+src/plugins/wp/TacClear.ml: CEA_WP
+src/plugins/wp/TacClear.mli: CEA_WP
src/plugins/wp/TacCongruence.ml: CEA_WP
src/plugins/wp/TacCongruence.mli: CEA_WP
src/plugins/wp/TacCompound.ml: CEA_WP
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index afc9ef27123cc365fa69e9ac81b39ccb9a6b8468..72ad09daf3b043ff114ba3ab2f89fdfc1681c145 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -86,7 +86,7 @@ PLUGIN_CMO:= \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
Footprint Tactical Strategy \
- TacSplit TacChoice TacRange TacInduction \
+ TacClear TacSplit TacChoice TacRange TacInduction \
TacArray TacCompound TacUnfold \
TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8705e32d693bc36839d8dcb823f7207b669934ce
--- /dev/null
+++ b/src/plugins/wp/TacClear.ml
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Tactical
+
+class clear =
+ object(_)
+ inherit Tactical.make ~id:"Wp.clear"
+ ~title:"Clear"
+ ~descr:"Erase Hypothese"
+ ~params:[]
+
+ method select _feedback sel =
+ match sel with
+ | Clause(Step step) ->
+ let removed = [ "Cleared hypothesis", Conditions.Have Lang.F.p_true] in
+ Applicable (Tactical.replace ~at:step.id removed)
+ | _ ->
+ Not_applicable
+ end
+
+let tactical = Tactical.export (new clear)
diff --git a/src/plugins/wp/TacClear.mli b/src/plugins/wp/TacClear.mli
new file mode 100644
index 0000000000000000000000000000000000000000..acb995cfacab566b1dc65c462e712aaf119d6590
--- /dev/null
+++ b/src/plugins/wp/TacClear.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Built-in Range Tactical (auto-registered) *)
+
+open Tactical
+
+val tactical : tactical
+
+(**************************************************************************)
diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i
new file mode 100644
index 0000000000000000000000000000000000000000..ea270dd7b3688d0cd6cd5c69254280a52fedb2f0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/clear.i
@@ -0,0 +1,28 @@
+/* run.config
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/oracle/@PTEST_NAME@.session
+*/
+/* run.config_qualif
+ DONT_RUN:
+*/
+
+/*@ axiomatic X {
+ predicate P ;
+ predicate Q ;
+ predicate R ;
+ predicate S(integer i) ;
+ }
+*/
+
+int a = 42, b;
+
+/*@ requires P;
+ @ requires Q;
+ @ requires R;
+ @ ensures S(a+b); */
+void clear(void) {
+ if (a < b) {
+ a++;
+ } else {
+ b--;
+ }
+}
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..08dbe46f1e28c74761624ee2a5425cf4f087a582
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -0,0 +1,118 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/clear.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp:script:allgoals]
+ Goal Post-condition (file tests/wp_tip/clear.i, line 21) in 'clear':
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1) /\ is_sint32(b_2).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ (* Pre-condition *)
+ Have: P_R.
+ If a_2 < b_2
+ Then { Have: (a_2 = a_1) /\ (b_2 = b). Have: (1 + a_1) = a. }
+ Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-0 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1) /\ is_sint32(b_2).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ (* Pre-condition *)
+ Have: P_R.
+ If a_2 < b_2
+ Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+ Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-1 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1) /\ is_sint32(b_2).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ If a_2 < b_2
+ Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+ Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-2 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ If a_2 < b_1
+ Then { Have: (a_2 = a_1) /\ (b_1 = b). }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-3 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(b).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-4 (generated):
+ Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_P. }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-5 (generated):
+ Assume { (* Pre-condition *) Have: P_P. }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-6 (generated):
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_ensures : Unsuccess
+[wp] Proved goals: 0 / 1
+[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..64fc7f20266a326aa4eb3d30f70c61d94343fedc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_ensures.json
@@ -0,0 +1,67 @@
+[ { "header": "Clear", "tactic": "Wp.clear", "params": {},
+ "select": { "select": "clause-step", "at": 9, "kind": "have",
+ "target": "(1+a_1)=a_0", "pattern": "=+$a1$a" },
+ "children": { "Cleared hypothesis": [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select": { "select": "clause-step",
+ "at": 4,
+ "kind": "have",
+ "target": "P_R",
+ "pattern": "P_R" },
+ "children": { "Cleared hypothesis":
+ [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 9,
+ "kind": "have",
+ "target": "(a_2=a_0) /\\ (b_2=b_1)",
+ "pattern": "&==$a$a$b$b" },
+ "children":
+ { "Cleared hypothesis":
+ [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 5,
+ "kind": "branch",
+ "target": "a_2<b_2",
+ "pattern": "<$a$b" },
+ "children":
+ { "Cleared hypothesis":
+ [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 3,
+ "kind": "have",
+ "target": "P_Q",
+ "pattern": "P_Q" },
+ "children":
+ { "Cleared hypothesis":
+ [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 0,
+ "kind": "type",
+ "target": "(is_sint32 a_0) /\\ (is_sint32 b_0)",
+ "pattern": "&is_sint32is_sint32$a$b" },
+ "children":
+ { "Cleared hypothesis":
+ [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 1,
+ "kind": "have",
+ "target": "P_P",
+ "pattern": "P_P" },
+ "children":
+ { "Cleared hypothesis": [] } } ] } } ] } } ] } } ] } } ] } } ] } } ]