diff options
author | Son Ho | 2022-01-05 19:22:08 +0100 |
---|---|---|
committer | Son Ho | 2022-01-05 19:22:08 +0100 |
commit | 6b9653a3f1a361c72eb841a5a9c04a374b99c8e5 (patch) | |
tree | ee14b7f18c2642ce284153d610ff4b0959b676d8 /src | |
parent | 8f2038542bcb8ec93b6c6447f38d098cff98fc2c (diff) |
Cleanup a bit
Diffstat (limited to 'src')
-rw-r--r-- | src/Interpreter.ml | 11 |
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 *) |