diff options
| author | Son Ho | 2022-01-27 11:43:59 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-27 11:43:59 +0100 |
| commit | b2d5671516b60ae83778b26867a8e5b6060f519d (patch) | |
| tree | 90aefb82bb32da8671a54543300a0a1155c2d8d7 /src/Invariants.ml | |
| parent | 98677400fc27087ab4443094fb94a95412515422 (diff) | |
Introduce AEndedSharedBorrow so as not to introduce ABottom when
ending shared aborrows
Diffstat (limited to '')
| -rw-r--r-- | src/Invariants.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Invariants.ml b/src/Invariants.ml index 522f2ffa..fe1b5e82 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -257,7 +257,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = | V.AIgnoredMutBorrow (Some bid, _) -> register_ignored_borrow Mut bid | V.AIgnoredMutBorrow (None, _) | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _ - | V.AProjSharedBorrow _ -> + | V.AEndedSharedBorrow | V.AProjSharedBorrow _ -> (* Do nothing *) () in @@ -361,7 +361,7 @@ let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = let info = match bc with | V.AMutBorrow (_, _, _) -> set_outer_mut info - | V.ASharedBorrow _ -> set_outer_shared info + | V.ASharedBorrow _ | V.AEndedSharedBorrow -> set_outer_shared info | V.AIgnoredMutBorrow _ | V.AEndedMutBorrow _ | V.AEndedIgnoredMutBorrow _ -> set_outer_mut info |