blob: 52f42c37f33968210065f017c87f9ec9b459c072 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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)
|
