diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 177752de55e92d4621e922a49bda256ae826f11a..45339f9fa7496a9d2b2dca9d7cc28e3f20245792 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -171,7 +171,7 @@ let refusage_param ~byref ~context x =
| WpContext.Kf f ->
Some f ,
WpStrategy.is_main_init f ||
- Wp_parameters.InitAlias.get () ||
+ Wp_parameters.AliasInit.get () ||
( WpStrategy.isInitConst () &&
WpStrategy.isGlobalInitConst x ) in
match RefUsage.get ?kf ~init x with
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_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c
index f6cc4a0d40e56145105da75bd539bc6ce19c3fa4..7866143743cdc9c7b317582af5b805e3865afd31 100644
--- a/src/plugins/wp/tests/wp_acsl/classify_float.c
+++ b/src/plugins/wp/tests/wp_acsl/classify_float.c
@@ -1,7 +1,7 @@
/* run.config_qualif
OPT: -wp-prover alt-ergo
OPT: -wp-prover why3:alt-ergo
- OPT: -wp-prover coq -wp-script tests/wp_acsl/classify_float.script
+ OPT: -wp-prover coq -wp-coq-script tests/wp_acsl/classify_float.script
*/
/*@
diff --git a/src/plugins/wp/tests/wp_acsl/equal.i b/src/plugins/wp/tests/wp_acsl/equal.i
index 3021b7c0498d0511df76743101328e1d3476908c..160b60ae74d0b7b905278c3221368903d6357c54 100644
--- a/src/plugins/wp/tests/wp_acsl/equal.i
+++ b/src/plugins/wp/tests/wp_acsl/equal.i
@@ -1,5 +1,9 @@
+/* run.config
+ STDOPT: +"-wp-no-extensional"
+*/
/* run.config_qualif
COMMENT:
+ STDOPT: +"-wp-no-extensional"
*/
/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/wp/tests/wp_acsl/init_label.i b/src/plugins/wp/tests/wp_acsl/init_label.i
index 24672c3143c13dd138d0c5ca27093d9c738c89a4..25f54a1e067f0a8d30da4a33da26bf10e99645bd 100644
--- a/src/plugins/wp/tests/wp_acsl/init_label.i
+++ b/src/plugins/wp/tests/wp_acsl/init_label.i
@@ -1,4 +1,10 @@
-
+/* run.config
+ STDOPT: +"-wp-no-extensional"
+*/
+/* run.config_qualif
+ COMMENT:
+ STDOPT: +"-wp-no-extensional"
+*/
int A[20] = {10,11,12} ;
diff --git a/src/plugins/wp/tests/wp_acsl/init_value.i b/src/plugins/wp/tests/wp_acsl/init_value.i
index b9d9caeabadd4510e4a64607a265906f70f4274c..46011a6a54c96ee222e31dabb01a7ec64539aefb 100644
--- a/src/plugins/wp/tests/wp_acsl/init_value.i
+++ b/src/plugins/wp/tests/wp_acsl/init_value.i
@@ -1,10 +1,10 @@
/* run.config
- OPT: -wp-init-const -wp-no-let
- OPT: -main main_ko -wp-no-let
+ OPT: -wp-no-let
+ OPT: -main main_ko -wp-no-let -wp-no-init-const
*/
/* run.config_qualif
- OPT: -wp-init-const -wp -wp-par 1 -wp-prop="-qed_ko"
- OPT: -main main_ko -wp-par 1 -wp-prop qed_ko -wp-steps 50
+ OPT: -wp -wp-par 1 -wp-prop="-qed_ko"
+ OPT: -main main_ko -wp-par 1 -wp-prop qed_ko -wp-steps 50 -wp-no-init-const
*/
/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
index e1cad92e54170a2376e7f1c2f93b2b1f3a4f4d4d..a5e1f5ba07cab2b47513553fd8ccba7343241e68 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/equal.res.oracle
@@ -7,7 +7,7 @@
Function simple_array
------------------------------------------------------------
-Goal Post-condition (file tests/wp_acsl/equal.i, line 18) in 'simple_array':
+Goal Post-condition (file tests/wp_acsl/equal.i, line 22) in 'simple_array':
Let x = t0_0[0].
Let x_1 = t0_0[1].
Assume {
@@ -21,7 +21,7 @@ Prove: EqArray1_int(2, t0_0, t1_0[0 <- x][1 <- x_1]).
Function simple_struct
------------------------------------------------------------
-Goal Post-condition (file tests/wp_acsl/equal.i, line 12) in 'simple_struct':
+Goal Post-condition (file tests/wp_acsl/equal.i, line 16) in 'simple_struct':
Prove: true.
------------------------------------------------------------
@@ -29,7 +29,7 @@ Prove: true.
Function with_array_struct
------------------------------------------------------------
-Goal Post-condition (file tests/wp_acsl/equal.i, line 24) in 'with_array_struct':
+Goal Post-condition (file tests/wp_acsl/equal.i, line 28) in 'with_array_struct':
Let a = st0_0.F2_St_tab.
Let a_1 = st1_0.F2_St_tab.
Assume {
@@ -45,7 +45,7 @@ Prove: EqS2_St(st0_0, st1_0).
Function with_ptr_and_array_struct
------------------------------------------------------------
-Goal Post-condition (file tests/wp_acsl/equal.i, line 43) in 'with_ptr_and_array_struct':
+Goal Post-condition (file tests/wp_acsl/equal.i, line 47) in 'with_ptr_and_array_struct':
Let a = q0_0.F4_Q_qs.
Let a_1 = q1_0.F4_Q_qs.
Let a_2 = q0_0.F4_Q_qt.
@@ -64,7 +64,7 @@ Prove: EqS4_Q(q0_0, q1_0).
Function with_ptr_array
------------------------------------------------------------
-Goal Post-condition (file tests/wp_acsl/equal.i, line 36) in 'with_ptr_array':
+Goal Post-condition (file tests/wp_acsl/equal.i, line 40) in 'with_ptr_array':
Assume {
(* Goal *)
When: forall i : Z. ((0 <= i) -> ((i <= 4) -> (tp1_0[i] = tp0_0[i]))).
@@ -76,7 +76,7 @@ Prove: EqArray1_pointer(5, tp0_0, tp1_0).
Function with_ptr_struct
------------------------------------------------------------
-Goal Post-condition (file tests/wp_acsl/equal.i, line 30) in 'with_ptr_struct':
+Goal Post-condition (file tests/wp_acsl/equal.i, line 34) in 'with_ptr_struct':
Assume { (* Goal *) When: (sp1_0.F3_Sp_p) = (sp0_0.F3_Sp_p). }
Prove: EqS3_Sp(sp0_0, sp1_0).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
index 76693dd4e7cffda1b00cb9c76a0e587a1d561827..eaf906f5ee4db946fea90806e5400e116ac17f29 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
-[kernel] tests/wp_acsl/init_label.i:21: Warning:
+[kernel] tests/wp_acsl/init_label.i:27: Warning:
No code nor implicit assigns clause for function main, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
index 9e580ba61f011754b8d6b9490e4514b540f27bd4..81dd069d35a8761f1807ebab8f5a5aa6e6538aaa 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/init_label.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
-[kernel] tests/wp_acsl/init_label.i:21: Warning:
+[kernel] tests/wp_acsl/init_label.i:27: Warning:
No code nor implicit assigns clause for function main, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
diff --git a/src/plugins/wp/tests/wp_acsl/record.i b/src/plugins/wp/tests/wp_acsl/record.i
index 4c03f95460c051f06c90f48eb94485b005f3835a..e8d300665bb89069d74ae05d5dad97d069c74bfd 100644
--- a/src/plugins/wp/tests/wp_acsl/record.i
+++ b/src/plugins/wp/tests/wp_acsl/record.i
@@ -1,6 +1,9 @@
+/* run.config
+ STDOPT: +"-wp-no-extensional"
+*/
/* run.config_qualif
- OPT: -wp -wp-model Typed -wp-par 1 -wp-prop="-qed_ko,-ko"
- OPT: -wp -wp-model Typed -wp-par 1 -wp-prop="qed_ko,ko" -wp-steps 50
+ OPT: -wp -wp-model Typed -wp-par 1 -wp-prop="-qed_ko,-ko" -wp-no-extensional
+ OPT: -wp -wp-model Typed -wp-par 1 -wp-prop="qed_ko,ko" -wp-steps 50 -wp-no-extensional
*/
struct T {
diff --git a/src/plugins/wp/tests/wp_acsl/tset.i b/src/plugins/wp/tests/wp_acsl/tset.i
index 2a3c1a3247e9f3fae7bb176f441fe67189101c23..f55445cd7fade2d9cb14d57a585e303f49cfdd40 100644
--- a/src/plugins/wp/tests/wp_acsl/tset.i
+++ b/src/plugins/wp/tests/wp_acsl/tset.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -wp -wp-prover alt-ergo,coq -wp-script tests/wp_acsl/tset.s
+ OPT: -wp -wp-prover alt-ergo,coq -wp-coq-script tests/wp_acsl/tset.s
*/
/*@
diff --git a/src/plugins/wp/tests/wp_bts/bts_1174.i b/src/plugins/wp/tests/wp_bts/bts_1174.i
index d2f5c650c6bcec7748fa1815de6182e39eaf99de..fbc70fef492d18c3647cd8a9f19a7d0cd35bf985 100644
--- a/src/plugins/wp/tests/wp_bts/bts_1174.i
+++ b/src/plugins/wp/tests/wp_bts/bts_1174.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -wp -wp-prover coq -wp-script tests/wp_bts/bts_1174.s -wp-model +real
+ OPT: -wp -wp-prover coq -wp-coq-script tests/wp_bts/bts_1174.s -wp-model +real
*/
/*@ requires -10. <= x && x <= 10.; */
diff --git a/src/plugins/wp/tests/wp_plugin/abs.i b/src/plugins/wp/tests/wp_plugin/abs.i
index 9016a124ea0d3337c9fb76478743a55a1ed10939..90f22cd6ab3a82191d3b1d88719576040cf71b59 100644
--- a/src/plugins/wp/tests/wp_plugin/abs.i
+++ b/src/plugins/wp/tests/wp_plugin/abs.i
@@ -4,7 +4,7 @@
/* run.config_qualif
OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover alt-ergo
- OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover coq -wp-script tests/wp_plugin/abs.script
+ OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover coq -wp-coq-script tests/wp_plugin/abs.script
OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover why3:alt-ergo
*/
diff --git a/src/plugins/wp/tests/wp_plugin/inductive.c b/src/plugins/wp/tests/wp_plugin/inductive.c
index 3a7755c9cb32acd14da60e13e0a7400b0a0144a3..a76e7864fb1428e2541c713b5a3bb3ff6ddf5f9d 100644
--- a/src/plugins/wp/tests/wp_plugin/inductive.c
+++ b/src/plugins/wp/tests/wp_plugin/inductive.c
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-prover native:coq -wp-script tests/wp_plugin/inductive.script -wp-timeout 240
+ OPT: -wp-prover native:coq -wp-coq-script tests/wp_plugin/inductive.script -wp-timeout 240
*/
typedef struct _list { int element; struct _list* next; } list;
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/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
index 2ec7a4d714e37310f755188e40334fd2a84825db..beb2d13df622002818e1d3fd6020647182c3160f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/trig.res.oracle
@@ -7,7 +7,7 @@
Function foo
------------------------------------------------------------
-Goal Assertion 'qed_ok,S' (file tests/wp_plugin/trig.i, line 39):
+Goal Assertion 'qed_ok,S' (file tests/wp_plugin/trig.i, line 42):
Let x = c.F1_MSG_size.
Let a_1 = c.F1_MSG_text.
Assume {
@@ -23,7 +23,7 @@ Prove: x = 10.
------------------------------------------------------------
-Goal Assertion 'qed_ok,A' (file tests/wp_plugin/trig.i, line 40):
+Goal Assertion 'qed_ok,A' (file tests/wp_plugin/trig.i, line 43):
Let a_1 = (a.F1_MSG_text)[2].
Let a_2 = c.F1_MSG_text.
Let a_3 = a_2[2].
@@ -41,7 +41,7 @@ Prove: a_3 = a_1.
------------------------------------------------------------
-Goal Assertion 'qed_ok,B' (file tests/wp_plugin/trig.i, line 41):
+Goal Assertion 'qed_ok,B' (file tests/wp_plugin/trig.i, line 44):
Let a_1 = c.F1_MSG_text.
Let a_2 = a_1[2].
Let a_3 = (a.F1_MSG_text)[2].
@@ -63,7 +63,7 @@ Prove: a_5 = a_4.
------------------------------------------------------------
-Goal Instance of 'Pre-condition 'qed_ok' in 'fconcat'' in 'foo' at initialization of 'c' (file tests/wp_plugin/trig.i, line 38)
+Goal Instance of 'Pre-condition 'qed_ok' in 'fconcat'' in 'foo' at initialization of 'c' (file tests/wp_plugin/trig.i, line 41)
:
Prove: true.
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/tests/wp_plugin/trig.i b/src/plugins/wp/tests/wp_plugin/trig.i
index 3ed3496557fdf88a2dededd8f4bc3ec7b5f02f0f..c97b9d6a18614969df4d5f71a7e43a3e3c9392d6 100644
--- a/src/plugins/wp/tests/wp_plugin/trig.i
+++ b/src/plugins/wp/tests/wp_plugin/trig.i
@@ -1,5 +1,8 @@
+/* run.config
+ STDOPT: +"-wp-no-extensional"
+*/
/* run.config_qualif
- OPT: -wp -wp-par 1
+ OPT: -wp -wp-par 1 -wp-no-extensional
*/
typedef struct MSG {
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 3cffa42e8e040b4345bc60b32441b78000ce204a..6d48fd7458959b16b42f491c3d96de5430bcf2cd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
@@ -50,7 +50,7 @@ Prove: x2_0 = v.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 10) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 52)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 57)
:
Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
}
@@ -58,7 +58,7 @@ Prove: k <= 9.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 10) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 53)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 58)
:
Let m = p[k <- v].
Assume {
@@ -139,7 +139,7 @@ Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 21) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 65)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 70)
:
Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
}
@@ -147,7 +147,7 @@ Prove: k <= 9.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 21) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 66)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 71)
:
Let m = q[k <- v].
Assume {
@@ -228,7 +228,7 @@ Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 32) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 78)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 83)
:
Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
}
@@ -236,7 +236,7 @@ Prove: k <= 9.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 32) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 79)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 84)
:
Let m = q[k <- v].
Assume {
@@ -264,19 +264,19 @@ Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 13) in 'job' (1/3):
+Goal Assigns (file tests/wp_typed/user_collect.i, line 18) in 'job' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 13) in 'job' (2/3):
-Effect at line 17
+Goal Assigns (file tests/wp_typed/user_collect.i, line 18) in 'job' (2/3):
+Effect at line 22
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 13) in 'job' (3/3):
-Effect at line 17
+Goal Assigns (file tests/wp_typed/user_collect.i, line 18) in 'job' (3/3):
+Effect at line 22
Prove: true.
------------------------------------------------------------
@@ -294,19 +294,19 @@ Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 24) in 'job2' (1/3):
+Goal Assigns (file tests/wp_typed/user_collect.i, line 29) in 'job2' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 24) in 'job2' (2/3):
-Effect at line 28
+Goal Assigns (file tests/wp_typed/user_collect.i, line 29) in 'job2' (2/3):
+Effect at line 33
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 24) in 'job2' (3/3):
-Effect at line 28
+Goal Assigns (file tests/wp_typed/user_collect.i, line 29) in 'job2' (3/3):
+Effect at line 33
Prove: true.
------------------------------------------------------------
@@ -331,19 +331,19 @@ Prove: EqArray1_S1_S(10, m, q[k <- s]).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 35) in 'job3' (1/3):
+Goal Assigns (file tests/wp_typed/user_collect.i, line 40) in 'job3' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 35) in 'job3' (2/3):
-Effect at line 39
+Goal Assigns (file tests/wp_typed/user_collect.i, line 40) in 'job3' (2/3):
+Effect at line 44
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 35) in 'job3' (3/3):
-Effect at line 40
+Goal Assigns (file tests/wp_typed/user_collect.i, line 40) in 'job3' (3/3):
+Effect at line 45
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
index 96e426f2f4edc8d0e6362ad1ff416de949eb2784..b5584066b9c0b50d900d56a88a69db04ebd2d0cf 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
@@ -50,7 +50,7 @@ Prove: x2_0 = v.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 10) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 52)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 57)
:
Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
}
@@ -58,7 +58,7 @@ Prove: k <= 9.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 10) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 53)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file tests/wp_typed/user_collect.i, line 58)
:
Let m = p[k <- v].
Assume {
@@ -139,7 +139,7 @@ Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 21) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 65)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 70)
:
Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
}
@@ -147,7 +147,7 @@ Prove: k <= 9.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 21) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 66)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file tests/wp_typed/user_collect.i, line 71)
:
Let m = q[k <- v].
Assume {
@@ -228,7 +228,7 @@ Prove: EqArray1_S1_S(10, m_1, m_2[k <- s2_0]).
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 32) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 78)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 83)
:
Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
}
@@ -236,7 +236,7 @@ Prove: k <= 9.
------------------------------------------------------------
-Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 32) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 79)
+Goal Instance of 'Pre-condition (file tests/wp_typed/user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file tests/wp_typed/user_collect.i, line 84)
:
Let m = q[k <- v].
Assume {
@@ -264,19 +264,19 @@ Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 13) in 'job' (1/3):
+Goal Assigns (file tests/wp_typed/user_collect.i, line 18) in 'job' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 13) in 'job' (2/3):
-Effect at line 17
+Goal Assigns (file tests/wp_typed/user_collect.i, line 18) in 'job' (2/3):
+Effect at line 22
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 13) in 'job' (3/3):
-Effect at line 17
+Goal Assigns (file tests/wp_typed/user_collect.i, line 18) in 'job' (3/3):
+Effect at line 22
Prove: true.
------------------------------------------------------------
@@ -294,19 +294,19 @@ Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 24) in 'job2' (1/3):
+Goal Assigns (file tests/wp_typed/user_collect.i, line 29) in 'job2' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 24) in 'job2' (2/3):
-Effect at line 28
+Goal Assigns (file tests/wp_typed/user_collect.i, line 29) in 'job2' (2/3):
+Effect at line 33
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 24) in 'job2' (3/3):
-Effect at line 28
+Goal Assigns (file tests/wp_typed/user_collect.i, line 29) in 'job2' (3/3):
+Effect at line 33
Prove: true.
------------------------------------------------------------
@@ -331,19 +331,19 @@ Prove: EqArray1_S1_S(10, m, q[k <- s]).
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 35) in 'job3' (1/3):
+Goal Assigns (file tests/wp_typed/user_collect.i, line 40) in 'job3' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 35) in 'job3' (2/3):
-Effect at line 39
+Goal Assigns (file tests/wp_typed/user_collect.i, line 40) in 'job3' (2/3):
+Effect at line 44
Prove: true.
------------------------------------------------------------
-Goal Assigns (file tests/wp_typed/user_collect.i, line 35) in 'job3' (3/3):
-Effect at line 40
+Goal Assigns (file tests/wp_typed/user_collect.i, line 40) in 'job3' (3/3):
+Effect at line 45
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/user_collect.i b/src/plugins/wp/tests/wp_typed/user_collect.i
index 00a0248cc748181aa415ad4de217b83003f73139..1c445567ee939c2779e961943c8d32116fd9b67f 100644
--- a/src/plugins/wp/tests/wp_typed/user_collect.i
+++ b/src/plugins/wp/tests/wp_typed/user_collect.i
@@ -1,4 +1,9 @@
-
+/* run.config
+ STDOPT: +"-wp-no-extensional"
+*/
+/* run.config_qualif
+ STDOPT: +"-wp-no-extensional"
+*/
int k ;
int p[10] ;
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 7b6ba044a297053255417158844f6f6f361a1c78..e67a9bf835de191c32ab68bf7565556bd7b1d63b 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -200,6 +200,13 @@ module InHeap =
let help = "Consider variable names aliased."
end)
+let () = Parameter_customize.set_group wp_model
+module AliasInit =
+ False(struct
+ let option_name = "-wp-alias-init"
+ let help = "Use initializers for aliasing propagation."
+ end)
+
let () = Parameter_customize.set_group wp_model
module InCtxt =
String_set
@@ -216,13 +223,6 @@ module ExternArrays =
let help = "Put some default size for extern arrays."
end)
-let () = Parameter_customize.set_group wp_model
-module ExtEqual =
- False(struct
- let option_name = "-wp-extensional"
- let help = "Use extensional equality on compounds (hypotheses only)."
- end)
-
let () = Parameter_customize.set_group wp_model
module Overflows =
False(struct
@@ -254,17 +254,11 @@ let wp_strategy = add_group "Computation Strategies"
let () = Parameter_customize.set_group wp_strategy
module Init =
- False(struct
+ True(struct
let option_name = "-wp-init-const"
let help = "Use initializers for global const variables."
end)
-module InitAlias =
- False(struct
- let option_name = "-wp-init-alias"
- let help = "Use initializers for aliasing propagation."
- end)
-
let () = Parameter_customize.set_group wp_strategy
module CalleePreCond =
True(struct
@@ -372,11 +366,18 @@ module Reduce =
let help = "Reduce function equalities with precedence to constructors."
end)
+let () = Parameter_customize.set_group wp_simplifier
+module ExtEqual =
+ True(struct
+ let option_name = "-wp-extensional"
+ let help = "Use extensional equality on compounds (hypotheses only)."
+ end)
+
let () = Parameter_customize.set_group wp_simplifier
module Filter =
True(struct
let option_name = "-wp-filter"
- let help = "Use variable filtering."
+ let help = "Filter non-used variables and related hypotheses."
end)
let () = Parameter_customize.set_group wp_simplifier
@@ -462,7 +463,7 @@ module Provers = String_list
- 'tip' (failed scripts only)\n\
- 'alt-ergo' (default)\n\
- 'altgr-ergo' (gui)\n\
- - 'coq', 'coqide' (see also -wp-script)\n\
+ - 'coq', 'coqide' (see also -wp-coq-script)\n\
- 'why3:<dp>' or '<dp>' (why3 prover, see -wp-detect)\n\
- 'native:alt-ergo'\n\
- 'native:altgr-ergo'\n\
@@ -496,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
@@ -622,7 +614,7 @@ module BackTrack = Int
let () = Parameter_customize.set_group wp_prover_options
module Script =
String(struct
- let option_name = "-wp-script"
+ let option_name = "-wp-coq-script"
let arg_name = "f.script"
let default = ""
let help = "Set user's file for Coq proofs."
@@ -631,7 +623,7 @@ module Script =
let () = Parameter_customize.set_group wp_prover_options
module UpdateScript =
True(struct
- let option_name = "-wp-update-script"
+ let option_name = "-wp-update-coq-script"
let help = "If turned off, do not save or modify user's proofs."
end)
@@ -685,7 +677,7 @@ let () = Parameter_customize.set_group wp_prover_options
module CoqTactic =
String
(struct
- let option_name = "-wp-tactic"
+ let option_name = "-wp-coq-tactic"
let arg_name = "proof"
let default = "auto with zarith"
let help = "Default tactic for Coq"
@@ -695,7 +687,7 @@ let () = Parameter_customize.set_group wp_prover_options
module TryHints =
False
(struct
- let option_name = "-wp-tryhints"
+ let option_name = "-wp-coq-tryhints"
let help = "Try scripts from other goals (see also -wp-hints)"
end)
@@ -703,7 +695,7 @@ let () = Parameter_customize.set_group wp_prover_options
module Hints =
Int
(struct
- let option_name = "-wp-hints"
+ let option_name = "-wp-coq-hints"
let arg_name = "n"
let default = 3
let help = "Maximum number of proposed Coq scripts (default 3)"
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index aea2b9677bdad5258b5d9c23466f6aaedef7f267..8918d667abf36e6abdcfe1047302addcad2414f9 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -50,9 +50,9 @@ module Model : Parameter_sig.String_list
module ByValue : Parameter_sig.String_set
module ByRef : Parameter_sig.String_set
module InHeap : Parameter_sig.String_set
+module AliasInit: Parameter_sig.Bool
module InCtxt : Parameter_sig.String_set
module ExternArrays: Parameter_sig.Bool
-module ExtEqual : Parameter_sig.Bool
module Literals : Parameter_sig.Bool
module Volatile : Parameter_sig.Bool
(* module Overflows : Parameter_sig.Bool *)
@@ -63,7 +63,6 @@ module Volatile : Parameter_sig.Bool
(** {2 Computation Strategies} *)
module Init: Parameter_sig.Bool
-module InitAlias: Parameter_sig.Bool
module InitWithForall: Parameter_sig.Bool
module BoundForallUnfolding: Parameter_sig.Int
module RTE: Parameter_sig.Bool
@@ -78,6 +77,7 @@ module Prenex: Parameter_sig.Bool
module Bits: Parameter_sig.Bool
module Ground: Parameter_sig.Bool
module Reduce: Parameter_sig.Bool
+module ExtEqual : Parameter_sig.Bool
module UnfoldAssigns : Parameter_sig.Bool
module Split: Parameter_sig.Bool
module SplitDepth: Parameter_sig.Int
@@ -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