diff options
| -rw-r--r-- | src/Invariants.ml | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index b67fa3a2..0478459b 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -9,6 +9,7 @@ module Subst = Substitute module A = CfimAst module L = Logging open InterpreterUtils +open Errors let debug_invariants : bool ref = ref false @@ -333,7 +334,28 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = let info = { outer_borrow = false; outer_shared = false } in visitor#visit_eval_ctx info ctx -let check_typing_invariant (_ctx : C.eval_ctx) : unit = () +let check_typing_invariant (ctx : C.eval_ctx) : unit = + let visitor = + object + inherit [_] C.iter_eval_ctx as super + + method! visit_typed_value info tv = + (* Check this pair (value, type) *) + (match (tv.V.value, tv.V.ty) with + | V.Concrete cv, _ -> raise Unimplemented + | V.Adt av, _ -> raise Unimplemented + | V.Bottom, _ -> (* Nothing to check *) () + | V.Borrow bc, _ -> raise Unimplemented + | V.Loan lc, _ -> raise Unimplemented + | V.Symbolic spc, _ -> raise Unimplemented + | _ -> failwith "Inconsistent typing"); + (* Continue exploring to inspect the subterms *) + super#visit_typed_value info tv + + method! visit_typed_avalue info atv = raise Unimplemented + end + in + visitor#visit_eval_ctx () ctx let check_invariants (ctx : C.eval_ctx) : unit = check_loans_borrows_relation_invariant ctx; |