Skip to content
Snippets Groups Projects
Commit e5f87adf authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Restore exact match as performed by Why3

parent 4c32277d
No related branches found
No related tags found
No related merge requests found
...@@ -63,7 +63,7 @@ type t = Why3.Whyconf.prover ...@@ -63,7 +63,7 @@ type t = Why3.Whyconf.prover
let find_opt s = let find_opt s =
try try
let config = Lazy.force cfg in let config = Lazy.force cfg in
let filter = Why3.Whyconf.parse_filter_prover (String.lowercase_ascii s) in let filter = Why3.Whyconf.parse_filter_prover s in
Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover) Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
with with
| Why3.Whyconf.ProverNotFound _ | Why3.Whyconf.ProverNotFound _
...@@ -77,14 +77,18 @@ let find_fallback name = ...@@ -77,14 +77,18 @@ let find_fallback name =
match find_opt name with match find_opt name with
| Some prv -> Exact prv | Some prv -> Exact prv
| None -> | None ->
match String.split_on_char ',' name with (* Why3 should deal with this intermediate case *)
| shortname :: _ :: _ -> match find_opt (String.lowercase_ascii name) with
begin | Some prv -> Exact prv
match find_opt (String.lowercase_ascii shortname) with | None ->
| Some prv -> Fallback prv match String.split_on_char ',' name with
| None -> NotFound | shortname :: _ :: _ ->
end begin
| _ -> NotFound 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_why3 = Why3.Whyconf.prover_parseable_format
let print_wp s = let print_wp s =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment