[Eva] Garbled mix origins: renames top to unknown.

src/kernel_services/abstract_interp/cvalue.ml

@@ -240,7 +240,7 @@ module V = struct
 
   let pretty_typ typ fmt v =
     let pretty_org fmt org =
-      if not (Origin.is_top org) then
+      if not (Origin.is_unknown org) then
         Format.fprintf fmt "@ @[(origin: %a)@]" Origin.pretty org
     in
     match v with

src/kernel_services/abstract_interp/map_lattice.ml

@@ -286,7 +286,7 @@ module Make_MapSet_Lattice
 
   type t = Top of KSet.t * Origin.t | Map of KVMap.t
 
-  let top = Top (KSet.top, Origin.top)
+  let top = Top (KSet.top, Origin.unknown)
 
   let bottom = Map KVMap.empty
 

src/kernel_services/abstract_interp/offsetmap.ml

@@ -2803,14 +2803,14 @@ module Make_bitwise(V: sig
         in
         `Value (Int_Intervals.fold aux_itv itvs m)
     with Error_Top ->
-      update_imprecise_everywhere ~validity Origin.top v m
+      update_imprecise_everywhere ~validity Origin.unknown v m
 
   let add_binding_ival ~validity ~exact offsets ~size v m =
     match size with
     | Int_Base.Value size ->
       update ~validity ~exact ~offsets ~size v m
     | Int_Base.Top ->
-      update_imprecise_everywhere ~validity Origin.top v m
+      update_imprecise_everywhere ~validity Origin.unknown v m
 
   let fold_itv ?direction ~entire f itv m acc =
     let f' itv (v, _, _) acc = f itv v acc in

src/kernel_services/abstract_interp/origin.ml

@@ -53,8 +53,8 @@ let current kind =
   Origin { kind; loc; id; }
 
 let well = Well
-let top = Unknown
-let is_top t = t = Unknown
+let unknown = Unknown
+let is_unknown t = t = Unknown
 
 module Prototype = struct
   include Datatype.Serializable_undefined
@@ -91,7 +91,7 @@ end
 include Datatype.Make (Prototype)
 
 let pretty_as_reason fmt org =
-  if not (is_top org)
+  if not (is_unknown org)
   then Format.fprintf fmt " because of %a" pretty org
 
 let join t1 t2 =

src/kernel_services/abstract_interp/origin.mli

@@ -40,8 +40,8 @@ val current: kind -> t
 (** This is automatically extracted from [Cil.CurrentLoc] *)
 
 val well: t
-val top: t
-val is_top: t -> bool
+val unknown: t
+val is_unknown: t -> bool
 
 val pretty_as_reason: Format.formatter -> t -> unit
 (** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or

src/plugins/eva/domains/cvalue/warn.ml

@@ -67,7 +67,7 @@ let warn_imprecise_lval_read lv loc contents =
         Printer.pp_lval lv
         (fun fmt ->
            match loc.loc with
-           | Location_Bits.Top (param,o) when Origin.equal o Origin.top  ->
+           | Location_Bits.Top (param,o) when Origin.is_unknown o  ->
              Format.fprintf fmt "@[The location %a.@]@ "
                pretty_param param
            | Location_Bits.Top (param,orig) ->
@@ -83,7 +83,7 @@ let warn_imprecise_lval_read lv loc contents =
         )
         (fun fmt ->
            match contents with
-           | Location_Bytes.Top (param,o) when Origin.equal o Origin.top ->
+           | Location_Bytes.Top (param,o) when Origin.is_unknown o ->
              Format.fprintf fmt "@[%a.@]"
                pretty_param_b param
            | Location_Bytes.Top (param,orig) ->
@@ -109,7 +109,7 @@ let warn_right_exp_imprecision lv loc_lv exp_val =
              (Locations.pretty_english ~prefix:false) loc_lv
          | (Var _, _) -> ())
       (fun fmt org ->
-         if not (Origin.is_top origin) then
+         if not (Origin.is_unknown origin) then
            Format.fprintf fmt
              "@ @[The imprecision@ originates@ from@ %a@]"
              Origin.pretty org)

src/plugins/eva/domains/equality/equality_domain.ml

@@ -212,7 +212,7 @@ module Make
       fun v ->
         let c = get v in
         if Cvalue.V.is_imprecise c then
-          let c' = Cvalue.V.topify_with_origin Origin.top c in
+          let c' = Cvalue.V.topify_with_origin Origin.unknown c in
           Value.set Main_values.CVal.key c' v
         else v
 

src/plugins/eva/domains/multidim/multidim_domain.ml

@@ -75,12 +75,12 @@ struct
   let of_bit ~typ:_ = function
     | Abstract_memory.Uninitialized -> uninitialized
     | Zero i -> make i (V.inject_int Integer.zero)
-    | Any (Top, i) -> make i (V.top_with_origin Origin.top)
+    | Any (Top, i) -> make i (V.top_with_origin Origin.unknown)
     | Any (Set s, i) ->
       let v =
         if Base.Hptset.is_empty s
         then V.inject_ival Ival.top
-        else V.inject_top_origin Origin.top s
+        else V.inject_top_origin Origin.unknown s
       in
       make i v