summaryrefslogtreecommitdiff
path: root/src/SynthesizeSymbolic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/SynthesizeSymbolic.ml')
-rw-r--r--src/SynthesizeSymbolic.ml19
1 files changed, 11 insertions, 8 deletions
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index c0d4489c..d578a13e 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -81,29 +81,32 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
synthesize_symbolic_expansion sv [ Some see ] exprl
-let synthesize_function_call (call_id : call_id) (type_params : T.ety list)
+let synthesize_function_call (call_id : call_id)
+ (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
(args : V.typed_value list) (dest : V.symbolic_value)
(expr : expression option) : expression option =
match expr with
| None -> None
| Some expr ->
- let call = { call_id; type_params; args; dest } in
+ let call = { call_id; abstractions; type_params; args; dest } in
Some (FunCall (call, expr))
let synthesize_regular_function_call (fun_id : A.fun_id)
- (call_id : V.FunCallId.id) (type_params : T.ety list)
- (args : V.typed_value list) (dest : V.symbolic_value)
- (expr : expression option) : expression option =
- synthesize_function_call (Fun (fun_id, call_id)) type_params args dest expr
+ (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
+ (type_params : T.ety list) (args : V.typed_value list)
+ (dest : V.symbolic_value) (expr : expression option) : expression option =
+ synthesize_function_call
+ (Fun (fun_id, call_id))
+ abstractions type_params args dest expr
let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
(dest : V.symbolic_value) (expr : expression option) : expression option =
- synthesize_function_call (Unop unop) [] [ arg ] dest expr
+ synthesize_function_call (Unop unop) [] [] [ arg ] dest expr
let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
(arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option)
: expression option =
- synthesize_function_call (Binop binop) [] [ arg0; arg1 ] dest expr
+ synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] dest expr
let synthesize_aggregated_value (aggr_v : V.typed_value)
(expr : expression option) : expression option =