Merge branch 'fix/wp/why3-prover-detection' into 'stable/titanium'

Fix Why3 prover detection

See merge request frama-c/frama-c!2926

opam/opam

@@ -135,3 +135,7 @@ messages: [
   "The Frama-C/Wp native support for Coq is now deprecated (use TIP or Why-3 instead)."
   {coq:installed}
 ]
+
+post-messages: [
+  "Why3 provers setup: rm -r ~/.why3.conf ; why3 config --detect"
+]

src/plugins/wp/Why3Provers.ml

@@ -64,7 +64,6 @@ let find_opt s =
   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
     Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
   with
   | Why3.Whyconf.ProverNotFound _
@@ -78,14 +77,18 @@ 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
+      (* Why3 should deal with this intermediate case *)
+      match find_opt (String.lowercase_ascii 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 =