From bbb1ea77402545d52af0bb0076923d99ecc4c9e2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Feb 2022 20:49:46 +0100
Subject: Add an option to allow the presence of bottom values below borrows

---
 src/Invariants.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/Invariants.ml')

diff --git a/src/Invariants.ml b/src/Invariants.ml
index fff5b897..0e4b1e23 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -298,14 +298,15 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
     - borrows/loans can't contain ⊥ or inactivated mut borrows
     - shared loans can't contain mutable loans
  *)
-let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit =
+let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) :
+    unit =
   let visitor =
     object
       inherit [_] C.iter_eval_ctx as super
 
       method! visit_Bottom info =
         (* No ⊥ inside borrowed values *)
-        assert (not info.outer_borrow)
+        assert (config.C.allow_bottom_below_borrow || not info.outer_borrow)
 
       method! visit_ABottom _info =
         (* ⊥ inside an abstraction is not the same as in a regular value *)
@@ -784,7 +785,7 @@ let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
   if config.C.check_invariants then (
     log#ldebug (lazy "Checking invariants");
     check_loans_borrows_relation_invariant ctx;
-    check_borrowed_values_invariant ctx;
+    check_borrowed_values_invariant config ctx;
     check_typing_invariant ctx;
     check_symbolic_values config ctx)
   else log#ldebug (lazy "Not checking invariants (check is not activated)")
-- 
cgit v1.2.3