[Eva] Uses Map.union instead of Map.merge.

src/plugins/value/engine/subdivided_evaluation.ml

@@ -67,16 +67,12 @@ let union expr depth map1 map2 =
   let top = ref LvalSet.empty in
   (* Lvalues such that a lvalue from [!top] appears in their subexpression. *)
   let deps = ref LvalSet.empty in
-  let merge lval a b = match a, b with
-    | None, None -> None
-    | Some x, None
-    | None, Some x -> Some x
-    | Some (_, _, deps1), Some (_, _, deps2) ->
-      top := LvalSet.add lval !top;
-      deps := LvalSet.union (LvalSet.union deps1 deps2) !deps;
-      Some (expr, depth, LvalSet.union deps1 deps2)
+  let merge lval (_, _, deps1) (_, _, deps2) =
+    top := LvalSet.add lval !top;
+    deps := LvalSet.union (LvalSet.union deps1 deps2) !deps;
+    Some (expr, depth, LvalSet.union deps1 deps2)
   in
-  let map = LvalMap.merge merge map1 map2 in
+  let map = LvalMap.union merge map1 map2 in
   LvalMap.mapi
     (fun lval (e, d, lvs) ->
        (* Alls lvalues in [expr] now appear in the subexpression of [!top]. *)

src/plugins/value/legacy/eval_terms.ml

@@ -164,13 +164,9 @@ let find_or_alarm ~alarm_mode state loc =
 type labels_states = Cvalue.Model.t Logic_label.Map.t
 
 let join_label_states m1 m2 =
-  let aux _ s1 s2 = match s1, s2 with
-    | None, None -> None
-    | Some s, None | None, Some s -> Some s
-    | Some s1, Some s2 -> Some (Cvalue.Model.join s1 s2)
-  in
+  let aux _ s1 s2 = Some (Cvalue.Model.join s1 s2) in
   if m1 == m2 then m1
-  else Logic_label.Map.merge aux m1 m2
+  else Logic_label.Map.union aux m1 m2
 
 (* The logic can refer to the state at other points of the program
    using labels. [e_cur] indicates the current label (in changes when

src/plugins/value/utils/structure.ml

@@ -140,11 +140,6 @@ module Open
 
   type 'a getter = Get : ('a, 'b) get -> 'a getter
 
-  let merge _k a b = match a, b with
-    | Some _, _ -> a
-    | _, Some _ -> b
-    | None, None -> assert false
-
   let lift_get f (Get (key, get)) = Get (key, fun t -> get (f t))
 
   let rec compute_getters : type a. a structure -> (a getter) KMap.t = function
@@ -153,7 +148,7 @@ module Open
     | Node (left, right) ->
       let l = compute_getters left and r = compute_getters right in
       let l = KMap.map (lift_get fst) l and r = KMap.map (lift_get snd) r in
-      KMap.merge merge l r
+      KMap.union (fun _k a _b -> Some a) l r
 
   let getters = compute_getters M.structure
   let get (type a) (key: a Shape.key) : (M.t -> a) option =
@@ -177,7 +172,7 @@ module Open
       let l = compute_setters left and r = compute_setters right in
       let l = KMap.map (lift_set (fun set (l, r) -> set l, r)) l
       and r = KMap.map (lift_set (fun set (l, r) -> l, set r)) r in
-      KMap.merge merge l r
+      KMap.union (fun _k a _b -> Some a) l r
 
   let setters = compute_setters M.structure
   let set (type a) (key: a Shape.key) : (a -> M.t -> M.t) =

src/plugins/value/utils/value_results.ml

@@ -319,12 +319,8 @@ let merge r1 r2 =
     | True, True -> True
   in
   let merge_callers _ m1 m2 =
-    let aux _kf s1 s2 = match s1, s2 with
-      | None, None -> None
-      | None, s | s, None -> s
-      | Some s1, Some s2 -> Some (Stmt.Set.union s1 s2)
-    in
-    Kernel_function.Map.merge aux m1 m2
+    let aux _kf s1 s2 = Some (Stmt.Set.union s1 s2) in
+    Kernel_function.Map.union aux m1 m2
   in
   let merge_s_cs = StmtH.merge merge_cs in
   let main = match r1.main, r2.main with

src/plugins/value_types/widen_type.ml

@@ -88,40 +88,33 @@ include Datatype.Make(struct
   end)
 
 let join wh1 wh2 =
-  let map_merge s_join os1 os2 =
-    match os1, os2 with
-    | Some bs1, Some bs2 -> Some (s_join bs1 bs2)
-    | Some bs, None | None, Some bs -> Some bs
-    | None, None -> None
-  in
+  let map_union s_join _key bs1 bs2 = Some (s_join bs1 bs2) in
   { priority_bases =
-      Stmt.Map.merge (fun _key -> map_merge Base.Set.union)
+      Stmt.Map.union (map_union Base.Set.union)
         wh1.priority_bases wh2.priority_bases;
     default_hints =
       Ival.Widen_Hints.union wh1.default_hints wh2.default_hints;
     default_float_hints =
       Fc_float.Widen_Hints.union wh1.default_float_hints wh2.default_float_hints;
     default_hints_by_stmt =
-      Stmt.Map.merge (fun _key -> map_merge Ival.Widen_Hints.union)
+      Stmt.Map.union (map_union Ival.Widen_Hints.union)
         wh1.default_hints_by_stmt wh2.default_hints_by_stmt;
     default_float_hints_by_stmt =
-      Stmt.Map.merge (fun _key -> map_merge Fc_float.Widen_Hints.union)
+      Stmt.Map.union (map_union Fc_float.Widen_Hints.union)
         wh1.default_float_hints_by_stmt wh2.default_float_hints_by_stmt;
     hints_by_addr =
-      Base.Map.merge (fun _key -> map_merge Ival.Widen_Hints.union)
+      Base.Map.union (map_union Ival.Widen_Hints.union)
         wh1.hints_by_addr wh2.hints_by_addr;
     float_hints_by_addr =
-      Base.Map.merge (fun _key -> map_merge Fc_float.Widen_Hints.union)
+      Base.Map.union (map_union Fc_float.Widen_Hints.union)
         wh1.float_hints_by_addr wh2.float_hints_by_addr;
     hints_by_addr_by_stmt =
-      Stmt.Map.merge (fun _key ->
-          map_merge (Base.Map.merge
-                       (fun _key -> map_merge Ival.Widen_Hints.union)))
+      Stmt.Map.union
+        (map_union (Base.Map.union (map_union Ival.Widen_Hints.union)))
         wh1.hints_by_addr_by_stmt wh2.hints_by_addr_by_stmt;
     float_hints_by_addr_by_stmt =
-      Stmt.Map.merge (fun _key ->
-          map_merge (Base.Map.merge
-                       (fun _key -> map_merge Fc_float.Widen_Hints.union)))
+      Stmt.Map.union
+        (map_union (Base.Map.union (map_union Fc_float.Widen_Hints.union)))
         wh1.float_hints_by_addr_by_stmt wh2.float_hints_by_addr_by_stmt;
   }
 
@@ -196,23 +189,17 @@ let hints_from_keys stmt h =
   let int_hints_by_base =
     try
       let at_stmt = Stmt.Map.find stmt h.hints_by_addr_by_stmt in
-      Base.Map.merge (fun _b os1 os2 ->
-          match os1, os2 with
-          | Some s1, Some s2 -> Some (Ival.Widen_Hints.union s1 s2)
-          | Some s, None | None, Some s -> Some s
-          | None, None -> None
-        ) at_stmt h.hints_by_addr
+      Base.Map.union
+        (fun _b s1 s2 -> Some (Ival.Widen_Hints.union s1 s2))
+        at_stmt h.hints_by_addr
     with Not_found -> h.hints_by_addr
   in
   let float_hints_by_base =
     try
       let at_stmt = Stmt.Map.find stmt h.float_hints_by_addr_by_stmt in
-      Base.Map.merge (fun _b os1 os2 ->
-          match os1, os2 with
-          | Some s1, Some s2 -> Some (Fc_float.Widen_Hints.union s1 s2)
-          | Some s, None | None, Some s -> Some s
-          | None, None -> None
-        ) at_stmt h.float_hints_by_addr
+      Base.Map.union
+        (fun _b s1 s2 -> Some (Fc_float.Widen_Hints.union s1 s2))
+        at_stmt h.float_hints_by_addr
     with Not_found -> h.float_hints_by_addr
   in
   let prio =