summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-30 09:55:43 +0100
committerSon Ho2021-11-30 09:55:43 +0100
commitf5e1f3338acb9e6282b5c6d60aa10ef81172a129 (patch)
tree27b7b663bd271c101779ed6eaf42d70971c2d36d
parentdf564c774866c3aa7316a336b3f48b7cfdeefdcf (diff)
Fix another bug
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 068c175c..e24f565e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1763,7 +1763,10 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
let ctx2, v = prepare_rplace config access p ctx in
(* Compute the rvalue - simply a shared borrow with a fresh id *)
let ctx3, bid = C.fresh_borrow_id ctx2 in
- let rv_ty = T.Ref (T.Erased, v.ty, Shared) in
+ (* Note that the reference is *mutable* if we do a two-phase borrow *)
+ let rv_ty =
+ T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
+ in
let bc =
if bkind = E.Shared then V.SharedBorrow bid
else V.InactivatedMutBorrow bid