diff options
author | Son Ho | 2024-04-11 20:31:16 +0200 |
---|---|---|
committer | Son Ho | 2024-04-11 20:31:16 +0200 |
commit | b6421bc01df278f625a8c95b4ea36ad2e4355718 (patch) | |
tree | 6246ef2b038560e3deae41e4fa700f14390cd14f /compiler/Interpreter.ml | |
parent | 44065f447dc3a2f4b1441b97b9687d1c1b85afbf (diff) | |
parent | 2f8aa9b47acb5c98aed91c29b04f71099452e781 (diff) |
Merge branch 'son/clean' into checked-ops
Diffstat (limited to 'compiler/Interpreter.ml')
-rw-r--r-- | compiler/Interpreter.ml | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index a65e1663..769e3144 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : * do it, and because it gives a bit of sanity. * *) let sg = fdef.signature in + (* Sanity check: no nested borrows, borrows in ADTs, etc. *) + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty)) + (sg.output :: sg.inputs)) + fdef.meta "Nested borrows are not supported yet"; + cassert __FILE__ __LINE__ + (List.for_all + (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty)) + (sg.output :: sg.inputs)) + fdef.meta "ADTs containing borrows are not supported yet"; + (* Create the context *) let regions_hierarchy = FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies @@ -612,7 +624,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* Evaluate the function *) let symbolic = - eval_function_body config (Option.get fdef.body).body cf_finish ctx + try eval_function_body config (Option.get fdef.body).body cf_finish ctx + with CFailure (meta, msg) -> Some (Error (meta, msg)) in (* Return *) |