diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index f401f1594ad1c808bca9fa2c2909eaba6f127dd5..a37f6ce682a5ac6020fe0f1d8582e436f46ff46e 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -504,11 +504,7 @@ module V = struct
with Not_based_on_null ->
if is_bottom e1 || is_bottom e2
then bottom
- else begin
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
- end
+ else topify_with_origin_kind topify (join e1 e2)
let arithmetic_function = import_function ~topify:Origin.Arith
@@ -540,9 +536,7 @@ module V = struct
try (* On the off chance that someone writes [i+(int)&p]... *)
Location_Bytes.shift (project_ival_bottom e1) e2
with Not_based_on_null ->
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ topify_with_origin_kind topify (join e1 e2)
end
with Not_found ->
(* we end up here if the only way left to make this
@@ -551,9 +545,7 @@ module V = struct
let right = Ival.scale_int_base factor (project_ival_bottom e2)
in Location_Bytes.shift right e1
with Not_based_on_null -> (* from [project_ival] *)
- join
- (topify_with_origin_kind topify e1)
- (topify_with_origin_kind topify e2)
+ topify_with_origin_kind topify (join e1 e2)
(* Under-approximating variant of add_untyped. Takes two
under-approximation, and returns an under-approximation.*)
@@ -669,9 +661,7 @@ module V = struct
then
bottom
else
- join
- (topify_with_origin_kind topify acc)
- (topify_with_origin_kind topify value)
+ topify_with_origin_kind topify (join acc value)
end
else
add_untyped ~topify ~factor:Int_Base.one value acc
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 768e9c12c4280d39cd317043436c1ad2e8601301..b9e0540726066a639a043cfbf61adcd38ed4e1b7 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -213,11 +213,9 @@ module Location_Bytes = struct
let topify_with_origin o v =
match v with
- | Top (s,a) ->
- Top (s, Origin.join a o)
- | v when is_zero v -> v
+ | Top _ -> v
| Map _ ->
- if equal v bottom then v
+ if is_zero v || equal v bottom then v
else
match get_keys v with
| Base.SetLattice.Top -> top_with_origin o
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 08fa4d98a93a955bd17f37776e332b8e9bca9a84..3359a012d02299a38bfd84124b21d0696b67ce0b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -1721,7 +1721,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let clip = clip_by_validity validity in
let r = fold
(fun (min, max as itv) (bound_v, _, _) acc ->
- let new_v = V.join (V.topify_with_origin o bound_v) v in
+ let new_v = V.topify_with_origin o (V.join bound_v v) in
let new_min, new_max = clip itv in
if new_min <=~ new_max then (* [min..max] and validity intersect *)
let acc =
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 99acf93c89cf194109e40cb81e16a96723b20aac..fd87a5148a45852f89a9bf5092f2785b3128701c 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -171,7 +171,7 @@ let clear () = History.clear ()
(* Keep the oldest known origin: it is probably the most relevant origin, as
subsequent ones may have been created because of the first. *)
let join t1 t2 =
- if t1 == t2 then t1 else
+ if equal t1 t2 then t1 else
match t1, t2 with
| Unknown, x | x, Unknown -> x
| Well, _ | _, Well -> Well
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 43b19bd42586c0c09577be32dd4c1aefe5958e90..094e3c9124c5027a8dd52a47d6eabe7e27989eaa 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -212,7 +212,7 @@ module State = struct
| Some location ->
let location = Precise_locs.imprecise_location location in
let v = Cvalue.Model.find ~conflate_bottom:false state location in
- Cvalue.V.join acc (Cvalue.V.topify_leaf_origin v)
+ Cvalue.V.topify_leaf_origin (Cvalue.V.join acc v)
else acc
in
List.fold_left one_from_contents Cvalue.V.top_int deps
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index 3f8b7a6bf342b97743c197ee9512490b8e823415..b3482f725d252d9d56188928a6adaeb7c8920b5d 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -364,7 +364,7 @@ let forward_minus_pp ~typ ev1 ev2 =
try
V.inject_ival (conv (Cvalue.V.project_ival minus_val))
with Cvalue.V.Not_based_on_null ->
- V.join (V.topify_arith_origin ev1) (V.topify_arith_origin ev2)
+ V.topify_arith_origin (V.join ev1 ev2)
else
(* Pointwise arithmetics.*)
let v = V.sub_pointer ev1 ev2 in
@@ -410,7 +410,7 @@ let forward_binop_int ~typ ev1 op ev2 =
let forward_binop_float fkind ev1 op ev2 =
match V.project_float ev1, V.project_float ev2 with
| exception V.Not_based_on_null ->
- V.join (V.topify_arith_origin ev1) (V.topify_arith_origin ev2)
+ V.topify_arith_origin (V.join ev1 ev2)
| f1, f2 ->
let binary_float_floats (_name: string) f =
V.inject_float (f fkind f1 f2)
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index 6fe4eedb72486a27ebdc2582a036bea66c8573cd..1559794a477915a5ad20d5b9232252094712ec3f 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -580,7 +580,7 @@
v4.x ∈ [--..--]
.y ∈ {{ (int)&t }}
{.p; .padding[0..23]} ∈ [--..--]
- v5 ∈ {{ garbled mix of &{t} (origin: Arithmetic {memcpy.c:91}) }}
+ v5 ∈ {{ garbled mix of &{t} (origin: Misaligned read {memcpy.c:91}) }}
t{[0]; [1]{.x; .y}} ∈ {0}
[1].p ∈ {{ &v1.y }}
{[1].padding[0..23]; [2]; [3]{.x; .y}} ∈ {0}