diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 22ab26bbb6a8c694c5244c66eb5762068ce9e68d..6f832d3856bae523423ff0f8e9c1d192c200f97c 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -111,21 +111,23 @@ let print_file file job =
(* -------------------------------------------------------------------------- *)
type timer = float ref
-type 'a result = Result of 'a | Error of exn
let dt_max tm dt = match tm with Some r when dt > !r -> r := dt | _ -> ()
let dt_add tm dt = match tm with Some r -> r := !r +. dt | _ -> ()
-let return = function Result x -> x | Error e -> raise e
-let catch f x = try Result(f x) with e -> Error e
let time ?rmax ?radd job data =
- begin
- let t0 = Sys.time () in
- let re = catch job data in
+ let t0 = Sys.time () in
+ try
+ let result = job data in
let t1 = Sys.time () in
let dt = t1 -. t0 in
dt_max rmax dt ;
dt_add radd dt ;
- return re ;
- end
+ result
+ with exn ->
+ let t1 = Sys.time () in
+ let dt = t1 -. t0 in
+ dt_max rmax dt ;
+ dt_add radd dt ;
+ raise exn
(* -------------------------------------------------------------------------- *)
(* --- Process --- *)
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 0643c00007d54479b2fbf20d7b197be26bb72232..676bccd9d2ba57bc27f4ac599d39c63632db72fe 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -62,9 +62,7 @@ val print_file : string -> (Format.formatter -> 'a) -> 'a
(* ************************************************************************* *)
type timer = float ref
-type 'a result = Result of 'a | Error of exn
-val catch : ('a -> 'b) -> 'a -> 'b result
-val return : 'a result -> 'a
+
val time : ?rmax:timer -> ?radd:timer -> ('a -> 'b) -> 'a -> 'b
(** Compute the elapsed time with [Sys.time].
The [rmax] timer is maximized and the [radd] timer is cumulated.
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 164a847defba67d1c9dbdbe964127a9f570c01fb..b3312aa812ac6a6f7871fff4ce9e21a350e25c8c 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -469,7 +469,7 @@ let schedule server q =
done
with Queue.Empty -> ()
-let rec run_server server () =
+let server_progress server () =
begin
server.running <- List.filter
(fun task ->
@@ -479,30 +479,29 @@ let rec run_server server () =
server.terminated <- succ server.terminated ; false )
) server.running ;
Array.iter (schedule server) server.queue ;
- try
- Db.yield ();
- fire server.activity ;
- if server.running <> [] then
- begin
- if not server.waiting && is_empty server then
- begin
- fire server.wait ;
- server.waiting <- true ;
- end ;
- true
- end
- else
- begin
- fire server.stop ;
- server.scheduled <- 0 ;
- server.terminated <- 0 ;
- false
- end
- with _ -> (* Db.Cancel ... *)
- cancel_all server ;
- run_server server ()
+ let () =
+ try Db.yield ()
+ with Db.Cancel -> cancel_all server
+ in
+ fire server.activity ;
+ if server.running <> [] then
+ begin
+ if not server.waiting && is_empty server then
+ begin
+ fire server.wait ;
+ server.waiting <- true ;
+ end ;
+ true
+ end
+ else
+ begin
+ fire server.stop ;
+ server.scheduled <- 0 ;
+ server.terminated <- 0 ;
+ false
+ end
end
let launch server =
if server.scheduled > server.terminated
- then ( fire server.start ; !on_idle (run_server server) )
+ then ( fire server.start ; !on_idle (server_progress server) )
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index bc8331ad3c9efd8c9fa18a649cf7e98f0ff840a8..a2ce1c72e39a2115017d7b4a0619014144b8abe7 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2239,8 +2239,10 @@ struct
let fresh sigma t = fresh sigma.pool t
let call f e =
- let v = f e in
- validate "Qed.Subst.add_fun" v ; v
+ if lc_closed e then
+ let v = f e in
+ validate "Qed.Subst.add_fun" v ; v
+ else raise Not_found
let rec compute e = function
| EMPTY -> raise Not_found
diff --git a/src/plugins/wp/Footprint.ml b/src/plugins/wp/Footprint.ml
index a05d0d02ad71ef611b02cd661930c1f72b044c42..0198e11baab73ddf075ac879d968a21867a0e00a 100644
--- a/src/plugins/wp/Footprint.ml
+++ b/src/plugins/wp/Footprint.ml
@@ -31,7 +31,8 @@ let iter f e =
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
- f e ; F.lc_iter (fun e -> Queue.push e q) e
+ if F.lc_closed e then f e ;
+ F.lc_iter (fun e -> Queue.push e q) e
done
let once f e =
@@ -42,7 +43,8 @@ let once f e =
Queue.add e q ;
while not (Queue.is_empty q) do
let e = Queue.pop q in
- f e ; F.lc_iter (fun e -> if once m e then Queue.push e q) e
+ if F.lc_closed e then f e ;
+ F.lc_iter (fun e -> if once m e then Queue.push e q) e
done
(* -------------------------------------------------------------------------- *)
@@ -151,3 +153,5 @@ let lookup ~occur ~inside =
) inside ;
raise Not_found
with Found e -> e
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Footprint.mli b/src/plugins/wp/Footprint.mli
index 868824c83bf007b4a8db215e4e4ae77519e76d87..9e2e9a739a4c629dd7af9e0d3ef293b7de53281d 100644
--- a/src/plugins/wp/Footprint.mli
+++ b/src/plugins/wp/Footprint.mli
@@ -49,3 +49,5 @@ val locate : select:term -> inside:term -> occurrence
(** Retrieve back the [k]-th occurrence of a footprint inside a term. *)
val lookup : occur:occurrence -> inside:term -> term
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 06edf050db3ce0ce5336420e15c4eed6971fce93..8bdd69c1a1ece481b844ab55a24304c804267634 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -312,6 +312,20 @@ and autofork env ~depth fork =
else
( Env.validate env ; Task.return true )
+(* -------------------------------------------------------------------------- *)
+(* --- Apply Script Tactic --- *)
+(* -------------------------------------------------------------------------- *)
+
+let apply env node jtactic subscripts =
+ match jfork (Env.tree env) ?node jtactic with
+ | None -> failwith "Selector not found"
+ | Some fork ->
+ let _,children = ProofEngine.commit fork in
+ reconcile children subscripts ; (*TODO: saveback forgiven script ? *)
+ List.filter
+ (fun (_,node) -> not (ProofEngine.proved node))
+ children
+
(* -------------------------------------------------------------------------- *)
(* --- Script Crawling --- *)
(* -------------------------------------------------------------------------- *)
@@ -348,30 +362,26 @@ let rec crawl env on_child node = function
| Tactic( _ , jtactic , subscripts ) :: alternative ->
begin
- match jfork (Env.tree env) ?node jtactic with
- | None ->
- Wp_parameters.warning
- "Script Error: on goal %a@\n\
- can not apply '%s'@\n\
- @[<hov 2>Params: %a@]@\n\
- @[<hov 2>Select: %a@]@."
- WpPropId.pretty (Env.goal env node).po_pid
- jtactic.tactic
- Json.pp jtactic.params
- Json.pp jtactic.select ;
- crawl env on_child node alternative
- | Some fork ->
- (*TODO: saveback forgiven script *)
- let _,children = ProofEngine.commit fork in
- reconcile children subscripts ;
- let residual = List.filter
- (fun (_,node) -> not (ProofEngine.proved node))
- children in
- if residual = [] then
- Env.validate env
- else
- List.iter (fun (_,n) -> on_child n) children ;
- Task.return ()
+ try
+ let residual = apply env node jtactic subscripts in
+ if residual = [] then
+ Env.validate env
+ else
+ List.iter (fun (_,n) -> on_child n) residual ;
+ Task.return ()
+ with exn when Wp_parameters.protect exn ->
+ Wp_parameters.warning
+ "Script Error: on goal %a@\n\
+ can not apply '%s'@\n\
+ exception %S@\n\
+ @[<hov 2>Params: %a@]@\n\
+ @[<hov 2>Select: %a@]@."
+ WpPropId.pretty (Env.goal env node).po_pid
+ jtactic.tactic
+ (Printexc.to_string exn)
+ Json.pp jtactic.params
+ Json.pp jtactic.select ;
+ crawl env on_child node alternative
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 45bd15f9cb42fc358617c41bbd8378979d3d690a..87fc5241966e3870a413dad3411aded9eb3e430a 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -121,7 +121,15 @@ let spawn wpo ~delayed
prover , task
) provers)
else
- let process = simplify ?start ?result wpo in
+ let process = simplify ?start ?result wpo >>= fun ok ->
+ begin
+ match success with
+ | None -> ()
+ | Some on_success ->
+ on_success wpo (if ok then Some VCS.Qed else None) ;
+ end ;
+ Task.return ()
+ in
let thread = Task.thread process in
let server = ProverTask.server () in
Task.spawn server ?pool thread
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
index 7e4bcea281b188bdcd20a782ff6423032d5941ec..260f73c47cb6ee354cdba05c71dfc9460a83c76a 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And.json
@@ -1,24 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_P1 i_0) /\\ (P_Q1 i_2) /\\ (P_P2 i_1 i_2)\n/\\ (exists i_3:int.\n (P_Q2 i_0 i_3))",
- "pattern": "\\E\\E\\E&P_P1P_Q1P_P2\\E#3#1#2#1P_Q2" },
- "children": { "Goal 1/2": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0511159896851 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int. (P_Q1 i_0) /\\ (P_P2 i_1 i_0)",
- "pattern": "\\E\\E&P_Q1P_P2#1#0#1" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0514709949493 } ] } } ],
- "Goal 2/2": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0521941184998 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0:int. (P_P1 i_0) /\\ (exists i_1:int.\n (P_Q2 i_0 i_1))",
- "pattern": "\\E&P_P1\\E#1P_Q2#1#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515058040619 } ] } } ] } } ]
+ "pattern": "\\E" },
+ "children": { "Goal 1/2": [], "Goal 2/2": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
index a908ac4adb3e577d040a3f24b4c6f0f06f56c053..212235b3fe925038ba1a99ed6b4ec08e7d3a6951 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_And_bis.json
@@ -1,34 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2,i_3:int.\n(P_Q1 1) /\\ (P_P2 i_0 i_1) /\\ (P_R2 i_1 i_2)\n/\\ (exists i_4:int.\n (P_Q2 i_3 i_4))",
- "pattern": "\\E\\E\\E\\E&P_Q1P_P2P_R2\\E1#4#3#3#2" },
- "children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0512578487396 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1:int. (P_Q2 i_0 i_1)",
- "pattern": "\\E\\EP_Q2#1#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515179634094 } ] } } ],
- "Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0517938137054 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "exists i_0,i_1,i_2:int. (P_P2 i_2 i_1) /\\ (P_R2 i_1 i_0)",
- "pattern": "\\E\\E\\E&P_P2P_R2#0#1#1#2" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515098571777 } ] } } ],
- "Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0528788566589 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "(P_Q1 1)",
- "pattern": "P_Q11" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515050888062 } ] } } ] } } ]
+ "pattern": "\\EP_Q11" },
+ "children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
index db3e60070bdd86a16f0ee3e96303a5cbe6c4c2d6..c70dddec42c798d67d2e64caedcd77123e5f7e9c 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Goal_Exist_Or.json
@@ -1,16 +1,6 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1,i_2:int.\n(P_Q1 1) \\/ (P_P1 i_0) \\/ (P_P2 i_1 i_2) \\/ (exists i_3:int.\n (P_Q2 i_0 i_3))",
- "pattern": "\\E\\E\\E|P_Q1P_P1P_P2\\E1#3#2#1P_Q2" },
- "children": { "Distrib (exists or)": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515348911285 },
- { "header": "NOP",
- "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-goal",
- "target": "(P_Q1 1) \\/ (exists i_0:int.\n (P_P1 i_0)) \\/ (exists i_0,i_1:int.\n (P_P2 i_1 i_0))\n\\/ (exists i_0,i_1:int.\n (P_Q2 i_0 i_1))",
- "pattern": "|P_Q1\\E\\E\\E1P_P1\\E\\E#0P_P2P_Q2#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0513439178467 } ] } } ] } } ]
+ "pattern": "\\EP_Q11" },
+ "children": { "Split": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
index bb1f7b0cb5bf7ff1d2360fa531444508b977cf6d..5a6e83f45232bf50cfe1b17f56085bb45f633852 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_And.json
@@ -1,18 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2:int.\n(P_Q1 1) /\\ (P_P1 i_0) /\\ (P_P2 i_1 i_2) /\\ (forall i_3:int.\n (P_Q2 i_0 i_3))",
- "pattern": "\\F\\F\\F&P_Q1P_P1P_P2\\F1#3#2#1P_Q2" },
- "children": { "Distrib (forall and)": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.051558971405 },
- { "header": "NOP",
- "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0,
- "kind": "have",
- "target": "(P_Q1 1) /\\ (forall i_0:int.\n (P_P1 i_0)) /\\ (forall i_0,i_1:int.\n (P_P2 i_1 i_0))\n/\\ (forall i_0,i_1:int.\n (P_Q2 i_0 i_1))",
- "pattern": "&P_Q1\\F\\F\\F1P_P1\\F\\F#0P_P2P_Q2#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0513830184937 } ] } } ] } } ]
+ "pattern": "\\FP_Q11" },
+ "children": { "Split (distrib forall and)": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
index 815a03e3dd65c3515a850fd69d37fe3eb51ae0cf..43bb875d32ba27e9ab410917a1c9789f632d467d 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.session/script/split_ensures_Hyp_Forall_Or_bis.json
@@ -1,37 +1,6 @@
-[ { "header": "Split", "tactic": "Wp.split", "params": {},
+[ { "prover": "script", "verdict": "unknown" },
+ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 0, "kind": "have",
"target": "forall i_0,i_1,i_2,i_3:int.\n(P_Q1 1) \\/ (P_P2 i_0 i_1) \\/ (P_R2 i_1 i_2)\n\\/ (forall i_4:int.\n (P_Q2 i_3 i_4))",
- "pattern": "\\F\\F\\F\\F|P_Q1P_P2P_R2\\F1#4#3#3#2" },
- "children": { "Goal 1/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0511250495911 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0, "kind": "have",
- "target": "forall i_0,i_1:int. (P_Q2 i_0 i_1)",
- "pattern": "\\F\\FP_Q2#1#0" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515208244324 } ] } } ],
- "Goal 2/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0517539978027 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0, "kind": "have",
- "target": "forall i_0,i_1,i_2:int. (P_P2 i_2 i_1) \\/ (P_R2 i_1 i_0)",
- "pattern": "\\F\\F\\F|P_P2P_R2#0#1#1#2" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.0515398979187 } ] } } ],
- "Goal 3/3": [ { "prover": "alt-ergo", "verdict": "unknown",
- "time": 0.0528609752655 },
- { "header": "NOP", "tactic": "Wp.Test.NOP",
- "params": {},
- "select": { "select": "clause-step",
- "at": 0, "kind": "have",
- "target": "(P_Q1 1)",
- "pattern": "P_Q11" },
- "children": { "Nop": [ { "prover": "alt-ergo",
- "verdict": "unknown",
- "time": 0.051561832428 } ] } } ] } } ]
+ "pattern": "\\FP_Q11" },
+ "children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
index 7d6f12f66d12dcc3006b3c17fb5bc2a54bbc3c66..119e483c91cbac96b94d8683183e2192941cf7a6 100644
--- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
@@ -17,7 +17,7 @@
predicate R2(integer a1, integer a2) reads \nothing ;
} */
-/*@ ensures Goal_Exist_Or:
+/*@ ensures Goal_Exist_Or:
(\exists integer a, b, c ;
P1(a) || P2(b, c) || Q1(1) || \exists integer d ; Q2(a,d)) ;
@@ -29,7 +29,7 @@
(\exists integer a, b, c, d ;
P2(a, b) && R2(b, c) && Q1(1) && \exists integer e ; Q2(d,e)) ;
- @ ensures Hyp_Forall_And:
+ @ ensures Hyp_Forall_And:
(\forall integer a, b, c ;
P1(a) && P2(b, c) && Q1(1) && \forall integer d ; Q2(a,d)
) ==>
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index a5f8a971b9f1229e8509d038e8f7451dafdfa9f7..e2661ac0ea5be08409c69084618d3cb685876c18 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index a5f8a971b9f1229e8509d038e8f7451dafdfa9f7..e2661ac0ea5be08409c69084618d3cb685876c18 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.017,
"steps": 22 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index 1a1c4c0451c01821da44f4cd61861b8ebeee4f02..a9310f3d13966a1a1a987551a3cfb57c72a1e8cd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0236,
"steps": 41 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index 398a69be748b427406223332d1c8447708dc51e1..a5b7496b8bcac1057fc2ee1bfc1baa80fad18099 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.018,
"steps": 29 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
index d7d87cb0431b99609b2b733ee68bb9ac2cdc04e6..2ee61e01ef268896d390d325575ef4051af1088e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 9927a473006bfd0846ae22f978f724ca10e5e553..6defa5bcd74401f918dc86a7cc117daec22e3cc0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0177,
"steps": 40 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index e43bf2a0c07c931be6a637bc59d7981d08afa12f..07c88e21be0523b36d4e4beb3bc08582fc5171d3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
+ "pattern": "\\E$i0$i$j$j9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0154,
"steps": 24 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index 8138f144480b3491b3bd4e0ba6074c5cd9988c62..6f266473c3da74f3125a63e16abeffe0f28b841c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0167,
"steps": 33 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index c110027873b58604a7e9b1f4add93925e424cd1f..33301d71a33e5ae00a155943d5cecf22939281b0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0167,
"steps": 33 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
index 2f0e9f12c125589ccbe9b513e6c1145d72b89497..cb380dd3e39f3d5b41787e5481e2eb7b62264873 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.011,
"steps": 16 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index 0f331f4933d265794ca3c72277892cdaeef876be..a9966d41d85a805900702002ac776ddb4a8b2853 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0196,
"steps": 39 } ],
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 9fc6a77f392331e6771b07d65d55ebfb62b84ae8..0be615900200669f51459d70bcd89d583f0a82b8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -1,7 +1,7 @@
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
- "pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
+ "pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid", "time": 0.0152,
"steps": 27 } ],
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 94f5b8131ffe76c1ea358b39e5130bc4b1088a3f..9335161d010553d664de54516270ead945483112 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1239,3 +1239,13 @@ let print_generated ?header file =
end
(* -------------------------------------------------------------------------- *)
+(* --- Debugging --- *)
+(* -------------------------------------------------------------------------- *)
+
+let protect e =
+ if debug_atleast 1 then false else
+ match e with
+ | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
+ | _ -> true
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index a37b5e895a7470f21a738e3c69a5c15dc9566796..97392faa580e3f4b36d686429ba3eb7b53c90c1d 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -175,3 +175,5 @@ val print_generated: ?header:string -> string -> unit
(** print the given file if the debugging category
"print-generated" is set *)
val cat_print_generated: category
+
+val protect : exn -> bool
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index a36b16398193812618864a7ab292f6d1d012b751..e5459e75b894fda2a88fd783408471bef27d773b 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -190,7 +190,14 @@ struct
let is_trivial g = Conditions.is_trivial g.sequent
- let apply phi g = g.sequent <- phi g.sequent
+ let apply option phi g =
+ try g.sequent <- phi g.sequent
+ with exn when Wp_parameters.protect exn ->
+ Wp_parameters.warning ~current:false ~once:true
+ "Goal simplification aborted (%s):@\n\
+ Exception %S@\n\
+ Re-run with debug level 1+ for details."
+ option (Printexc.to_string exn)
let default_simplifiers = [
Wp_parameters.SimplifyIsCint.get, Cint.is_cint_simplifier ;
@@ -200,23 +207,23 @@ struct
let preprocess g =
if Wp_parameters.Let.get () then
begin
- apply Conditions.introduction_eq g ;
+ apply "introcution" Conditions.introduction_eq g ;
let fold acc (get,solver) = if get () then solver::acc else acc in
let solvers = List.fold_left fold [] default_simplifiers in
- apply (Conditions.simplify ~solvers) g ;
+ apply "-wp-simplify-*" (Conditions.simplify ~solvers) g ;
if Wp_parameters.FilterInit.get ()
- then apply Conditions.init_filter g ;
+ then apply "-wp-filter-init" Conditions.init_filter g ;
if Wp_parameters.Prune.get ()
- then apply (Conditions.pruning ~solvers) g ;
+ then apply "-wp-pruning" (Conditions.pruning ~solvers) g ;
if Wp_parameters.Filter.get ()
- then apply Conditions.filter g ;
+ then apply "-wp-filter" Conditions.filter g ;
if Wp_parameters.Parasite.get ()
- then apply Conditions.parasite g ;
+ then apply "-wp-parasite" Conditions.parasite g ;
end
else
begin
if Wp_parameters.Clean.get ()
- then apply Conditions.clean g ;
+ then apply "-wp-clean" Conditions.clean g ;
end ;
if Conditions.is_trivial g.sequent then
g.sequent <- Conditions.trivial ;