Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

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)