From 0f6f44df1cfd24c6bc6ee8874da7596e12dfb438 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 25 Apr 2022 09:55:29 +0200
Subject: [PATCH] [Eva] Multidim: [Abstract_offset.references] returns a set
instead of a list.
---
src/plugins/value/domains/multidim/abstract_offset.ml | 4 ++--
src/plugins/value/domains/multidim/abstract_offset.mli | 2 +-
src/plugins/value/domains/multidim/multidim_domain.ml | 4 ++--
3 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/domains/multidim/abstract_offset.ml b/src/plugins/value/domains/multidim/abstract_offset.ml
index 366d77da8fa..bb77adc682a 100644
--- a/src/plugins/value/domains/multidim/abstract_offset.ml
+++ b/src/plugins/value/domains/multidim/abstract_offset.ml
@@ -249,7 +249,7 @@ let references =
| Field (_, sub) | Index (None, _, _, sub) -> aux acc sub
| Index (Some e, _, _, sub) ->
let r = Cil.extract_varinfos_from_exp e in
- let acc = (Cil_datatype.Varinfo.Set.to_seq r |> List.of_seq) @ acc in
+ let acc = Cil_datatype.Varinfo.Set.union r acc in
aux acc sub
in
- aux []
+ aux Cil_datatype.Varinfo.Set.empty
diff --git a/src/plugins/value/domains/multidim/abstract_offset.mli b/src/plugins/value/domains/multidim/abstract_offset.mli
index b200d12f69c..8281c8a662e 100644
--- a/src/plugins/value/domains/multidim/abstract_offset.mli
+++ b/src/plugins/value/domains/multidim/abstract_offset.mli
@@ -36,7 +36,7 @@ val of_ival : base_typ:Cil_types.typ -> typ:Cil_types.typ -> Ival.t -> t or_top
val of_term_offset : Cil_types.typ -> Cil_types.term_offset -> t or_top
val is_singleton : t -> bool
-val references : t -> Cil_types.varinfo list (* variables referenced in the offset *)
+val references : t -> Cil_datatype.Varinfo.Set.t (* variables referenced in the offset *)
val append : t -> t -> t (* Does not check that the appened offset fits *)
val join : t -> t -> t or_top
diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index 2fcc17bd224..2f6459d9c5c 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -168,9 +168,9 @@ struct
let add_refs _b o acc =
match o with
| `Top -> acc
- | `Value o -> Set.union (Set.of_list (Offset.references o)) acc
+ | `Value o -> Set.union (Offset.references o) acc
in
- Map.fold add_refs map Set.empty |> Set.to_seq |> List.of_seq
+ Map.fold add_refs map Set.empty |> Set.elements
let of_var (vi : Cil_types.varinfo) : t =
Map.singleton (Base.of_varinfo vi) (`Value (Offset.of_var_address vi))
--
GitLab