diff options
Diffstat (limited to 'src/Invariants.ml')
| -rw-r--r-- | src/Invariants.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index ee58a1a3..2d26404d 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -595,13 +595,22 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.ASymbolic aproj, ty -> ( let ty1 = Subst.erase_regions ty in match aproj with - | V.AProjLoans (sv, _) | V.AProjBorrows (sv, _) -> + | V.AProjLoans (sv, _) -> let ty2 = Subst.erase_regions sv.V.sv_ty in assert (ty1 = ty2); (* Also check that the symbolic values contain regions of interest - * otherwise they should have been reduced to `_` *) let abs = Option.get info in + log#ldebug (lazy (symbolic_value_to_string ctx sv)); assert (ty_has_regions_in_set abs.regions sv.V.sv_ty) + | V.AProjBorrows (sv, proj_ty) -> + let ty2 = Subst.erase_regions sv.V.sv_ty in + assert (ty1 = ty2); + (* Also check that the symbolic values contain regions of interest - + * otherwise they should have been reduced to `_` *) + let abs = Option.get info in + log#ldebug (lazy (symbolic_value_to_string ctx sv)); + assert (ty_has_regions_in_set abs.regions proj_ty) | V.AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> |