From c0f230dc6c331e9eb120900e8c31a03e1f5ab476 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 18 Jan 2022 23:03:55 +0100
Subject: Remove ty_has_regions and use ty_has_borrows instead

---
 src/InterpreterExpressions.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/InterpreterExpressions.ml')

diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f15c7558..60918bac 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -35,7 +35,10 @@ let expand_primitively_copyable_at_place (config : C.config)
   (* Small helper *)
   let rec expand ctx =
     let v = read_place_unwrap config access p ctx in
-    match find_first_primitively_copyable_sv v with
+    match
+      find_first_primitively_copyable_sv_with_borrows
+        ctx.type_context.type_infos v
+    with
     | None -> ctx
     | Some sv ->
         let ctx = expand_symbolic_value_no_branching config sv ctx in
@@ -178,7 +181,10 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) :
       let ctx, v = prepare_rplace config expand_prim_copy access p ctx in
       (* Copy the value *)
       assert (not (bottom_in_value ctx.ended_regions v));
-      assert (Option.is_none (find_first_primitively_copyable_sv v));
+      assert (
+        Option.is_none
+          (find_first_primitively_copyable_sv_with_borrows
+             ctx.type_context.type_infos v));
       let allow_adt_copy = false in
       copy_value allow_adt_copy config ctx v
   | Expressions.Move p -> (
-- 
cgit v1.2.3