From 534c70dc60ce26da3117395b916d1cabd4033abd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 10:07:29 +0100
Subject: Implement the SharedBorrow case of
 SymbolicToPure.typed_value_to_rvalue

---
 src/SymbolicToPure.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index a77a64ca..e0ee557a 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -533,9 +533,6 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
     - function call
     - end abstraction
     - return
-    
-    TODO: we have a problem with shared borrows. I think the shared borrows
-    should carry the shared value as a meta-value.
  *)
 let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
     =
@@ -554,9 +551,10 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
         | MutLoan _ -> failwith "Unreachable")
     | Borrow bc -> (
         match bc with
-        | V.SharedBorrow _ ->
-            (* TODO: *)
-            raise Unimplemented
+        | V.SharedBorrow (mv, _) ->
+            (* The meta-value stored in the shared borrow was added especially
+             * for this case (because we can't use the borrow id for lookups) *)
+            (translate mv).value
         | V.InactivatedMutBorrow _ -> failwith "Unreachable"
         | V.MutBorrow (_, v) ->
             (* Borrows are the identity in the extraction *)
-- 
cgit v1.2.3