[Eva] Lmap.add_binding does not check if the written value is bottom.

This case should be processed by the caller if needed.

src/kernel_services/abstract_interp/cvalue.ml

@@ -1058,6 +1058,11 @@ module Model = struct
     let v = find_indeterminate ~conflate_bottom state loc in
     V_Or_Uninitialized.get_v v
 
+  let add_binding ~exact mem loc v =
+    if V_Or_Uninitialized.is_bottom v
+    then bottom
+    else add_binding ~exact mem loc v
+
   let add_indeterminate_binding ~exact mem loc v =
     add_binding ~exact mem loc v
 

src/kernel_services/abstract_interp/lmap.ml

@@ -656,17 +656,14 @@ struct
     | Map m -> Map (M.add_base_value base ~size v ~size_v m)
 
   let add_binding ~exact m loc v =
-    (* TODO: this should depend on bottom being strict. *)
-    if V.equal v V.bottom then Bottom
-    else
-      match m with
-      | Top -> Top
-      | Bottom -> Bottom
-      | Map m ->
-        try
-          let non_bottom, r = M.add_binding ~exact m loc v in
-          if non_bottom then Map r else Bottom
-        with M.Result_is_top -> Top
+    match m with
+    | Top -> Top
+    | Bottom -> Bottom
+    | Map m ->
+      try
+        let non_bottom, r = M.add_binding ~exact m loc v in
+        if non_bottom then Map r else Bottom
+      with M.Result_is_top -> Top
 
   let find ?(conflate_bottom=true) m loc =
     match m with