diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index da270ebd1d85c68271d689e33e8358c975191e5d..a6db6ea1b032bfaee6fa566c3abbde6f8fc9464c 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -358,8 +358,9 @@ let json_of_result (p : VCS.prover) (r : VCS.result) =
`Assoc (name :: verdict :: (time @ steps))
let prover_of_json js =
- try VCS.parse_prover (js >? "prover" |> Json.string)
- with Not_found -> None
+ match js >? "prover" |> Json.string with
+ | exception Not_found -> None
+ | pname -> VCS.prover_of_name ~fallback:true pname
let result_of_json js =
let verdict = try js >? "verdict" |> verdict_of_json with _ -> VCS.NoResult in
@@ -417,8 +418,7 @@ and alternative js =
| Some prover -> Prover(prover,result_of_json js)
| None ->
match tactic_of_json js with
- | Some(tactic, children) ->
- a_tactic tactic (List.map subscript children)
+ | Some(tactic, children) -> a_tactic tactic (List.map subscript children)
| None -> Error("Invalid Tactic",js)
let rec encode script = `List (alternatives script)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 25d32bef0af34c84dc592e7497b018483f7dfa28..265f0d4c0a84cd70f197942abcf20847c7260513 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -46,21 +46,12 @@ let parse_prover = function
| "why3" -> Some (Why3 { Why3.Whyconf.prover_name = "why3";
Why3.Whyconf.prover_version = "";
Why3.Whyconf.prover_altern = "generate only" })
- | s ->
- let prv = String.split_on_char ':' s in
- let prv = match prv with "why3"::prv -> prv | _ -> prv in
- let name = String.concat "," prv in
- match Why3Provers.find_fallback name with
- | Exact p -> Some (Why3 p)
- | Fallback p ->
- Wp_parameters.warning ~current:false ~once:true
- "Prover '%s' not found, fallback to '%s'"
- (String.concat ":" prv) (Why3Provers.ident_wp p) ;
- Some (Why3 p)
- | NotFound ->
+ | name ->
+ match Why3Provers.lookup name with
+ | Some p -> Some (Why3 p)
+ | None ->
Wp_parameters.error ~once:true
- "Prover '%s' not found in why3.conf" name ;
- None
+ "Prover '%s' not found in why3.conf" name ; None
let parse_mode m =
match String.lowercase_ascii m with
@@ -71,14 +62,21 @@ let parse_mode m =
| "fixup" -> FixUpdate
| _ ->
Wp_parameters.error ~once:true
- "Unrecognized mode %S (use 'batch' instead)" m ;
- Batch
+ "Unrecognized mode %S (use 'batch' instead)" m ; Batch
let name_of_prover = function
| Why3 s -> Why3Provers.ident_wp s
| Qed -> "qed"
| Tactical -> "script"
+let prover_of_name ?fallback = function
+ | "qed" -> Some Qed
+ | "script" -> Some Tactical
+ | name ->
+ match Why3Provers.lookup ?fallback name with
+ | None -> None
+ | Some prv -> Some (Why3 prv)
+
let title_of_prover ?version = function
| Why3 s ->
let version = match version with Some v -> v | None ->
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 6f9c67f88d0212c265054b454f727b3e9ff73334..4a737a298f346a5df5b91209b8c90801770ed9c1 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -50,8 +50,13 @@ val filename_for_prover : prover -> string
val title_of_mode : mode -> string
val parse_mode : string -> mode
+
+(** For the command line *)
val parse_prover : string -> prover option
+(** For scripts *)
+val prover_of_name : ?fallback:bool -> string -> prover option
+
val pp_prover : Format.formatter -> prover -> unit
val pp_mode : Format.formatter -> mode -> unit
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 04d4e4e5a0ac2160571b17966b3ec2863f55a71a..204a593d6d3948bc2dcc7e24d08df3c5194f0bd4 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -62,40 +62,6 @@ let configure =
type t = Why3.Whyconf.prover
-(* In an ambiguous map of provers, tries to find the basic alternative, if none
- is found, just give an arbitrary one. *)
-let resolve_ambiguity provers =
- let open Why3.Whyconf in
- let provers = fst @@ List.split @@ Mprover.bindings provers in
- try List.find (fun p -> p.prover_altern = "") provers
- with Not_found -> List.hd provers
-
-let find_opt s =
- let open Why3.Whyconf in
- try
- let config = Lazy.force cfg in
- let filter = parse_filter_prover s in
- Some ((filter_one_prover config filter).prover)
- with
- | ParseFilterProver _ -> None
- | ProverNotFound _ -> None
- | ProverAmbiguity (_, _, provers) -> Some (resolve_ambiguity provers)
-
-type fallback = Exact of t | Fallback of t | NotFound
-
-let find_fallback name =
- match find_opt name with
- | Some prv -> Exact prv
- | None ->
- match String.split_on_char ',' name with
- | shortname :: _ :: _ ->
- begin
- match find_opt shortname with
- | Some prv -> Fallback prv
- | None -> NotFound
- end
- | _ -> NotFound
-
let ident_why3 = Why3.Whyconf.prover_parseable_format
let ident_wp s =
let name = Why3.Whyconf.prover_parseable_format s in
@@ -133,19 +99,65 @@ let provers_set () : Why3.Whyconf.Sprover.t =
let is_available p =
Why3.Whyconf.Mprover.mem p (Why3.Whyconf.get_provers (config ()))
-let has_shortcut p s =
- match Why3.Wstdlib.Mstr.find_opt s
- (Why3.Whyconf.get_prover_shortcuts (config ())) with
- | None -> false
- | Some p' -> Why3.Whyconf.Prover.equal p p'
-
let with_counter_examples p =
if has_counter_examples p then Some p else
let name = p.prover_name in
+ let version = p.prover_version in
List.find_opt
- (fun (q : t) -> q.prover_name = name && has_counter_examples q)
+ (fun (q : t) ->
+ q.prover_name = name &&
+ q.prover_version = version &&
+ has_counter_examples q)
@@ provers ()
+(* -------------------------------------------------------------------------- *)
+(* --- Prover Lookup --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* semantical version comparison *)
+
+type sem = V of int | S of string
+let sem s = try V (int_of_string s) with Failure _ -> S s
+let cmp x y =
+ match x,y with
+ | V a,V b -> b - a
+ | V _,S _ -> (-1)
+ | S _,V _ -> (+1)
+ | S a,S b -> String.compare a b
+let scmp u v = cmp (sem u) (sem v)
+let vcmp u v =
+ List.compare scmp (String.split_on_char '.' u) (String.split_on_char '.' v)
+let by_version (p:t) (q:t) = vcmp p.prover_version q.prover_version
+
+let filter ~name ?version (p:t) =
+ p.prover_altern = "" &&
+ String.lowercase_ascii p.prover_name = name &&
+ match version with None -> true | Some v -> p.prover_version = v
+
+let select ~name ?version () =
+ match
+ List.sort by_version @@ List.filter (filter ~name ?version) @@ provers ()
+ with p::_ -> Some p | [] -> None
+
+let lookup ?(fallback=false) prover_name =
+ match String.split_on_char ':' @@ String.lowercase_ascii prover_name with
+ | [name] -> select ~name ()
+ | [name;version] ->
+ begin
+ match select ~name ~version () with
+ | Some _ as res -> res
+ | None ->
+ if fallback then
+ match select ~name () with
+ | None -> None
+ | Some p as res ->
+ Wp_parameters.warning ~once:true ~current:false
+ "Prover %s not found, fallback to %s" prover_name (ident_wp p) ;
+ res
+ else None
+ end
+ | _ -> None
+
(* -------------------------------------------------------------------------- *)
(* --- Models --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 0142173be48e4b1e529858398f9aebcd2c679bbf..58fa30bd2871a6b2ca442c53a3fc5f203bae3e34 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -27,11 +27,6 @@ val set_procs : int -> unit
type t = Why3.Whyconf.prover
-val find_opt : string -> t option
-
-type fallback = Exact of t | Fallback of t | NotFound
-val find_fallback : string -> fallback
-
val ident_why3 : t -> string
val ident_wp : t -> string
val title : ?version:bool -> t -> string
@@ -40,6 +35,7 @@ val version : t -> string
val altern : t -> string
val compare : t -> t -> int
+val lookup : ?fallback:bool -> string -> t option
val provers : unit -> t list
val provers_set : unit -> Why3.Whyconf.Sprover.t
val is_auto : t -> bool
@@ -47,8 +43,6 @@ val is_available : t -> bool
val is_mainstream : t -> bool
val has_counter_examples : t -> bool
val with_counter_examples : t -> t option
-val has_shortcut : t -> string -> bool
-
type model = Why3.Model_parser.concrete_syntax_term
val pp_model : model Pretty_utils.formatter
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 173961c6dc021ba721b4ef6fb1b08714307e6545..75d6ddea26e308eabf60cc12378b24bec829cc7f 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1450,8 +1450,11 @@ Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use
Finally, since \textsf{Why-3} also provides the alias
\verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.
-If you require a specific version of a prover which is not installed,
-\textsf{WP} will fallback to the default version available to \textsf{Why-3} for this prover, if any.
+If you require on command line a specific version of a prover which is not
+installed, \textsf{WP} will emit an error. When a script contains a couple
+prover/version that is not installed, \textsf{WP} will try to find another
+version of the same prover and fallback on this solver (emitting a warning) if
+it finds one. In this case, one should update the scripts.
Notice that \textsf{Why-3} provers benefit from a cache management when used in combination
with a \textsf{WP}-session, see Section~\ref{wp-cache} for more details.
diff --git a/src/plugins/wp/gui/GuiConfig.ml b/src/plugins/wp/gui/GuiConfig.ml
index f40609610d935c291e8d1bfe4e24c46efb05d3d7..061068f4178a401bad8193f5d0a95f72f0529640 100644
--- a/src/plugins/wp/gui/GuiConfig.ml
+++ b/src/plugins/wp/gui/GuiConfig.ml
@@ -41,7 +41,7 @@ class provers =
in
let selection = List.fold_left
(fun acc e ->
- match Why3Provers.find_opt e with
+ match Why3Provers.lookup e with
| None -> acc
| Some p -> S.add p acc)
S.empty cmdline
diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
index 7681d66416b9cac73165739e2e916f5c8fcae817..3eced44d70b6ff13872e3284d59f5a69e1da68a3 100644
--- a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
+++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
@@ -2,7 +2,7 @@
OPT: -wp-gen -wp-rte -wp-prover why3 -wp-msg-key print-generated
*/
/* run.config_qualif
- OPT: -wp-rte -wp-prover Alt-Ergo
+ OPT: -wp-rte
*/
/*@
diff --git a/src/plugins/wp/tests/wp_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c
index ec858e5eedb8e057984b7bb96daf5d71d4783bc5..56142759693b5013a45982e82608bcc0059e3d66 100644
--- a/src/plugins/wp/tests/wp_acsl/classify_float.c
+++ b/src/plugins/wp/tests/wp_acsl/classify_float.c
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -wp-prover Alt-Ergo
+ OPT:
OPT: -wp-model real
*/
diff --git a/src/plugins/wp/tests/wp_acsl/div_mod.i b/src/plugins/wp/tests/wp_acsl/div_mod.i
index 10cf92b70f4e4c07d3c0015633b4f0db3ed68760..8fd5fb4e5cba3d521329a917cca3a5aebe361d0e 100644
--- a/src/plugins/wp/tests/wp_acsl/div_mod.i
+++ b/src/plugins/wp/tests/wp_acsl/div_mod.i
@@ -3,8 +3,6 @@
*/
/* run.config_qualif
OPT: -wp-prop="-ko"
- OPT: -wp-prover why3:Alt-Ergo -wp-prop="-ko"
- OPT: -wp-prover "Alt-Ergo" -wp-prop="ko" -wp-steps 50
*/
//@ axiomatic Eq { predicate Peq(integer x,integer y) = x == y ; }
diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i b/src/plugins/wp/tests/wp_acsl/float_compare.i
index ff33d352a8f43a5d40ec834fd0de0e04d27f4f88..3e5efe0a21c480dfdc4b9b1e28a5fea022b32516 100644
--- a/src/plugins/wp/tests/wp_acsl/float_compare.i
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -wp-prover why3:Alt-Ergo
+ OPT:
OPT: -wp-model real
*/
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
deleted file mode 100644
index d56892bed73e2320f69ba98f7d23a947f7420d22..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
+++ /dev/null
@@ -1,13 +0,0 @@
-# frama-c -wp -wp-model 'Typed (Real)' [...]
-[kernel] Parsing classify_float.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] 3 goals scheduled
-[wp] [Qed] Goal typed_real_lemma_InfN_not_finite : Valid
-[wp] [Qed] Goal typed_real_lemma_InfP_not_finite : Valid
-[wp] [Qed] Goal typed_real_lemma_NaN_not_finite : Valid
-[wp] Proved goals: 3 / 3
- Qed: 3
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Lemma 3 - 3 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
deleted file mode 100644
index b02c8f809bee5d45a5106eb0c70ded9bbd50d026..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+++ /dev/null
@@ -1,38 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing div_mod.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
-[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
-[wp] Warning: Missing RTE guards
-[wp] 22 goals scheduled
-[wp] [Valid] typed_f_ensures_d0_div_pos_pos (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_d1_div_neg_pos (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_d2_div_pos_neg (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_d3_div_neg_neg (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_d4_div_x_1 (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_d5_div_x_minus1 (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_d6_div_0_x (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_sd0_div_pos_pos (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_sd1_div_neg_pos (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_f_ensures_sd2_div_pos_neg (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_f_ensures_sd3_div_neg_neg (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_m0_mod_pos_pos (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_m1_mod_neg_pos (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_m2_mod_pos_neg (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_m3_mod_neg_neg (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_m4_mod_x_1 (Alt-Ergo) (Trivial)
-[wp] [Valid] typed_f_ensures_m5_mod_x_minus1 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_m6_mod_0_x (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_sm0_mod_pos_pos (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_sm1_mod_neg_pos (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_sm2_mod_pos_neg (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_sm3_mod_neg_neg (Alt-Ergo) (Cached)
-[wp] Proved goals: 22 / 24
- Terminating: 1
- Unreachable: 1
- Alt-Ergo: 20
- Unsuccess: 2
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f - 20 22 90.9%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
deleted file mode 100644
index ed6ef43b129e8d6b00acd9a47a4e667a91b9a83f..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
+++ /dev/null
@@ -1,13 +0,0 @@
-# frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing div_mod.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
-[wp] [Unsuccess] typed_f_ensures_d7_div_0_x_ko (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_f_ensures_m7_mod_0_x_ko (Alt-Ergo) (Cached)
-[wp] Proved goals: 0 / 2
- Unsuccess: 2
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f - - 2 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.res.oracle
similarity index 100%
rename from src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
rename to src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/tset.i b/src/plugins/wp/tests/wp_acsl/tset.i
index 9a2cbce1d8bce0e0f39ced6ab7fd000625739529..c7304aa8fb23304a18ba780b3c85531599794e5d 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
+ OPT: -wp
*/
/*@
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
index 64a63d80a8da9a8de7785aca320496251a1056e9..91c3d02472db8fd44f4e46b013492a7af1a0c9ac 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
@@ -6,8 +6,6 @@
OPT: -wp-rte -wp-prover=Alt-Ergo,script -wp-prop=-lack @USING_WP_SESSION@
*/
-// The use '-wp-prover=z3,why3:Alt-Ergo' or using Alt-Ergo 2.3.0 gives better results.
-
typedef unsigned uint32_t ;
typedef unsigned long long uint64_t ;
diff --git a/src/plugins/wp/tests/wp_plugin/abs.i b/src/plugins/wp/tests/wp_plugin/abs.i
index 160340d39d99ba6c47be191e778ba27506b29efc..8e6b8f3a033d932933eefcc0f2d7d158c983b9db 100644
--- a/src/plugins/wp/tests/wp_plugin/abs.i
+++ b/src/plugins/wp/tests/wp_plugin/abs.i
@@ -6,7 +6,7 @@
/* run.config_qualif
COMMENT: depends from files mentionned into "abs.driver"
DEPS: @PTEST_DEPS@ abs.why
- OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver} -wp-prover Alt-Ergo
+ OPT: -wp -wp-driver %{dep:@PTEST_DIR@/abs.driver}
*/
/*@ axiomatic Absolute { logic integer ABS(integer x) ; } */
diff --git a/src/plugins/wp/tests/wp_plugin/bit_test.c b/src/plugins/wp/tests/wp_plugin/bit_test.c
index 03c9e001851f354430dd177e746aa66c6a16c019..8596c3bea92c55ad2e4788fe68ad217835f0ad73 100644
--- a/src/plugins/wp/tests/wp_plugin/bit_test.c
+++ b/src/plugins/wp/tests/wp_plugin/bit_test.c
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-driver %{dep:@PTEST_DIR@/bit_test.driver} -wp-prover why3:Alt-Ergo
+ OPT: -wp-driver %{dep:@PTEST_DIR@/bit_test.driver}
*/
/*@
diff --git a/src/plugins/wp/tests/wp_plugin/dune b/src/plugins/wp/tests/wp_plugin/dune
index 7323baff07fc5124c2e55b6e9e808096efbd1bdf..77a700def17a207f5ee1d2efb640bad964f9b4b8 100644
--- a/src/plugins/wp/tests/wp_plugin/dune
+++ b/src/plugins/wp/tests/wp_plugin/dune
@@ -2,6 +2,10 @@
result_qualif/bitmask0x8000.0.session_qualif/script
(copy_files ../../../bitmask0x8000.0.session_qualif/script/*))
+(subdir
+ result_qualif/fallback.0.session_qualif/script
+ (copy_files ../../../fallback.0.session_qualif/script/*))
+
(subdir
result_qualif/unroll.0.session_qualif/script
(copy_files ../../../unroll.0.session_qualif/script/*))
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..2f92c64659efb2b81d45b139a3336994508cb838
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
@@ -0,0 +1 @@
+[ { "prover": "Alt-Ergo:1.2.0", "verdict": "valid", "time": 0.1 } ]
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
index 2290dc57bd436e0896d471e7aab94c339561907c..b4ec19b80dfbeaff50d1d8ffd6fa17db2d7dfe8e 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.i
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -1,6 +1,9 @@
/* run.config_qualif
- OPT: -wp-prover=Alt-Ergo:1.2.0
+ DEPS: @PTEST_DEPS@ @WP_SESSION@/script/job_ensures.json
+ OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
*/
/*@ ensures \result == a * b ; */
-int job(int a,int b) { return (a - 1)*b + b ; }
+int job(int a,int b){
+ return (a - 1) * b + b ;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/float_format.i b/src/plugins/wp/tests/wp_plugin/float_format.i
index 4a7f3dac8e9f1c1937f4dc54819c661abfa60648..0686e1ef489d58cdbf1f0ba92b2d9bedae051bdc 100644
--- a/src/plugins/wp/tests/wp_plugin/float_format.i
+++ b/src/plugins/wp/tests/wp_plugin/float_format.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- OPT: -wp-prover Alt-Ergo -wp-steps 5 -wp-timeout 100
+ OPT: -wp-steps 5 -wp-timeout 100
*/
//@ ensures KO: \result == 0.2 + x ;
diff --git a/src/plugins/wp/tests/wp_plugin/math.i b/src/plugins/wp/tests/wp_plugin/math.i
index 891798bc63247a25ca7898532347c5898cbcdac0..bf12316c003d15744ff5c53d42937f55e9713a9b 100644
--- a/src/plugins/wp/tests/wp_plugin/math.i
+++ b/src/plugins/wp/tests/wp_plugin/math.i
@@ -3,8 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-prover Alt-Ergo -wp-prop=-ko
- OPT: -wp-prover Alt-Ergo -wp-prop=ko -wp-steps 10
+ OPT: -wp-prop=-ko
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
index eb72aff708d33044859e5b7cd8f437377d001395..5c5012bb8debf2df198b9b5611d6bc78b74dec67 100644
--- a/src/plugins/wp/tests/wp_plugin/nosession.i
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -4,7 +4,7 @@
/* run.config_qualif
CMD: @frama-c@ -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
PLUGIN: wp,rtegen
- OPT: -wp -wp-prover Alt-Ergo -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
+ OPT: -wp -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
COMMENT: The session directory shall not be created
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
index 02f6170d68aa77e687421e86faa1a6da7ccafae8..c31f09c80a4d0d475ee977e838297611a64b92b9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
@@ -8,7 +8,7 @@
Function job
------------------------------------------------------------
-Goal Post-condition (file fallback.i, line 5) in 'job':
+Goal Post-condition (file fallback.i, line 6) in 'job':
Let x = b + (b * (a - 1)).
Assume { Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(x). }
Prove: (a * b) = x.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index 97cac7711880c5fafc774c13a75819dc053c50b0..6a4ce52b61af3d5549331f5d148b5d2c53687aa8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -1,10 +1,10 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+# frama-c -wp [...]
[kernel] Parsing sequence.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] sequence.i:23: Warning:
+[kernel:annot:missing-spec] sequence.i:13: Warning:
Neither code nor explicit exits and terminates for function f,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] sequence.i:29: Warning:
+[kernel:annot:missing-spec] sequence.i:19: Warning:
Neither code nor explicit exits and terminates for function g,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
@@ -56,27 +56,27 @@ Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'ok,id_max' (file sequence.i, line 97):
+Goal Preservation of Invariant 'ok,id_max' (file sequence.i, line 87):
Prove: true.
------------------------------------------------------------
-Goal Establishment of Invariant 'ok,id_max' (file sequence.i, line 97):
+Goal Establishment of Invariant 'ok,id_max' (file sequence.i, line 87):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'ok,id_min' (file sequence.i, line 96):
+Goal Preservation of Invariant 'ok,id_min' (file sequence.i, line 86):
Prove: true.
------------------------------------------------------------
-Goal Establishment of Invariant 'ok,id_min' (file sequence.i, line 96):
+Goal Establishment of Invariant 'ok,id_min' (file sequence.i, line 86):
Prove: true.
------------------------------------------------------------
-Goal Preservation of Invariant 'ok,inv' (file sequence.i, line 98):
+Goal Preservation of Invariant 'ok,inv' (file sequence.i, line 88):
Let a = ([ y ] *^ i).
Let x_1 = 1 + i.
Assume {
@@ -107,56 +107,56 @@ Prove: ([ y ] *^ x_1) = a ^ [ y ].
------------------------------------------------------------
-Goal Establishment of Invariant 'ok,inv' (file sequence.i, line 98):
+Goal Establishment of Invariant 'ok,inv' (file sequence.i, line 88):
Prove: true.
------------------------------------------------------------
-Goal Loop assigns (file sequence.i, line 95):
+Goal Loop assigns (file sequence.i, line 85):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 79) in 'loops' (1/3):
+Goal Assigns (file sequence.i, line 69) in 'loops' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 79) in 'loops' (2/3):
-Effect at line 101
+Goal Assigns (file sequence.i, line 69) in 'loops' (2/3):
+Effect at line 91
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 79) in 'loops' (3/3):
-Effect at line 101
+Goal Assigns (file sequence.i, line 69) in 'loops' (3/3):
+Effect at line 91
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 79) in 'loops' (1/3):
+Goal Assigns (file sequence.i, line 69) in 'loops' (1/3):
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 79) in 'loops' (2/3):
-Effect at line 101
+Goal Assigns (file sequence.i, line 69) in 'loops' (2/3):
+Effect at line 91
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 79) in 'loops' (3/3):
-Effect at line 101
+Goal Assigns (file sequence.i, line 69) in 'loops' (3/3):
+Effect at line 91
Prove: true.
------------------------------------------------------------
-Goal Decreasing of Loop variant at loop (file sequence.i, line 101):
+Goal Decreasing of Loop variant at loop (file sequence.i, line 91):
Prove: true.
------------------------------------------------------------
-Goal Positivity of Loop variant at loop (file sequence.i, line 101):
+Goal Positivity of Loop variant at loop (file sequence.i, line 91):
Prove: true.
------------------------------------------------------------
@@ -315,7 +315,7 @@ Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 35) in 'no_calls':
+Goal Assigns (file sequence.i, line 25) in 'no_calls':
Prove: true.
------------------------------------------------------------
@@ -333,12 +333,12 @@ Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 54) in 'sequence':
+Goal Assigns (file sequence.i, line 44) in 'sequence':
Prove: true.
------------------------------------------------------------
-Goal Assigns (file sequence.i, line 54) in 'sequence':
+Goal Assigns (file sequence.i, line 44) in 'sequence':
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index af751c1e16ffa4e5864cde7fb9c8d4e1a5b315b5..6c923007a1824b9a86158c4527d8a020be54e708 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -4,13 +4,15 @@
[wp] [Valid] Goal job_exits (Cfg) (Unreachable)
[wp] [Valid] Goal job_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
-[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.5.3'
[wp] 1 goal scheduled
+[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
[wp] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 3 / 3
Terminating: 1
Unreachable: 1
Alt-Ergo: 1
+[wp] Session can be updated
+ - 1 script unused (now automated)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - 1 1 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
deleted file mode 100644
index b8ae6b5a64a81003f6090701536070c3a73904c4..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ /dev/null
@@ -1,22 +0,0 @@
-# frama-c -wp -wp-steps 10 [...]
-[kernel] Parsing math.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] [Valid] Goal ko_exits (Cfg) (Unreachable)
-[wp] Warning: Missing RTE guards
-[wp] 9 goals scheduled
-[wp] [Unsuccess] typed_ko_ensures_ko_sin_asin (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_cos_acos (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_asin_sin (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_acos_cos (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_atan_tan (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_log_pow (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_exp_log (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_exp_log_add_mul (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_ko_ensures_ko_sqrt_pos (Alt-Ergo) (Cached)
-[wp] Proved goals: 1 / 10
- Unreachable: 1
- Unsuccess: 9
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- ko - - 9 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.res.oracle
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/math.0.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/math.res.oracle
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
deleted file mode 100644
index 31de6fd9f893e0a04b7536a092959c1d5672842c..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ /dev/null
@@ -1,69 +0,0 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing sequence.i (no preprocessing)
-[wp] Running WP plugin...
-[kernel:annot:missing-spec] sequence.i:23: Warning:
- Neither code nor explicit exits and terminates for function f,
- generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] sequence.i:29: Warning:
- Neither code nor explicit exits and terminates for function g,
- generating default clauses. See -generated-spec-* options for more info
-[wp] Warning: Missing RTE guards
-[wp] [Valid] Goal no_calls_exits (Cfg) (Unreachable)
-[wp] [Valid] Goal no_calls_terminates (Cfg) (Trivial)
-[wp] 45 goals scheduled
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_m1 (Qed)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_m2 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_bug_why3_n1 (Qed)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_n2 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_n3 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_bug_why3_n5 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_bug_why3_n6 (Qed)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_bug_why3_n5_ok (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_bug_why3_n6_ok (Qed)
-[wp] [Valid] typed_caveat_no_calls_assigns (Qed)
-[wp] [Valid] typed_caveat_sequence_terminates (Qed)
-[wp] [Valid] typed_caveat_sequence_exits (Qed)
-[wp] [Valid] typed_caveat_sequence_assigns_exit (Qed)
-[wp] [Valid] typed_caveat_sequence_assigns_normal (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_o1 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_p1 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_p2 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_p3 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_o2 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_q1 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_q2 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_q3 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_terminates (Qed)
-[wp] [Valid] typed_caveat_loops_ensures_ok_first (Qed)
-[wp] [Valid] typed_caveat_loops_ensures_ok_last (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_exits (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_max_preserved (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_max_established (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_min_preserved (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_min_established (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_inv_preserved (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_inv_established (Qed)
-[wp] [Valid] typed_caveat_loops_loop_assigns (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_exit_part1 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_exit_part2 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_exit_part3 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_normal_part1 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_normal_part2 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_normal_part3 (Qed)
-[wp] [Valid] typed_caveat_loops_loop_variant_decrease (Qed)
-[wp] [Valid] typed_caveat_loops_loop_variant_positive (Qed)
-[wp] [Valid] typed_caveat_loops_g_called_ensures_ok_u1 (Qed)
-[wp] [Valid] typed_caveat_loops_g_called_ensures_ok_u2 (Qed)
-[wp] [Valid] typed_caveat_loops_g_not_called_ensures_ok_v1 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_g_not_called_ensures_ok_v2 (Alt-Ergo) (Cached)
-[wp] Proved goals: 47 / 47
- Terminating: 1
- Unreachable: 1
- Qed: 34
- Alt-Ergo: 11
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- no_calls 5 5 10 100%
- sequence 10 2 12 100%
- loops 19 4 23 100%
-------------------------------------------------------------
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
deleted file mode 100644
index ac58a64fe0ff180f0e4b0b7d44cfb4184d57411a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ /dev/null
@@ -1,64 +0,0 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' [...]
-[kernel] Parsing sequence.i (no preprocessing)
-[wp] Running WP plugin...
-[kernel:annot:missing-spec] sequence.i:23: Warning:
- Neither code nor explicit exits and terminates for function f,
- generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] sequence.i:29: Warning:
- Neither code nor explicit exits and terminates for function g,
- generating default clauses. See -generated-spec-* options for more info
-[wp] Warning: Missing RTE guards
-[wp] [Valid] Goal no_calls_exits (Cfg) (Unreachable)
-[wp] [Valid] Goal no_calls_terminates (Cfg) (Trivial)
-[wp] 40 goals scheduled
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_m1 (Qed)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_m2 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_n2 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_ensures_ok_n3 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_no_calls_assigns (Qed)
-[wp] [Valid] typed_caveat_sequence_terminates (Qed)
-[wp] [Valid] typed_caveat_sequence_exits (Qed)
-[wp] [Valid] typed_caveat_sequence_assigns_exit (Qed)
-[wp] [Valid] typed_caveat_sequence_assigns_normal (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_o1 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_p1 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_p2 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_called_ensures_ok_p3 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_o2 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_q1 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_q2 (Qed)
-[wp] [Valid] typed_caveat_sequence_g_not_called_ensures_ok_q3 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_terminates (Qed)
-[wp] [Valid] typed_caveat_loops_ensures_ok_first (Qed)
-[wp] [Valid] typed_caveat_loops_ensures_ok_last (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_exits (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_max_preserved (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_max_established (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_min_preserved (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_id_min_established (Qed)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_inv_preserved (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_loop_invariant_ok_inv_established (Qed)
-[wp] [Valid] typed_caveat_loops_loop_assigns (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_exit_part1 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_exit_part2 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_exit_part3 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_normal_part1 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_normal_part2 (Qed)
-[wp] [Valid] typed_caveat_loops_assigns_normal_part3 (Qed)
-[wp] [Valid] typed_caveat_loops_loop_variant_decrease (Qed)
-[wp] [Valid] typed_caveat_loops_loop_variant_positive (Qed)
-[wp] [Valid] typed_caveat_loops_g_called_ensures_ok_u1 (Qed)
-[wp] [Valid] typed_caveat_loops_g_called_ensures_ok_u2 (Qed)
-[wp] [Valid] typed_caveat_loops_g_not_called_ensures_ok_v1 (Alt-Ergo) (Cached)
-[wp] [Valid] typed_caveat_loops_g_not_called_ensures_ok_v2 (Alt-Ergo) (Cached)
-[wp] Proved goals: 42 / 42
- Terminating: 1
- Unreachable: 1
- Qed: 31
- Alt-Ergo: 9
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- no_calls 2 3 5 100%
- sequence 10 2 12 100%
- loops 19 4 23 100%
-------------------------------------------------------------
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
deleted file mode 100644
index 6a23c1a83b41693e26942bdfb8ea7e4eb24f6353..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
+++ /dev/null
@@ -1,6 +0,0 @@
-# frama-c -wp -wp-model 'Typed (Caveat)' -wp-steps 50 [...]
-[kernel] Parsing sequence.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] Warning: No goal generated
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..15634da6162d98b33d7493c981c44dff5afab582
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.res.oracle
@@ -0,0 +1,69 @@
+# frama-c -wp [...]
+[kernel] Parsing sequence.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] sequence.i:13: Warning:
+ Neither code nor explicit exits and terminates for function f,
+ generating default clauses. See -generated-spec-* options for more info
+[kernel:annot:missing-spec] sequence.i:19: Warning:
+ Neither code nor explicit exits and terminates for function g,
+ generating default clauses. See -generated-spec-* options for more info
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal no_calls_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal no_calls_terminates (Cfg) (Trivial)
+[wp] 45 goals scheduled
+[wp] [Valid] typed_no_calls_ensures_ok_m1 (Qed)
+[wp] [Valid] typed_no_calls_ensures_ok_m2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_no_calls_ensures_ok_bug_why3_n1 (Qed)
+[wp] [Valid] typed_no_calls_ensures_ok_n2 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_no_calls_ensures_ok_n3 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_no_calls_ensures_ok_bug_why3_n5 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_no_calls_ensures_ok_bug_why3_n6 (Qed)
+[wp] [Valid] typed_no_calls_ensures_ok_bug_why3_n5_ok (Alt-Ergo) (Cached)
+[wp] [Valid] typed_no_calls_ensures_ok_bug_why3_n6_ok (Qed)
+[wp] [Valid] typed_no_calls_assigns (Qed)
+[wp] [Valid] typed_sequence_terminates (Qed)
+[wp] [Valid] typed_sequence_exits (Qed)
+[wp] [Valid] typed_sequence_assigns_exit (Qed)
+[wp] [Valid] typed_sequence_assigns_normal (Qed)
+[wp] [Valid] typed_sequence_g_called_ensures_ok_o1 (Qed)
+[wp] [Valid] typed_sequence_g_called_ensures_ok_p1 (Qed)
+[wp] [Valid] typed_sequence_g_called_ensures_ok_p2 (Qed)
+[wp] [Valid] typed_sequence_g_called_ensures_ok_p3 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_sequence_g_not_called_ensures_ok_o2 (Qed)
+[wp] [Valid] typed_sequence_g_not_called_ensures_ok_q1 (Qed)
+[wp] [Valid] typed_sequence_g_not_called_ensures_ok_q2 (Qed)
+[wp] [Valid] typed_sequence_g_not_called_ensures_ok_q3 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_loops_terminates (Qed)
+[wp] [Valid] typed_loops_ensures_ok_first (Qed)
+[wp] [Valid] typed_loops_ensures_ok_last (Alt-Ergo) (Cached)
+[wp] [Valid] typed_loops_exits (Qed)
+[wp] [Valid] typed_loops_loop_invariant_ok_id_max_preserved (Qed)
+[wp] [Valid] typed_loops_loop_invariant_ok_id_max_established (Qed)
+[wp] [Valid] typed_loops_loop_invariant_ok_id_min_preserved (Qed)
+[wp] [Valid] typed_loops_loop_invariant_ok_id_min_established (Qed)
+[wp] [Valid] typed_loops_loop_invariant_ok_inv_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_loops_loop_invariant_ok_inv_established (Qed)
+[wp] [Valid] typed_loops_loop_assigns (Qed)
+[wp] [Valid] typed_loops_assigns_exit_part1 (Qed)
+[wp] [Valid] typed_loops_assigns_exit_part2 (Qed)
+[wp] [Valid] typed_loops_assigns_exit_part3 (Qed)
+[wp] [Valid] typed_loops_assigns_normal_part1 (Qed)
+[wp] [Valid] typed_loops_assigns_normal_part2 (Qed)
+[wp] [Valid] typed_loops_assigns_normal_part3 (Qed)
+[wp] [Valid] typed_loops_loop_variant_decrease (Qed)
+[wp] [Valid] typed_loops_loop_variant_positive (Qed)
+[wp] [Valid] typed_loops_g_called_ensures_ok_u1 (Qed)
+[wp] [Valid] typed_loops_g_called_ensures_ok_u2 (Qed)
+[wp] [Valid] typed_loops_g_not_called_ensures_ok_v1 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_loops_g_not_called_ensures_ok_v2 (Alt-Ergo) (Cached)
+[wp] Proved goals: 47 / 47
+ Terminating: 1
+ Unreachable: 1
+ Qed: 34
+ Alt-Ergo: 11
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ no_calls 5 5 10 100%
+ sequence 10 2 12 100%
+ loops 19 4 23 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/sequence.i b/src/plugins/wp/tests/wp_plugin/sequence.i
index 6d79c4df6a6e9dcc7885ccba230d53bfbcb76f6f..f69ebca60684ee9fbf930f29892f4ada60935e80 100644
--- a/src/plugins/wp/tests/wp_plugin/sequence.i
+++ b/src/plugins/wp/tests/wp_plugin/sequence.i
@@ -1,13 +1,3 @@
-/* run.config
- OPT: -wp-model Caveat
- */
-
-/* run.config_qualif
- 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;
/*@ axiomatic Call {
@ logic \list<integer> call_obs{L} reads call_seq ;