diff options
author | Son Ho | 2022-01-05 19:21:13 +0100 |
---|---|---|
committer | Son Ho | 2022-01-05 19:21:13 +0100 |
commit | 8f2038542bcb8ec93b6c6447f38d098cff98fc2c (patch) | |
tree | 68f63c4bc83152813fc4044cf51348db6f6ce8f8 /src/Synthesis.ml | |
parent | 4feb960fe3b5d58a5420b0c569bcea645a420b9f (diff) |
Split eval_local_function_call_symbolic to isolate a function which can
be reused for non-local function calls
Diffstat (limited to '')
-rw-r--r-- | src/Synthesis.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/Synthesis.ml b/src/Synthesis.ml index 60c387d2..1f683209 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -63,12 +63,7 @@ let synthesize_eval_rvalue_aggregate (aggregate_kind : E.aggregate_kind) (ops : E.operand list) : unit = () -let synthesize_non_local_function_call (fid : A.assumed_fun_id) - (region_params : T.erased_region list) (type_params : T.ety list) - (args : E.operand list) (dest : E.place) : unit = - () - -let synthesize_local_function_call (fid : A.FunDefId.id) +let synthesize_function_call (fid : A.fun_id) (region_params : T.erased_region list) (type_params : T.ety list) (args : V.typed_value list) (dest : E.place) (res : V.symbolic_value) : unit = |