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/SymbolicToPure.ml | |
| parent | 98677400fc27087ab4443094fb94a95412515422 (diff) | |
Introduce AEndedSharedBorrow so as not to introduce ABottom when
ending shared aborrows
Diffstat (limited to '')
| -rw-r--r-- | src/SymbolicToPure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 1985bfd3..80d08ac4 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -678,7 +678,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented - | AProjSharedBorrow _ -> + | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Ignore *) None @@ -784,7 +784,7 @@ and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) : | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented - | AProjSharedBorrow _ -> + | AEndedSharedBorrow | AProjSharedBorrow _ -> (* Ignore *) (ctx, None) |