diff --git a/src/plugins/value/domains/multidim/abstract_offset.ml b/src/plugins/value/domains/multidim/abstract_offset.ml index 366d77da8fa62f64051566184e488a58c9b2dc55..bb77adc682ab5a53f53505262a5c29c6b678ff99 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 b200d12f69ceb185544e2cab47e295ba575e53a4..8281c8a662e24ea4095ab71aa8c9100054266a33 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 2fcc17bd224e18e4f6ac04c8d518237675a7f059..2f6459d9c5c63631f202e43bf47504a6dfb34690 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))