diff options
Diffstat (limited to 'src/Invariants.ml')
-rw-r--r-- | src/Invariants.ml | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml new file mode 100644 index 00000000..f6a5b6b0 --- /dev/null +++ b/src/Invariants.ml @@ -0,0 +1,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 |