summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-05 19:22:08 +0100
committerSon Ho2022-01-05 19:22:08 +0100
commit6b9653a3f1a361c72eb841a5a9c04a374b99c8e5 (patch)
treeee14b7f18c2642ce284153d610ff4b0959b676d8 /src
parent8f2038542bcb8ec93b6c6447f38d098cff98fc2c (diff)
Cleanup a bit
Diffstat (limited to 'src')
-rw-r--r--src/Interpreter.ml11
1 files changed, 0 insertions, 11 deletions
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 *)