Merge branch 'stable/nickel' into 'master'

Merge fixes from Nickel

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

dev/build-release.sh

@@ -95,12 +95,14 @@ VERSION_AND_CODENAME="${VERSION_SAFE}-${CODENAME}"
 if [ "$VERSION_MINOR" != 0 ]; then
   # We compare new minor to previous minor
   PREVIOUS="$VERSION_MAJOR.$((VERSION_MINOR - 1))"
+  PREVIOUS_TAG="$PREVIOUS"
 else
   # We compare new major to previous major, the exact previous version is not
   # of interest for a new major version
   PREVIOUS="$((VERSION_MAJOR - 1))"
+  PREVIOUS_TAG="$PREVIOUS.0"
 fi
-PREVIOUS_NAME=$(git show $PREVIOUS:VERSION_CODENAME)
+PREVIOUS_NAME=$(git show "$PREVIOUS_TAG":VERSION_CODENAME)
 
 if [ "$VERSION_MODIFIER" == "+dev" ]; then
   echo "Development version ($VERSION)"

ivette/package.json

 {
   "name": "ivette",
   "productName": "Ivette",
-  "version": "1.0.0",
+  "version": "28.0.0",
   "main": "index.js",
   "repository": "git@git.frama-c.com:frama-c/Ivette.git",
   "author": "Loïc Correnson <loic.correnson@cea.fr>",

ivette/src/dome/template/makefile

@@ -270,7 +270,7 @@ dome-dist-win: dome-app
 
 dome-dist-mac: dome-app
 	@echo "[Dome] packaging application (macOS exe)"
-	DOME=$(DOME) yarn run electron-builder --mac
+	DOME=$(DOME) yarn run electron-builder --mac -c.mac.identity=null
 	@echo "[Dome] application packaged in ./dist"
 
 # --------------------------------------------------------------------------

src/plugins/wp/Why3Provers.ml

@@ -62,16 +62,24 @@ 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 = Why3.Whyconf.parse_filter_prover s in
-    Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
+    let filter = parse_filter_prover s in
+    Some ((filter_one_prover config filter).prover)
   with
-  | Why3.Whyconf.ProverNotFound _
-  | Why3.Whyconf.ParseFilterProver _
-  | Why3.Whyconf.ProverAmbiguity _  ->
-    None
+  | ParseFilterProver _ -> None
+  | ProverNotFound _ -> None
+  | ProverAmbiguity (_, _, provers)  -> Some (resolve_ambiguity provers)
 
 type fallback = Exact of t | Fallback of t | NotFound
 
@@ -79,18 +87,14 @@ let find_fallback name =
   match find_opt name with
   | Some prv -> Exact prv
   | None ->
-    (* 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
+    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 ident_why3 = Why3.Whyconf.prover_parseable_format
 let ident_wp s =

src/plugins/wp/gui/GuiConfig.ml

@@ -36,7 +36,7 @@ class provers =
         (* select automatically the provers set on the command line *)
         let cmdline =
           match Wp_parameters.Provers.get () with
-          | [] -> [ "alt-ergo" ]
+          | [] -> [ "Alt-Ergo" ]
           | prvs -> prvs
         in
         let selection = List.fold_left

src/plugins/wp/register.ml

@@ -565,7 +565,7 @@ let spawn_wp_proofs ~script goals =
 
 let get_prover_names () =
   match Wp_parameters.Provers.get () with
-  | [] -> [ "alt-ergo" ] | pnames -> pnames
+  | [] -> [ "Alt-Ergo" ] | pnames -> pnames
 
 let compute_provers ~mode ~script =
   script.provers <- List.fold_right

src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml

@@ -22,7 +22,7 @@ let run () =
          | None -> prvs
          | Some VCS.Tactical -> prvs
          | Some prv -> (VCS.Batch, prv) :: prvs)
-      ["alt-ergo"] []
+      ["Alt-Ergo"] []
   in
 
   let spawn goal =