From 8c3dc80d255ba2000d35c0bcdf9dbe927215bb81 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Jun 2022 06:51:08 +0200
Subject: Add `can_end` in `abs` and use it for the return abs when generating
 the backward functions

---
 src/InterpreterBorrows.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/InterpreterBorrows.ml')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index f5f3a8fa..26374bf7 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -985,6 +985,9 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
   (* Lookup the abstraction *)
   let abs = C.ctx_lookup_abs ctx abs_id in
 
+  (* Check that we can end the abstraction *)
+  assert abs.can_end;
+
   (* End the parent abstractions first *)
   let cc = end_abstractions config chain abs.parents in
   let cc =
-- 
cgit v1.2.3