diff options
| author | Son Ho | 2022-01-26 10:04:52 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-26 10:04:52 +0100 |
| commit | 14833cb33792703bf87c7e7d933687f289886294 (patch) | |
| tree | b7c18f894854372dbd318f9b5dd3b6c54696aa7e /src/InterpreterExpansion.ml | |
| parent | 144b660f7cfb8b65672f5872c05272a9caa0de78 (diff) | |
Add a meta-value in SharedBorrow to carry the shared value
Diffstat (limited to 'src/InterpreterExpansion.ml')
| -rw-r--r-- | src/InterpreterExpansion.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 69e12545..2dd36535 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -298,6 +298,8 @@ let expand_symbolic_value_shared_borrow (config : C.config) | _ -> failwith "Unexpected" else None in + (* The fresh symbolic value for the shared value *) + let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in (* Visitor to replace the projectors on borrows *) let obj = object (self) @@ -306,7 +308,8 @@ let expand_symbolic_value_shared_borrow (config : C.config) method! visit_Symbolic env sv = if same_symbolic_id sv original_sv then let bid = fresh_borrow () in - V.Borrow (V.SharedBorrow bid) + V.Borrow + (V.SharedBorrow (mk_typed_value_from_symbolic_value shared_sv, bid)) else super#visit_Symbolic env sv method! visit_Abs proj_regions abs = @@ -362,7 +365,6 @@ let expand_symbolic_value_shared_borrow (config : C.config) (* Finally, replace the projectors on loans *) let bids = !borrows in assert (not (V.BorrowId.Set.is_empty bids)); - let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in let see = V.SeSharedRef (bids, shared_sv) in let allow_reborrows = true in let ctx = |