diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index aa3c9b484b35e309d6343b8bffbfbefdd658254a..f401f1594ad1c808bca9fa2c2909eaba6f127dd5 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/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
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 62bb89ef6cddb8192951f297deaadd932b7f2f2e..204ad8aa11e5eeea839c306f7343033f456b7f88 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/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
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 0b88644948d8017cb4c40384c3591101ac45a011..2585c74c98c1599bb6c55475e6cd695b76ca1ffd 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/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
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index c3c4b4e1ac47a2492699f46d98ac869ac2ed2def..2b743f0d8540fa1d95052b20b33ff304bd1c6d2c 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/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 =
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 572f9d586946995be6faf4ae7f92e72dd7d8a2c0..a739d8dca4c4782a0f71d99b6e9a881d0e08ebe2 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/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
diff --git a/src/plugins/eva/domains/cvalue/warn.ml b/src/plugins/eva/domains/cvalue/warn.ml
index 3604d914973d55ba0cf412c4b6aee1436ec81f32..402f79f5702e6ba776db5bdded866e41561d0d50 100644
--- a/src/plugins/eva/domains/cvalue/warn.ml
+++ b/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)
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 9c7407b2d0138c580d74b96b56252074168718ea..55affa63dc9a97b8759e9139264972c7e574d5c2 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/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
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index d721e62e638a22343470bb3815108b0e92ad2ec0..c5606b0ebeb8571025778bb05ca5f1fb8434c374 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/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