From 49c8e42ec3bcfc323e61c5ba0345abeb41372ac4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 14:50:21 +0200
Subject: Implement a BorrowCheck.borrow_check_crate

---
 compiler/BorrowCheck.ml | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 compiler/BorrowCheck.ml

(limited to 'compiler/BorrowCheck.ml')

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)
-- 
cgit v1.2.3