summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-22 10:33:17 +0100
committerSon Ho2021-11-22 10:33:17 +0100
commit3d47e1943547780aed2f86736bfaef31c6431ce0 (patch)
tree4ad235a99db7426e8fb3ed983490951f583108da
parent61e54d5c7fa5e8662d8cc438f4f2bd4856bf3ca6 (diff)
Implement abs_to_string
-rw-r--r--src/Print.ml13
-rw-r--r--src/Values.ml5
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.