diff options
| author | Son Ho | 2022-01-04 23:11:14 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-04 23:11:14 +0100 |
| commit | 1e83bc8b14c97170833a5af721e58ff746d61317 (patch) | |
| tree | 63150120c3a66e3f0c80ffd32e21a7f0f9a95860 | |
| parent | ab2637af8b82f13be8ac38a800368bce6bbd10e5 (diff) | |
Cleanup a bit
| -rw-r--r-- | src/Invariants.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 9390436c..fec6b2ed 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -9,7 +9,6 @@ module Subst = Substitute module A = CfimAst module L = Logging open InterpreterUtils -open Errors let debug_invariants : bool ref = ref false @@ -404,7 +403,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | Abstract (V.ASharedLoan (_, sv, _)) -> assert (sv.V.ty = ref_ty) | _ -> failwith "Inconsistent context") - | V.MutBorrow (bid, bv), T.Mut -> + | V.MutBorrow (_, bv), T.Mut -> assert ( (* Check that the borrowed value has the proper type *) bv.V.ty = ref_ty) @@ -478,7 +477,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.ABottom, _ -> (* Nothing to check *) () | V.ABorrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with - | V.AMutBorrow (bid, av), T.Mut -> + | V.AMutBorrow (_, av), T.Mut -> (* Check that the child value has the proper type *) assert (av.V.ty = ref_ty) | V.ASharedBorrow bid, T.Shared -> ( |