diff options
Diffstat (limited to 'compiler/Interpreter.ml')
| -rw-r--r-- | compiler/Interpreter.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index fb3701f3..81d6ff72 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -489,9 +489,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) - the list of symbolic values introduced for the input values (this is useful for the synthesis) - the symbolic AST generated by the symbolic execution + + If [synthesize] is [true]: we synthesize the symbolic AST that is used for + the translation. Otherwise, we do not (the symbolic execution then simply + borrow-checks the function). *) -let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) : - symbolic_value list * SA.expression = +let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) + (fdef : fun_decl) : symbolic_value list * SA.expression option = (* Debug *) let name_to_string () = Print.Types.name_to_string @@ -615,9 +619,13 @@ let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) : let ctx_resl, cc = eval_function_body config (Option.get fdef.body).body ctx in - let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in - cc el - with CFailure (span, msg) -> Error (span, msg) + if synthesize then + (* Finish synthesizing *) + let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in + Some (cc el) + else None + with CFailure (span, msg) -> + if synthesize then Some (Error (span, msg)) else None in (* Return *) (input_svs, symbolic) |