From 4252473c00bd6bf8dc4adaa55c2f74ffe119e0c1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 21 Feb 2020 15:44:50 +0100
Subject: [PATCH] [wp] prover name fallback
---
src/plugins/wp/Changelog | 4 +-
src/plugins/wp/ProverWhy3.ml | 2 +-
src/plugins/wp/VCS.ml | 35 ++++++-----
src/plugins/wp/Why3Provers.ml | 46 ++++++--------
src/plugins/wp/Why3Provers.mli | 7 ++-
src/plugins/wp/doc/manual/wp_plugin.tex | 23 +++----
src/plugins/wp/register.ml | 4 +-
.../oracle_qualif/classify_float.1.res.oracle | 4 +-
.../oracle_qualif/classify_float.2.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/cnf.res.oracle | 62 +++++++++----------
.../wp_bts/oracle_qualif/bts_1174.res.oracle | 2 +-
.../oracle_qualif/bts_2471.1.res.oracle | 2 +-
.../oracle_qualif/bts_2471.2.res.oracle | 2 +-
.../oracle_qualif/issue_143.3.res.oracle | 2 +-
src/plugins/wp/tests/wp_plugin/fallback.i | 6 ++
.../wp_plugin/oracle/fallback.res.oracle | 15 +++++
.../wp_plugin/oracle_qualif/abs.1.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/abs.2.res.oracle | 4 +-
.../oracle_qualif/convert.1.res.oracle | 4 +-
.../oracle_qualif/fallback.res.oracle | 15 +++++
.../oracle_qualif/float_format.0.res.oracle | 2 +-
.../oracle_qualif/float_format.1.res.oracle | 2 +-
.../oracle_qualif/inductive.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/math.1.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/math.3.res.oracle | 2 +-
25 files changed, 148 insertions(+), 107 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/fallback.i
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 4f52be2cbe9..51d6fba4b02 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,7 +20,9 @@
# <Prover>: prover
###############################################################################
--* WP [2020/02/20] Fixes handling of LoopCurrent in loop invariants
+- WP [2020/02/21] Why3 prover version fallback
+- WP [2020/02/21] Why3 prover full-names use ':' instead of ','
+-* WP [2020/02/20] Fixes handling of LoopCurrent in loop invariants
- WP [2019/12/04] Added option -wp-run-all-provers
##########################
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index f225a3cb684..c73eea6a1d8 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1264,7 +1264,7 @@ let task_hash wpo drv prover task =
let _ = Command.print_file file
begin fun fmt ->
Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
- (Why3Provers.print prover) ;
+ (Why3Provers.print_why3 prover) ;
Why3.Driver.print_task_prepared drv fmt task ;
end
in Digest.file file |> Digest.to_hex
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index f71051092d0..ad02dc72d23 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -63,10 +63,19 @@ let prover_of_name = function
Why3.Whyconf.prover_version = "";
Why3.Whyconf.prover_altern = "generate only" })
| s ->
- match Extlib.string_del_prefix "why3:" s with
- | Some "" -> None
- | Some s' -> Some (Why3 (Why3Provers.find s'))
- | None -> Some (Why3 (Why3Provers.find 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
+ "Prover '%s' not found, fallback to '%s'"
+ (String.concat ":" prv) (Why3Provers.print_wp p) ;
+ Some (Why3 p)
+ | NotFound ->
+ Wp_parameters.error "Prover '%s' not found in why3.conf" name ;
+ None
let mode_of_prover_name = function
| "native:coqedit" -> EditMode
@@ -74,16 +83,16 @@ let mode_of_prover_name = function
| _ -> BatchMode
let name_of_prover = function
- | Why3 s -> "why3:" ^ (Why3Provers.print s)
- | NativeAltErgo -> "alt-ergo"
- | NativeCoq -> "coq"
+ | Why3 s -> Why3Provers.print_wp s
+ | NativeAltErgo -> "native:alt-ergo"
+ | NativeCoq -> "native:coq"
| Qed -> "qed"
| Tactical -> "script"
let title_of_prover = function
| Why3 s -> Why3Provers.title s
- | NativeAltErgo -> "Alt-Ergo"
- | NativeCoq -> "Coq"
+ | NativeAltErgo -> "Alt-Ergo (native)"
+ | NativeCoq -> "Coq (native)"
| Qed -> "Qed"
| Tactical -> "Script"
@@ -107,7 +116,7 @@ let sanitize_why3 s =
Buffer.contents buffer
let filename_for_prover = function
- | Why3 s -> sanitize_why3 (Why3Provers.print s)
+ | Why3 s -> sanitize_why3 (Why3Provers.print_wp s)
| NativeAltErgo -> "Alt-Ergo"
| NativeCoq -> "Coq"
| Qed -> "Qed"
@@ -136,11 +145,7 @@ let cmp_prover p q =
let pp_prover fmt = function
| NativeAltErgo -> Format.pp_print_string fmt "Alt-Ergo (Native)"
| NativeCoq -> Format.pp_print_string fmt "Coq (Native)"
- | Why3 smt ->
- if Wp_parameters.debug_atleast 1 then
- Format.fprintf fmt "Why:%s" (Why3Provers.print smt)
- else
- Format.pp_print_string fmt (Why3Provers.title smt)
+ | Why3 smt -> Format.pp_print_string fmt (Why3Provers.title smt)
| Qed -> Format.fprintf fmt "Qed"
| Tactical -> Format.pp_print_string fmt "Tactical"
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index a7bb7832566..7c7095340b0 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -70,33 +70,27 @@ let find_opt s =
| Why3.Whyconf.ProverAmbiguity _ ->
None
-let find ?donotfail s =
- try
- try
- let config = Lazy.force cfg in
- let filter = Why3.Whyconf.parse_filter_prover s in
- let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
- (Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover
- with
- | Why3.Whyconf.ProverNotFound _ as exn when donotfail <> None ->
- Wp_parameters.warning ~once:true "%a" Why3.Exn_printer.exn_printer exn;
- (** from Why3.Whyconf.parse_filter_prover *)
- let sl = Why3.Strings.rev_split ',' s in
- (* reverse order *)
- let prover_name, prover_version, prover_altern =
- match sl with
- | [name] -> name,"",""
- | [version;name] -> name,version,""
- | [altern;version;name] -> name,version,altern
- | _ -> raise (Why3.Whyconf.ParseFilterProver s) in
- { Why3.Whyconf.prover_name; Why3.Whyconf.prover_version; Why3.Whyconf.prover_altern }
- with
- | ( Why3.Whyconf.ProverNotFound _
- | Why3.Whyconf.ParseFilterProver _
- | Why3.Whyconf.ProverAmbiguity _ ) as exn ->
- Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
+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 (String.lowercase_ascii shortname) with
+ | Some prv -> Fallback prv
+ | None -> NotFound
+ end
+ | _ -> NotFound
+
+let print_why3 = Why3.Whyconf.prover_parseable_format
+let print_wp s =
+ let name = Why3.Whyconf.prover_parseable_format s in
+ let prv = String.split_on_char ',' name in
+ String.concat ":" prv
-let print = Why3.Whyconf.prover_parseable_format
let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
let compare = Why3.Whyconf.Prover.compare
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index d08bf2d0337..2e53fcdbead 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -28,9 +28,12 @@ val set_procs : int -> unit
type t = Why3.Whyconf.prover
val find_opt : string -> t option
-val find : ?donotfail:unit -> string -> t
-val print : t -> string
+type fallback = Exact of t | Fallback of t | NotFound
+val find_fallback : string -> fallback
+
+val print_why3 : t -> string
+val print_wp : t -> string
val title : t -> string
val compare : t -> t -> int
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 82d7691f3e1..a7eacac8514 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1032,24 +1032,25 @@ Support for \textsf{Why-3 IDE} is no longer provided.
Suppose you have the following configuration:
\begin{logs}
-# frama-c -wp-detect
-[wp] Why3 provers detected:
- - Alt-Ergo 2.0.0 [alt-ergo,altergo]
- - CVC4 1.6 [cvc4]
- - CVC4 1.6 (counterexamples) [cvc4-ce]
- - Coq 8.9.0 [coq]
- - Z3 4.6.0 [z3]
- - Z3 4.6.0 (counterexamples) [z3-ce]
- - Z3 4.6.0 (noBV) [z3-nobv]
+$ ./bin/frama-c -wp-detect
+[wp] Prover Alt-Ergo 2.0.0 [alt-ergo|altergo|Alt-Ergo:2.0.0]
+[wp] Prover CVC4 1.6 [cvc4|CVC4:1.6]
+[wp] Prover CVC4 1.6 [cvc4-ce|CVC4:1.6,counterexamples]
+[wp] Prover Eprover 2.4 [eprover|Eprover:2.4]
+[wp] Prover Z3 4.8.7 [z3-ce|Z3:4.8.7:counterexamples]
\end{logs}
Then, to use (for instance) \textsf{CVC4 1.6},
-you can use \verb+-wp-prover cvc4+.
+you can use \verb+-wp-prover cvc4+ or \verb+-wp-prover CVC4:1.6.
Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+.
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}.
-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.
+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.
+
+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.
%% \paragraph{Sessions.}
%% Your \textsf{Why3} session is saved in the \texttt{"project.session"}
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 5ee0a232c14..19ec59bd109 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -919,10 +919,10 @@ let do_prover_detect () =
shortcuts in
List.iter
(fun p ->
- Wp_parameters.result "Prover %10s %-6s [%a%a]"
+ Wp_parameters.result "Prover %10s %-6s [%a%s]"
p.prover_name p.prover_version
print_prover_shortcuts_for p
- print_prover_parseable_format p
+ (Why3Provers.print_wp p)
) provers
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index a082bf32458..66f1ea11458 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
@@ -8,8 +8,8 @@
[wp] [Alt-Ergo (Native)] Goal typed_lemma_InfP_not_finite : Valid
[wp] [Alt-Ergo (Native)] Goal typed_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3
- Qed: 0
- Alt-Ergo: 3
+ Qed: 0
+ Alt-Ergo (native): 3
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 3 100%
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
index 31c7f0957d7..a2f933bfe8c 100644
--- 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
@@ -12,7 +12,7 @@
[wp] [Coq (Native)] Goal typed_lemma_NaN_not_finite : Valid
[wp] Proved goals: 3 / 3
Qed: 0
- Coq: 3
+ Coq (native): 3
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 3 100%
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 19943bc4eb4..a682b67b435 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -11,14 +11,14 @@
[wp:cnf] CNF=P_A2
[wp] [Qed] Goal typed_f_ensures_a2 : Valid
[wp:cnf] CNF=((not P_A1) \/ P_A2) /\ (P_A1 \/ (not P_A2))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a3 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a3 : Valid
[wp:cnf] CNF=((not P_A) \/ P_A1) /\ (P_A \/ P_A2)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a4 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a4 : Valid
[wp:cnf]
CNF=(P_A \/ P_B) /\ (P_A \/ P_B1) /\ (P_A \/ P_B2) /\ (P_A \/ P_C)
/\ (P_A1 \/ P_B) /\ (P_A1 \/ P_B1) /\ (P_A1 \/ P_B2) /\ (P_A1 \/ P_C)
/\ (P_A2 \/ P_B) /\ (P_A2 \/ P_B1) /\ (P_A2 \/ P_B2) /\ (P_A2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a5 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a5 : Valid
[wp:cnf]
CNF=(P_A \/ P_A1 \/ P_A2 \/ P_C) /\ (P_A \/ P_A1 \/ P_A2 \/ P_B \/ P_C)
/\ (P_A \/ P_A1 \/ P_A2 \/ P_B1 \/ P_C)
@@ -27,7 +27,7 @@
/\ (P_A \/ P_A1 \/ P_A2 \/ P_B \/ P_B1 \/ P_C)
/\ (P_A \/ P_A1 \/ P_A2 \/ P_B \/ P_B2 \/ P_C)
/\ (P_A \/ P_A1 \/ P_A2 \/ P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a6 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a6 : Valid
[wp:cnf]
CNF=(P_A2 \/ P_C) /\ (P_A2 \/ (not P_B) \/ P_C)
/\ (P_A2 \/ (not P_B1) \/ P_C) /\ (P_A2 \/ P_B2 \/ P_C)
@@ -35,7 +35,7 @@
/\ (P_A2 \/ (not P_B) \/ (not P_B1) \/ P_C)
/\ (P_A2 \/ (not P_B) \/ P_B2 \/ P_C)
/\ (P_A2 \/ (not P_B1) \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a7 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a7 : Valid
[wp:cnf]
CNF=((not P_A1) \/ P_A2 \/ P_C) /\ (P_A1 \/ (not P_A2) \/ P_C)
/\ ((not P_A1) \/ P_A2 \/ (not P_B1) \/ P_B2)
@@ -58,7 +58,7 @@
/\ (P_A1 \/ (not P_A2) \/ (not P_B1) \/ P_B2 \/ P_C)
/\ (P_A1 \/ (not P_A2) \/ P_B1 \/ (not P_B2) \/ P_C)
/\ (P_A1 \/ (not P_A2) \/ P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a8 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a8 : Valid
[wp:cnf]
CNF=((not P_A) \/ P_A1 \/ P_C) /\ (P_A \/ P_A2 \/ P_C)
/\ ((not P_A) \/ P_A1 \/ (not P_B) \/ P_B1)
@@ -120,17 +120,17 @@
/\ ((not P_A) \/ P_A1 \/ P_A2 \/ P_B \/ P_B1 \/ P_B2 \/ P_C)
/\ (P_A \/ P_A1 \/ P_A2 \/ (not P_B) \/ P_B1 \/ P_B2 \/ P_C)
/\ (P_A \/ P_A1 \/ P_A2 \/ P_B \/ P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_a9 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_a9 : Valid
[wp:cnf] CNF=P_B /\ P_B1 /\ P_B2 /\ P_C
[wp] [Qed] Goal typed_f_ensures_b0 : Valid
[wp:cnf] CNF=P_C /\ (P_B \/ P_B1 \/ P_B2)
[wp] [Qed] Goal typed_f_ensures_b1 : Valid
[wp:cnf] CNF=P_C /\ ((not P_B) \/ (not P_B1) \/ P_B2)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_b2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_b2 : Valid
[wp:cnf] CNF=P_C /\ ((not P_B1) \/ P_B2) /\ (P_B1 \/ (not P_B2))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_b3 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_b3 : Valid
[wp:cnf] CNF=P_C /\ ((not P_B) \/ P_B1) /\ (P_B \/ P_B2)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_b4 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_b4 : Valid
[wp:cnf] CNF=true
[wp] [Qed] Goal typed_f_ensures_b5 : Valid
[wp:cnf] CNF=P_B \/ P_B1 \/ P_B2 \/ P_C1
@@ -140,17 +140,17 @@
[wp:cnf] CNF=true
[wp] [Qed] Goal typed_f_ensures_b9 : Valid
[wp:cnf] CNF=(P_B \/ P_C) /\ (P_B1 \/ P_C) /\ (P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c0 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c0 : Valid
[wp:cnf] CNF=P_B \/ P_B1 \/ P_B2 \/ P_C
[wp] [Qed] Goal typed_f_ensures_c1 : Valid
[wp:cnf] CNF=P_B2 \/ P_C
[wp] [Qed] Goal typed_f_ensures_c2 : Valid
[wp:cnf] CNF=((not P_B1) \/ P_B2 \/ P_C) /\ (P_B1 \/ (not P_B2) \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c3 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c3 : Valid
[wp:cnf]
CNF=((not P_B) \/ P_B1 \/ P_C) /\ (P_B \/ P_B2 \/ P_C)
/\ ((not P_B) \/ P_B1 \/ P_B2 \/ P_C) /\ (P_B \/ P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c4 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c4 : Valid
[wp:cnf]
CNF=(P_B \/ (not P_C) \/ (not P_C1)) /\ (P_B \/ P_C \/ P_C1)
/\ (P_B1 \/ (not P_C) \/ (not P_C1)) /\ (P_B1 \/ P_C \/ P_C1)
@@ -179,7 +179,7 @@
/\ (P_B \/ (not P_B1) \/ (not P_B2) \/ P_C \/ P_C1)
/\ (P_B \/ (not P_B1) \/ P_B2 \/ P_C \/ P_C1)
/\ (P_B \/ P_B1 \/ (not P_B2) \/ P_C \/ P_C1)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c5 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c5 : Valid
[wp:cnf]
CNF=((not P_B) \/ P_C1) /\ ((not P_B1) \/ P_C1) /\ ((not P_B2) \/ P_C1)
/\ ((not P_B) \/ (not P_B1) \/ P_C1)
@@ -206,7 +206,7 @@
/\ (P_B \/ P_B1 \/ (not P_B2) \/ (not P_C) \/ P_C1)
/\ (P_B \/ P_B1 \/ P_B2 \/ (not P_C) \/ (not P_C1))
/\ (P_B \/ P_B1 \/ P_B2 \/ P_C \/ P_C1)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c6 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c6 : Valid
[wp:cnf]
CNF=((not P_B2) \/ P_C1) /\ (P_B \/ P_C1) /\ (P_B1 \/ P_C1)
/\ ((not P_B) \/ (not P_B2) \/ P_C1) /\ ((not P_B) \/ P_B1 \/ P_C1)
@@ -232,72 +232,72 @@
/\ ((not P_B) \/ (not P_B1) \/ P_B2 \/ P_C \/ P_C1)
/\ ((not P_B) \/ P_B1 \/ P_B2 \/ (not P_C) \/ P_C1)
/\ (P_B \/ (not P_B1) \/ P_B2 \/ (not P_C) \/ P_C1)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c7 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c7 : Valid
[wp:cnf] Too big CNF/DNF
[wp:cnf]
CNF=((P_C \/ (P_B2 <-> P_B1)) -> ((P_B2 <-> P_B1) <-> P_C1))
/\ (((P_B2 <-> P_B1) <-> P_C1) -> (P_C \/ (P_B2 <-> P_B1)))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c8 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c8 : Valid
[wp:cnf] Too big CNF/DNF
[wp:cnf]
CNF=((P_C \/ ((P_B -> P_B1) /\ ((not P_B) -> P_B2)))
-> ((P_B2 <-> P_B1) <-> P_C1))
/\ (((P_B2 <-> P_B1) <-> P_C1)
-> (P_C \/ ((P_B -> P_B1) /\ ((not P_B) -> P_B2))))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_c9 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_c9 : Valid
[wp:cnf]
CNF=(P_B \/ (not P_C)) /\ (P_B1 \/ (not P_C)) /\ (P_B2 \/ (not P_C))
/\ ((not P_B) \/ (not P_B1) \/ (not P_B2) \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d0 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d0 : Valid
[wp:cnf]
CNF=((not P_B) \/ P_C) /\ ((not P_B1) \/ P_C) /\ ((not P_B2) \/ P_C)
/\ (P_B \/ P_B1 \/ P_B2 \/ (not P_C))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d1 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d1 : Valid
[wp:cnf]
CNF=((not P_B2) \/ P_C) /\ (P_B \/ P_C) /\ (P_B1 \/ P_C)
/\ ((not P_B) \/ (not P_B1) \/ P_B2 \/ (not P_C))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d2 : Valid
[wp:cnf]
CNF=((not P_B1) \/ (not P_B2) \/ P_C) /\ ((not P_B1) \/ P_B2 \/ (not P_C))
/\ (P_B1 \/ (not P_B2) \/ (not P_C)) /\ (P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d3 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d3 : Valid
[wp:cnf]
CNF=((not P_B) \/ (not P_B1) \/ P_C) /\ ((not P_B) \/ P_B1 \/ (not P_C))
/\ ((not P_B1) \/ (not P_B2) \/ P_C) /\ (P_B \/ (not P_B2) \/ P_C)
/\ (P_B \/ P_B2 \/ (not P_C))
/\ ((not P_B) \/ P_B1 \/ P_B2 \/ (not P_C))
/\ (P_B \/ P_B1 \/ P_B2 \/ (not P_C))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d4 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d4 : Valid
[wp:cnf]
CNF=((not P_B1) \/ P_B2) /\ (P_B \/ (not P_B1)) /\ (P_B \/ (not P_B2))
/\ (P_B \/ (not P_C)) /\ (P_B1 \/ (not P_B2)) /\ (P_B1 \/ (not P_C))
/\ (P_B2 \/ (not P_C))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d5 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d5 : Valid
[wp:cnf]
CNF=((not P_B) \/ P_B1 \/ P_B2 \/ P_C) /\ (P_B \/ P_B1 \/ P_B2 \/ (not P_C))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d6 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d6 : Valid
[wp:cnf]
CNF=((not P_B) \/ (not P_B1) \/ P_B2) /\ (P_B1 \/ P_B2 \/ P_C)
/\ ((not P_B) \/ (not P_B1) \/ P_B2 \/ (not P_C))
/\ (P_B \/ P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d7 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d7 : Valid
[wp:cnf]
CNF=((not P_B1) \/ P_B2) /\ (P_B1 \/ (not P_B2))
/\ ((not P_B1) \/ P_B2 \/ (not P_C))
/\ (P_B1 \/ (not P_B2) \/ (not P_C)) /\ (P_B1 \/ P_B2 \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d8 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d8 : Valid
[wp:cnf]
CNF=((not P_B) \/ P_B1 \/ (not P_B2)) /\ ((not P_B) \/ P_B1 \/ (not P_C))
/\ (P_B \/ (not P_B1) \/ P_B2) /\ (P_B \/ P_B2 \/ (not P_C))
/\ ((not P_B) \/ P_B1 \/ P_B2 \/ (not P_C))
/\ (P_B \/ P_B1 \/ P_B2 \/ (not P_C))
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_d9 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_d9 : Valid
[wp:cnf] CNF=P_A /\ ((not P_B) \/ P_C) /\ ((not P_A) \/ (not P_B) \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_e0 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_e0 : Valid
[wp:cnf] CNF=P_B /\ ((not P_B) \/ P_C) /\ ((not P_A) \/ (not P_B) \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_e1 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_e1 : Valid
[wp:cnf] CNF=P_C /\ ((not P_B) \/ P_C) /\ ((not P_A) \/ (not P_B) \/ P_C)
-[wp] [Why:Alt-Ergo,2.0.0] Goal typed_f_ensures_e2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures_e2 : Valid
[wp] Proved goals: 43 / 43
Qed: 12
Alt-Ergo 2.0.0: 31
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
index 96e57860259..84548daae80 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
@@ -9,7 +9,7 @@
[wp] [Coq (Native)] Goal typed_real_job_assert_qed_ok : Valid
[wp] Proved goals: 1 / 1
Qed: 0
- Coq: 1
+ Coq (native): 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - - 1 100%
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
index 945eb815d75..59c1f47d165 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
@@ -7,7 +7,7 @@
[wp] 1 goal scheduled
[wp] [Alt-Ergo (Native)] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unsuccess: 1)
+ Alt-Ergo (native): 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
index 4e7f9b5df66..de7fa3935c2 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
@@ -8,7 +8,7 @@
[wp] [Coq] Goal typed_foo_assert_ko : Default tactic
[wp] [Coq (Native)] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1
- Coq: 0 (unsuccess: 1)
+ Coq (native): 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
index c9e8d86aca4..5f1f89f93b8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
@@ -10,7 +10,7 @@
[wp] [Coq (Native)] Goal typed_lemma_ok_because_consistent : Failed
Command './tests/inexistant-prover' not found
[wp] Proved goals: 0 / 2
- Coq: 0 (failed: 2)
+ Coq (native): 0 (failed: 2)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic A - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
new file mode 100644
index 00000000000..2290dc57bd4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -0,0 +1,6 @@
+/* run.config_qualif
+ OPT: -wp-prover=Alt-Ergo:1.2.0
+ */
+
+/*@ ensures \result == a * b ; */
+int job(int a,int b) { return (a - 1)*b + b ; }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
new file mode 100644
index 00000000000..61fd74dd9d8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
@@ -0,0 +1,15 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/fallback.i, line 5) 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_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
index 73390320340..e509833a656 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
@@ -9,7 +9,7 @@
[wp] [Coq (Native)] Goal typed_abs_abs_ensures : Valid
[wp] Proved goals: 1 / 1
Qed: 0
- Coq: 1
+ Coq (native): 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
abs - - 1 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
index 9bab36322ce..c23f1aadec1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
@@ -7,8 +7,8 @@
[wp] 1 goal scheduled
[wp] [Alt-Ergo (Native)] Goal typed_abs_abs_ensures : Valid
[wp] Proved goals: 1 / 1
- Qed: 0
- Alt-Ergo: 1
+ Qed: 0
+ Alt-Ergo (native): 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
abs - - 1 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index bc2790699b3..e2d9341755d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -7,8 +7,8 @@
[wp] [Alt-Ergo (Native)] Goal typed_lemma_ceil : Valid
[wp] [Alt-Ergo (Native)] Goal typed_lemma_floor : Valid
[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
+ Qed: 0
+ Alt-Ergo (native): 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 2 100%
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
new file mode 100644
index 00000000000..c4e27534a76
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -0,0 +1,15 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/fallback.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo 2.0.0] Goal typed_job_ensures : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Alt-Ergo 2.0.0: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job - 1 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
index 0e688ad1d41..41ad4aa4977 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
@@ -11,7 +11,7 @@
[wp] [Coq] Goal typed_output_ensures_KO : Default tactic
[wp] [Coq (Native)] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- Coq: 0 (unsuccess: 1)
+ Coq (native): 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
output - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index 46763154314..cf394e79b34 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
@@ -10,7 +10,7 @@
[wp] 1 goal scheduled
[wp] [Alt-Ergo (Native)] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unsuccess: 1)
+ Alt-Ergo (native): 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
output - - 1 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
index 9ef8f395f9c..100d4304b66 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
@@ -10,7 +10,7 @@
[wp] [Coq (Native)] Goal typed_lemma_test : Valid
[wp] Proved goals: 2 / 2
Qed: 0
- Coq: 2
+ Coq (native): 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 2 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
index 34ddb8162cb..c017e1da01d 100644
--- 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
@@ -36,8 +36,8 @@
[wp] [Alt-Ergo (Native)] Goal typed_ok_ensures_sqrt_pos : Valid
[wp] [Alt-Ergo (Native)] Goal typed_ok_ensures_sqrt_pos0 : Valid
[wp] Proved goals: 30 / 30
- Qed: 5
- Alt-Ergo: 25
+ Qed: 5
+ Alt-Ergo (native): 25
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma 3 - 19 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index 5e68c91300c..2e45968da18 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -15,7 +15,7 @@
[wp] [Alt-Ergo (Native)] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
[wp] [Alt-Ergo (Native)] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
[wp] Proved goals: 0 / 9
- Alt-Ergo: 0 (unsuccess: 9)
+ Alt-Ergo (native): 0 (unsuccess: 9)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
ko - - 9 0.0%
--
GitLab