diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index 856a047be4e3663416594c297fa53e15eff655a4..da074d2311efa22959f55a17467314188ed34ac0 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -252,12 +252,6 @@ let wp_panel
~packing:(addcontrol 1 2)
Wp_parameters.Steps.get Wp_parameters.Steps.set demon ;
- Gtk_form.label ~text:"Depth" ~packing:(addcontrol 2 1) () ;
- Gtk_form.spinner ~lower:0 ~upper:100000
- ~tooltip:"Search space bound for alt-ergo prover"
- ~packing:(addcontrol 2 2)
- Wp_parameters.Depth.get Wp_parameters.Depth.set demon ;
-
Gtk_form.label ~text:"Timeout" ~packing:(addcontrol 3 1) () ;
Gtk_form.spinner ~lower:0 ~upper:100000
~tooltip:"Timeout for proving one proof obligation"
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 36edf5745028932f70ab1c221f5bab26a0ba30bf..e195b340f27b94255147f418ceb411639437cc2c 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -51,22 +51,12 @@ let stepout_for = function
Some spin
| _ -> None
-let depth_for = function
- | VCS.NativeAltErgo ->
- let value = Wp_parameters.Depth.get () in
- let spin = new Widget.spinner
- ~tooltip:"Search Depth (-age-bound, 0 for prover default)"
- ~min:0 ~step:100 ~value () in
- Some spin
- | _ -> None
-
class prover ~(console:Wtext.text) ~prover =
let tooltip = "Configure Prover" in
let content = new Wpane.form () in
let result = new Widget.label ~style:`Code ~align:`Center ~text:"No Result" () in
let timeout = timeout_for prover in
let stepout = stepout_for prover in
- let depth = depth_for prover in
object(self)
inherit Wpalette.tool ~tooltip ~content:content#widget ()
initializer
@@ -75,7 +65,6 @@ class prover ~(console:Wtext.text) ~prover =
content#add_row ~xpadding:6 ~ypadding:4 result#coerce ;
Wutil.on timeout (fun spin -> content#add_field ~label:"Timeout" spin#coerce) ;
Wutil.on stepout (fun spin -> content#add_field ~label:"Steps" spin#coerce) ;
- Wutil.on depth (fun spin -> content#add_field ~label:"Depth" spin#coerce) ;
end
method prover = prover
@@ -101,7 +90,6 @@ class prover ~(console:Wtext.text) ~prover =
VCS.valid = false ;
VCS.timeout = spinner timeout ;
VCS.stepout = spinner stepout ;
- VCS.depth = spinner depth ;
} in
let result wpo _prv _res = self#update wpo in
let task = Prover.prove ~config ~result wpo prover in
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 9bc0cf1931a1ea4d1942d60313099e0e3b65e683..6649d349e675155a87176d1a248a5943af7414fe 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -339,8 +339,7 @@ let json_of_result (p : VCS.prover) (r : VCS.result) =
let verdict = "verdict" , json_of_verdict r.verdict in
let time = if r.prover_time > 0.0 then [ "time" , `Float r.prover_time ] else [] in
let steps = if r.prover_steps > 0 then [ "steps" , `Int r.prover_steps ] else [] in
- let depth = if r.prover_depth > 0 then [ "depth" , `Int r.prover_depth ] else [] in
- `Assoc (name :: verdict :: (time @ steps @ depth))
+ `Assoc (name :: verdict :: (time @ steps))
let prover_of_json js =
try VCS.prover_of_name (js >? "prover" |> Json.string)
@@ -350,8 +349,7 @@ let result_of_json js =
let verdict = try js >? "verdict" |> verdict_of_json with _ -> VCS.NoResult in
let time = try js >? "time" |> Json.float with _ -> 0.0 in
let steps = try js >? "steps" |> Json.int with _ -> 0 in
- let depth = try js >? "depth" |> Json.int with _ -> 0 in
- VCS.result ~time ~steps ~depth verdict
+ VCS.result ~time ~steps verdict
(* -------------------------------------------------------------------------- *)
(* --- Script --- *)
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 205e4e09cf77002d6c3605c250711db2221a562d..19b82a4ef4163d4d2ac13019ba5a144082d7d442 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -352,7 +352,6 @@ class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
val mutable unsat = false
val mutable timer = 0.0
val mutable steps = 0
- val mutable depth = 0
method private time t = timer <- t
@@ -398,7 +397,7 @@ class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
raise Not_found in
VCS.result
~time:(if gui then 0.0 else timer)
- ~steps ~depth verdict
+ ~steps verdict
with
| Not_found when Wp_parameters.Check.get () ->
if r = 0 then VCS.checked
@@ -422,13 +421,11 @@ class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
method prove =
files <- lines ;
- depth <- VCS.get_depth config ;
if gui then ergo#set_command (Wp_parameters.AltGrErgo.get ()) ;
if Wp_parameters.Check.get () then
ergo#add ["-type-only"]
else
begin
- ergo#add_positive ~name:"-age-bound" ~value:depth ;
ergo#add_parameter ~name:"-proof" Wp_parameters.ProofTrace.get ;
ergo#add_parameter ~name:"-model" Wp_parameters.ProofTrace.get ;
end ;
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index 69aa5ea1cd391c6ac1dbbae0653f96a040f495bb..e9bb77dc5b58e7db6a8c749cb56b436ddcc6f753 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -141,10 +141,6 @@ let stepout = function
| None -> Wp_parameters.Steps.get ()
| Some t -> t
-let depth = function
- | None -> Wp_parameters.Depth.get ()
- | Some t -> t
-
let pp_file ~message ~file =
if Sys.file_exists file then
Log.print_on_output
diff --git a/src/plugins/wp/ProverTask.mli b/src/plugins/wp/ProverTask.mli
index e3a567f91212221236f292dfc94a84c68dbf91bf..43fff7d910c0fda972e0ddbfae5e3855e066119b 100644
--- a/src/plugins/wp/ProverTask.mli
+++ b/src/plugins/wp/ProverTask.mli
@@ -56,7 +56,6 @@ val location : string -> int -> Lexing.position
val timeout : int option -> int
val stepout : int option -> int
-val depth : int option -> int
type logs = [ `OUT | `ERR | `BOTH ]
class virtual command : string ->
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 5118efccbcfd128a4172e3a9bd1cf7e1000d09b5..6f05aaeaa80b225700cd0a60651aa1c18ce1addf 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -235,7 +235,6 @@ type config = {
valid : bool ;
timeout : int option ;
stepout : int option ;
- depth : int option ;
}
let param f = let v = f() in if v>0 then Some v else None
@@ -244,10 +243,9 @@ let current () = {
valid = false ;
timeout = param Wp_parameters.Timeout.get ;
stepout = param Wp_parameters.Steps.get ;
- depth = param Wp_parameters.Depth.get ;
}
-let default = { valid = false ; timeout = None ; stepout = None ; depth = None }
+let default = { valid = false ; timeout = None ; stepout = None }
let get_timeout = function
| { timeout = None } -> Wp_parameters.Timeout.get ()
@@ -257,10 +255,6 @@ let get_stepout = function
| { stepout = None } -> Wp_parameters.Steps.get ()
| { stepout = Some t } -> t
-let get_depth = function
- | { depth = None } -> Wp_parameters.Depth.get ()
- | { depth = Some t } -> t
-
(* -------------------------------------------------------------------------- *)
(* --- Results --- *)
(* -------------------------------------------------------------------------- *)
@@ -281,7 +275,6 @@ type result = {
solver_time : float ;
prover_time : float ;
prover_steps : int ;
- prover_depth : int ;
prover_errpos : Lexing.position option ;
prover_errmsg : string ;
}
@@ -305,17 +298,13 @@ let configure r =
let stepout =
if r.prover_steps > 0 && r.prover_time <= 0.0 then
let stepout = Wp_parameters.Steps.get () in
- let margin = 1000 + r.prover_depth in
+ let margin = 1000 in
Some(max stepout margin)
else None in
- let depth =
- if r.prover_depth > 0 then Some r.prover_depth else None
- in
{
valid ;
timeout ;
stepout ;
- depth ;
}
let time_fits t =
@@ -330,23 +319,16 @@ let step_fits n =
let stepout = Wp_parameters.Steps.get () in
stepout = 0 || n < stepout
-let depth_fits n =
- n = 0 ||
- let depth = Wp_parameters.Depth.get () in
- depth = 0 || n < depth
-
let autofit r =
time_fits r.prover_time &&
- step_fits r.prover_steps &&
- depth_fits r.prover_depth
+ step_fits r.prover_steps
-let result ?(solver=0.0) ?(time=0.0) ?(steps=0) ?(depth=0) verdict =
+let result ?(solver=0.0) ?(time=0.0) ?(steps=0) verdict =
{
verdict ;
solver_time = solver ;
prover_time = time ;
prover_steps = steps ;
- prover_depth = depth ;
prover_errpos = None ;
prover_errmsg = "" ;
}
@@ -364,7 +346,6 @@ let failed ?pos msg = {
solver_time = 0.0 ;
prover_time = 0.0 ;
prover_steps = 0 ;
- prover_depth = 0 ;
prover_errpos = pos ;
prover_errmsg = msg ;
}
@@ -439,7 +420,6 @@ let merge r1 r2 =
solver_time = max r1.solver_time r2.solver_time ;
prover_time = max r1.prover_time r2.prover_time ;
prover_steps = max r1.prover_steps r2.prover_steps ;
- prover_depth = max r1.prover_depth r2.prover_depth ;
prover_errpos = err.prover_errpos ;
prover_errmsg = err.prover_errmsg ;
}
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 2b696a3a725c937a51b9a766415c0ee08e580d2b..0b753f34975bef35c69dc66191c317a0f613928b 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -100,7 +100,6 @@ type config = {
valid : bool ;
timeout : int option ;
stepout : int option ;
- depth : int option ;
}
@@ -109,7 +108,6 @@ val default : config (** all None *)
val get_timeout : config -> int (** 0 means no-timeout *)
val get_stepout : config -> int (** 0 means no-stepout *)
-val get_depth : config -> int (** 0 means prover default *)
(** {2 Results} *)
@@ -129,7 +127,6 @@ type result = {
solver_time : float ;
prover_time : float ;
prover_steps : int ;
- prover_depth : int ;
prover_errpos : Lexing.position option ;
prover_errmsg : string ;
}
@@ -144,7 +141,7 @@ val timeout : int -> result
val computing : (unit -> unit) -> result
val failed : ?pos:Lexing.position -> string -> result
val kfailed : ?pos:Lexing.position -> ('a,Format.formatter,unit,result) format4 -> 'a
-val result : ?solver:float -> ?time:float -> ?steps:int -> ?depth:int -> verdict -> result
+val result : ?solver:float -> ?time:float -> ?steps:int -> verdict -> result
val is_auto : prover -> bool
val is_verdict : result -> bool
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 8babaed7338b4a43534c9bec6e54fdb475af7b5b..641359887d9438f08d426b381c62f7790180c784 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -813,8 +813,6 @@ let pp_wp_parameters fmt =
if tm > 10 then Format.fprintf fmt " -wp-timeout %d" tm ;
let st = Wp_parameters.Steps.get () in
if tm > 10 then Format.fprintf fmt " -wp-steps %d" st ;
- let dp = Wp_parameters.Depth.get () in
- if dp > 0 then Format.fprintf fmt " -wp-depth %d" dp ;
if not (Kernel.SignedOverflow.get ()) then
Format.pp_print_string fmt " -no-warn-signed-overflow" ;
if Kernel.UnsignedOverflow.get () then
diff --git a/src/plugins/wp/tests/wp_plugin/nth.i b/src/plugins/wp/tests/wp_plugin/nth.i
index ec2167c7987fb03177d475b7598304f8d70888d4..9c53c9927da577d50605072427990d3238fbbdb0 100644
--- a/src/plugins/wp/tests/wp_plugin/nth.i
+++ b/src/plugins/wp/tests/wp_plugin/nth.i
@@ -1,6 +1,6 @@
/* run.config_qualif
- OPT: -wp-prover alt-ergo -wp-depth 16 -wp-prop=-lack
- OPT: -wp-prover why3:alt-ergo -wp-depth 16
+ OPT: -wp-prover alt-ergo -wp-prop=-lack
+ OPT: -wp-prover why3:alt-ergo
*/
/*@
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle
index e86cc65ef01943ade9b9d4597d5293ac746f53dc..7409dcd50ccde6a33b8b0fbe710f6cab78e32164 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...]
+# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
index 0815def0020a7db6e8c38ed38a666140849c8555..3b2532f0d41508e2d60c23b61489597c09da6580 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...]
+# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
index c2817aedca9085f5f44158f0d53162e6d5aa1b61..87fabd092458751d9da6d409bde18a8f9ce64434 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...]
+# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index 60d453b63fce576ea6d8f13808e8726606e9ea2e..80b9ff0503b45f67bd3b130d0c8b3dc1b7803b79 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 -wp-depth 16 [...]
+# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 1500 [...]
[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
index c637752ab865f76a65a39b925f46ab5253e3bd37..92097c803f9ea4eea08995f5a907a9767c02eac4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 50 -wp-depth 16 [...]
+# frama-c -wp -wp-model 'Typed (Caveat)' -wp-timeout 45 -wp-steps 50 [...]
[kernel] Parsing tests/wp_plugin/sequence.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_plugin/sequence.i b/src/plugins/wp/tests/wp_plugin/sequence.i
index cae97dbfe14a70367b02b2d71f1045a26ec1f6fb..5faaa939e50a2b3f54b985f7330716a676761a92 100644
--- a/src/plugins/wp/tests/wp_plugin/sequence.i
+++ b/src/plugins/wp/tests/wp_plugin/sequence.i
@@ -3,9 +3,9 @@
*/
/* run.config_qualif
- OPT: -wp -wp-model Caveat -wp-prover alt-ergo -wp-depth 16 -wp-prop="-ko"
- OPT: -wp -wp-model Caveat -wp-prover why3:alt-ergo -wp-depth 16 -wp-prop="-ko,-bug_why3"
- OPT: -wp -wp-model Caveat -wp-prover alt-ergo -wp-depth 16 -wp-prop="ko" -wp-steps 50
+ OPT: -wp -wp-model Caveat -wp-prover alt-ergo -wp-prop="-ko"
+ OPT: -wp -wp-model Caveat -wp-prover why3:alt-ergo -wp-prop="-ko,-bug_why3"
+ OPT: -wp -wp-model Caveat -wp-prover alt-ergo -wp-prop="ko" -wp-steps 50
*/
//@ ghost int call_seq;
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index f0888501c367b969eb0794c76e1ee2bcb80c53af..6a14906d3e05b1fdea4de19b80fa4ae03dab3d67 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -497,15 +497,6 @@ module Drivers =
let help = "Load drivers for linking to external libraries"
end)
-let () = Parameter_customize.set_group wp_prover
-module Depth =
- Int(struct
- let option_name = "-wp-depth"
- let default = 0
- let arg_name = "p"
- let help = "Set depth of exploration for provers."
- end)
-
let () = Parameter_customize.set_group wp_prover
module Steps =
Int(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 04a35a46e48af144ad679b1dc166cdadaf331901..8918d667abf36e6abdcfe1047302addcad2414f9 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -104,7 +104,6 @@ module CoqTimeout: Parameter_sig.Int
module CoqCompiler : Parameter_sig.String
module CoqIde : Parameter_sig.String
module CoqProject : Parameter_sig.String
-module Depth: Parameter_sig.Int
module Steps: Parameter_sig.Int
module Procs: Parameter_sig.Int
module ProofTrace: Parameter_sig.Bool