From 0658739222a23474c5453eb32f282587ae8eb95e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jan 2022 21:56:36 +0100
Subject: Update the projectors to ignore values when they don't contain
 regions of interest

---
 src/Values.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'src/Values.ml')

diff --git a/src/Values.ml b/src/Values.ml
index 707986f8..9d25025e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -236,7 +236,8 @@ class ['self] map_typed_avalue_base =
 *)
 type avalue =
   | AConcrete of constant_value
-      (** Note that this case is not used in the projections to keep track of the
+      (** TODO: remove
+          Note that this case is not used in the projections to keep track of the
           borrow graph (because there are no borrows in "concrete" values!) but
           to correctly instantiate the backward functions (we may give back some
           values at different moments: we need to remember what those values were
@@ -250,7 +251,9 @@ type avalue =
   | ALoan of aloan_content
   | ABorrow of aborrow_content
   | ASymbolic of aproj
-  | AIgnored  (** A value we don't own and thus ignore *)
+  | AIgnored
+      (** A value which doesn't contain borrows, or which borrows we
+          don't own and thus ignore *)
 
 and adt_avalue = {
   variant_id : (VariantId.id option[@opaque]);
-- 
cgit v1.2.3