summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-05 18:36:47 +0100
committerSon Ho2022-01-05 18:36:47 +0100
commitd22f5d1ae5155c53b9cd0daf165dccb5d5563c1f (patch)
tree8358f23b1eb4ee5b8200ab3e77c234d1c1f248d6 /src/Values.ml
parentb191de7f680e4ae43178fc42ccabc91808e189f8 (diff)
Finish implementing eval_local_function_call_symbolic
Diffstat (limited to '')
-rw-r--r--src/Values.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/Values.ml b/src/Values.ml
index 001c0347..ae9eb127 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -542,9 +542,6 @@ and typed_avalue = { value : avalue; ty : rty }
type abs = {
abs_id : (AbstractionId.id[@opaque]);
parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *)
- acc_regions : (RegionId.set_t[@opaque]);
- (** Union of the regions owned by the (transitive) parent abstractions and
- by the current abstraction. TODO: why do we need those? *)
regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *)
avalues : typed_avalue list; (** The values in this abstraction *)
}