diff options
| author | Son Ho | 2022-01-26 10:07:29 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-26 10:07:29 +0100 |
| commit | 534c70dc60ce26da3117395b916d1cabd4033abd (patch) | |
| tree | b1efd648f07dff4476d5a708ddf5170e3b302c2a | |
| parent | 14833cb33792703bf87c7e7d933687f289886294 (diff) | |
Implement the SharedBorrow case of SymbolicToPure.typed_value_to_rvalue
Diffstat (limited to '')
| -rw-r--r-- | src/SymbolicToPure.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index a77a64ca..e0ee557a 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -533,9 +533,6 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var = - function call - end abstraction - return - - TODO: we have a problem with shared borrows. I think the shared borrows - should carry the shared value as a meta-value. *) let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue = @@ -554,9 +551,10 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue | MutLoan _ -> failwith "Unreachable") | Borrow bc -> ( match bc with - | V.SharedBorrow _ -> - (* TODO: *) - raise Unimplemented + | V.SharedBorrow (mv, _) -> + (* The meta-value stored in the shared borrow was added especially + * for this case (because we can't use the borrow id for lookups) *) + (translate mv).value | V.InactivatedMutBorrow _ -> failwith "Unreachable" | V.MutBorrow (_, v) -> (* Borrows are the identity in the extraction *) |