From 6b9653a3f1a361c72eb841a5a9c04a374b99c8e5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 19:22:08 +0100
Subject: Cleanup a bit

---
 src/Interpreter.ml | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3c8e40b6..770c1c71 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -4262,17 +4262,6 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
   in
   (* Substitute the signature *)
   let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
-  (* TODO: cut from here *)
-  (* Generate a fresh symbolic value for the return value *)
-  let ret_sv_ty = inst_sg.A.output in
-  let ctx, ret_spc =
-    mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx
-  in
-  let ret_value = mk_typed_value_from_proj_comp ret_spc in
-  let ret_av = V.ASymbolic (V.AProjLoans ret_spc.V.svalue) in
-  let ret_av : V.typed_avalue =
-    { V.value = ret_av; V.ty = ret_spc.V.svalue.V.sv_ty }
-  in
   (* Sanity check *)
   assert (List.length args = def.A.arg_count);
   (* Evaluate the function call *)
-- 
cgit v1.2.3