diff options
Diffstat (limited to 'src/Synthesis.ml')
| -rw-r--r-- | src/Synthesis.ml | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/src/Synthesis.ml b/src/Synthesis.ml index b0ecd554..b45c2810 100644 --- a/src/Synthesis.ml +++ b/src/Synthesis.ml @@ -5,7 +5,7 @@ module C = Contexts module Subst = Substitute module A = CfimAst module L = Logging -open InterpreterUtils +open Cps open InterpreterProjectors (* for symbolic_expansion definition *) @@ -25,6 +25,19 @@ open InterpreterProjectors (* TODO: error Panic *) +(* +type synth_function_res = + (P.expression option, InterpreterExpressions.eval_error) result + +type synth_function = C.eval_ctx -> synth_function_res +(** The synthesis functions (and thus the interpreter functions) are written + in a continuation passing style. *) +*) + +let synthesize_symbolic_expansion (_sv : V.symbolic_value) (resl : sexpr list) : + sexpr = + SList resl + (** Synthesize code for a symbolic expansion which doesn't lead to branching (i.e., applied on a value which is not an enumeration with several variants). *) @@ -53,22 +66,23 @@ let synthesize_binary_op (_binop : E.binop) (_op1 : V.typed_value) (_op2 : V.typed_value) (_dest : V.symbolic_value) : unit = () -(** Actually not sure if we need this, or a synthesize_symbolic_expansion_enum *) -let synthesize_eval_rvalue_discriminant (_p : E.place) : unit = () - +(* let synthesize_eval_rvalue_ref (_p : E.place) (_bkind : E.borrow_kind) : unit = () +*) let synthesize_eval_rvalue_aggregate (_aggregate_kind : E.aggregate_kind) (_ops : E.operand list) : unit = () +(* 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 = () -let synthesize_panic () : unit = () +(*let synthesize_panic () : unit = ()*) let synthesize_assert (_v : V.typed_value) : unit = () + *) |