From 7a89bb9fc212d804a5227ad937c5e5b2e0c6d360 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 3 Jan 2022 16:26:14 +0100
Subject: Make more progress

---
 src/Interpreter.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index fc87b6d2..68b92361 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1644,7 +1644,16 @@ let convert_avalue_to_value (ended_regions : T.RegionId.set_t)
     (ctx, { V.value = V.Bottom; V.ty })
   else
     (* Doesn't contain ended regions: return a symbolic value *)
-    raise Unimplemented
+    let ctx, sv_id = C.fresh_symbolic_value_id ctx in
+    let svalue : V.symbolic_value = { V.sv_id; sv_ty = av.V.ty } in
+    let value : V.symbolic_proj_comp =
+      (* Note that the set of ended regions is empty: we shouldn't have to take
+       * into account any ended regions at this point, otherwise we would be in
+       * the first case where we should return ⊥ *)
+      { V.svalue; V.rset_ended = T.RegionId.Set.empty }
+    in
+    let value = V.Symbolic value in
+    (ctx, { V.value; V.ty })
 
 (** End a borrow identified by its borrow id in a context
     
-- 
cgit v1.2.3