summaryrefslogtreecommitdiff
path: root/src/Synthesis.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Synthesis.ml')
-rw-r--r--src/Synthesis.ml7
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
=