blob: f6a5b6b0e4f8b5e3c490281403f98a922ffb8254 (
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
29
30
31
|
(* The following module defines functions to check that some invariants
* are always maintained by evaluation contexts *)
module T = Types
module V = Values
open Scalars
module E = Expressions
open Errors
module C = Contexts
module Subst = Substitute
module A = CfimAst
module L = Logging
open TypesUtils
open ValuesUtils
(** Check that:
- loans and borrows are correctly related
- borrows/loans can't contain ⊥ or inactivated mut borrows
- shared loans can't contain mutable loans
- TODO: a two-phase borrow can't point to a value inside an abstraction
*)
let check_borrows_invariant (ctx : C.eval_ctx) : unit = ()
let check_no_bottom_below_ref_invariant (ctx : C.eval_ctx) : unit = ()
let check_typing_invariant (ctx : C.eval_ctx) : unit = ()
let check_invariants (ctx : C.eval_ctx) : unit =
check_borrows_invariant ctx;
check_no_bottom_below_ref_invariant ctx;
check_typing_invariant ctx
|
