From 3d47e1943547780aed2f86736bfaef31c6431ce0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 22 Nov 2021 10:33:17 +0100 Subject: Implement abs_to_string --- src/Print.ml | 13 +++++++++++++ src/Values.ml | 5 +++-- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/src/Print.ml b/src/Print.ml index 1555afc4..0240a307 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -379,4 +379,17 @@ module Values = struct ^ ")" | AProjBorrows (sv, rty) -> "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" + + let abs_to_string (fmt : value_formatter) (abs : abs) : string = + let avs = + List.map (fun av -> " " ^ typed_avalue_to_string fmt av) abs.avalues + in + let avs = String.concat ",\n" avs in + "abs@" + ^ AbstractionId.to_string abs.abs_id + ^ "{parents=" + ^ AbstractionId.set_to_string abs.parents + ^ "}" ^ "{regions=" + ^ RegionId.set_to_string abs.regions + ^ "}" ^ " {\n" ^ avs ^ "\n}" end diff --git a/src/Values.ml b/src/Values.ml index d63ace85..90267ce1 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -171,12 +171,13 @@ and aproj = and typed_avalue = { avalue : avalue; aty : rty } type abs = { - parents : AbstractionId.Set.t; (** The parent abstraction *) + abs_id : AbstractionId.id; + parents : AbstractionId.Set.t; (** The parent abstractions *) acc_regions : RegionId.Set.t; (** Union of the regions owned by the (transitive) parent abstractions and by the current abstraction *) regions : RegionId.Set.t; (** Regions owned by this abstraction *) - values : typed_avalue list; (** The values in this abstraction *) + avalues : typed_avalue list; (** The values in this abstraction *) } (** Abstractions model the parts in the borrow graph where the borrowing relations have been abstracted because of a function call. -- cgit v1.2.3