diff options
Diffstat (limited to 'compiler/BorrowCheck.ml')
-rw-r--r-- | compiler/BorrowCheck.ml | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/compiler/BorrowCheck.ml b/compiler/BorrowCheck.ml new file mode 100644 index 00000000..52f42c37 --- /dev/null +++ b/compiler/BorrowCheck.ml @@ -0,0 +1,28 @@ +open Interpreter +open LlbcAst + +(** The local logger *) +let log = Logging.borrow_check_log + +(** Borrow-check a crate. + + Note that we don't return anything: if we find borrow-checking errors, + we register them and print them later. + *) +let borrow_check_crate (crate : crate) : unit = + (* Debug *) + log#ldebug (lazy "translate_crate_to_pure"); + + (* Compute the translation context *) + let trans_ctx = compute_contexts crate in + + (* Borrow-check *) + let borrow_check_fun (fdef : fun_decl) : unit = + match fdef.body with + | None -> () + | Some _ -> + let synthesize = false in + let _ = evaluate_function_symbolic synthesize trans_ctx fdef in + () + in + List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls) |