From 2e6894fc54a024702ef9f9a80184f57e0a098f9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 10 Apr 2024 00:14:23 +0200
Subject: [PATCH] [wp] refactor prover selection and cleanup tests
---
src/plugins/wp/VCS.ml | 20 ++---
src/plugins/wp/Why3Provers.ml | 77 +++++++++----------
src/plugins/wp/Why3Provers.mli | 8 +-
src/plugins/wp/gui/GuiConfig.ml | 2 +-
.../wp/tests/wp_acsl/chunk_typing_usable.i | 2 +-
src/plugins/wp/tests/wp_acsl/classify_float.c | 2 +-
src/plugins/wp/tests/wp_acsl/div_mod.i | 2 -
src/plugins/wp/tests/wp_acsl/float_compare.i | 2 +-
.../oracle_qualif/classify_float.2.res.oracle | 13 ----
.../oracle_qualif/div_mod.1.res.oracle | 38 ---------
.../oracle_qualif/div_mod.2.res.oracle | 13 ----
...iv_mod.0.res.oracle => div_mod.res.oracle} | 0
src/plugins/wp/tests/wp_acsl/tset.i | 2 +-
.../tests/wp_gallery/binary-multiplication.c | 2 -
src/plugins/wp/tests/wp_plugin/abs.i | 2 +-
src/plugins/wp/tests/wp_plugin/bit_test.c | 2 +-
src/plugins/wp/tests/wp_plugin/fallback.i | 1 +
src/plugins/wp/tests/wp_plugin/float_format.i | 2 +-
src/plugins/wp/tests/wp_plugin/math.i | 3 +-
src/plugins/wp/tests/wp_plugin/nosession.i | 2 +-
.../wp_plugin/oracle/fallback.res.oracle | 2 +-
.../wp_plugin/oracle/sequence.res.oracle | 50 ++++++------
.../oracle_qualif/fallback.res.oracle | 13 ++--
.../wp_plugin/oracle_qualif/math.1.res.oracle | 22 ------
.../{math.0.res.oracle => math.res.oracle} | 0
.../oracle_qualif/sequence.0.res.oracle | 69 -----------------
.../oracle_qualif/sequence.1.res.oracle | 64 ---------------
.../oracle_qualif/sequence.2.res.oracle | 6 --
.../oracle_qualif/sequence.res.oracle | 69 +++++++++++++++++
src/plugins/wp/tests/wp_plugin/sequence.i | 10 ---
30 files changed, 153 insertions(+), 347 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
rename src/plugins/wp/tests/wp_acsl/oracle_qualif/{div_mod.0.res.oracle => div_mod.res.oracle} (100%)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
rename src/plugins/wp/tests/wp_plugin/oracle_qualif/{math.0.res.oracle => math.res.oracle} (100%)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.res.oracle
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 25d32bef0af..fb2766c4ac9 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -46,21 +46,11 @@ 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 ->
- Wp_parameters.error ~once:true
- "Prover '%s' not found in why3.conf" name ;
- None
+ | 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
let parse_mode m =
match String.lowercase_ascii m with
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 04d4e4e5a0a..f84d4b764a1 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,48 @@ 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 =
+ match String.split_on_char ':' @@ String.lowercase_ascii name with
+ | [name;version] -> List.filter (filter ~name ~version) @@ provers ()
+ | [name] -> List.sort by_version @@ List.filter (filter ~name) @@ provers ()
+ | _ -> []
+let lookup name = match select name with p :: _ -> Some p | [] -> None
+
(* -------------------------------------------------------------------------- *)
(* --- Models --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 0142173be48..11e189d5799 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 : 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/gui/GuiConfig.ml b/src/plugins/wp/gui/GuiConfig.ml
index f40609610d9..061068f4178 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 7681d66416b..3eced44d70b 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 ec858e5eedb..56142759693 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 10cf92b70f4..8fd5fb4e5cb 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 ff33d352a8f..3e5efe0a21c 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 d56892bed73..00000000000
--- 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 b02c8f809be..00000000000
--- 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 ed6ef43b129..00000000000
--- 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 9a2cbce1d8b..c7304aa8fb2 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 64a63d80a8d..91c3d02472d 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 160340d39d9..8e6b8f3a033 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 03c9e001851..8596c3bea92 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/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
index 2290dc57bd4..dc9e3482885 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.i
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -1,4 +1,5 @@
/* run.config_qualif
+ EXIT: 1
OPT: -wp-prover=Alt-Ergo:1.2.0
*/
diff --git a/src/plugins/wp/tests/wp_plugin/float_format.i b/src/plugins/wp/tests/wp_plugin/float_format.i
index 4a7f3dac8e9..0686e1ef489 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 891798bc632..bf12316c003 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 eb72aff708d..5c5012bb8de 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 02f6170d68a..c31f09c80a4 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 97cac771188..6a4ce52b61a 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 af751c1e16f..757ff0c0135 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,14 +4,11 @@
[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] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
-[wp] Proved goals: 3 / 3
- Terminating: 1
- Unreachable: 1
- Alt-Ergo: 1
+[wp] User Error: Prover 'Alt-Ergo:1.2.0' not found in why3.conf
+[wp] Goal typed_job_ensures : not tried
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- job - 1 1 100%
+ job - - 1 0.0%
------------------------------------------------------------
+[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
+[kernel] Plug-in wp aborted: invalid user input.
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 b8ae6b5a64a..00000000000
--- 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 31de6fd9f89..00000000000
--- 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 ac58a64fe0f..00000000000
--- 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 6a23c1a83b4..00000000000
--- 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 00000000000..15634da6162
--- /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 6d79c4df6a6..f69ebca6068 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 ;
--
GitLab