summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml14
1 files changed, 10 insertions, 4 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 66668b1f..be0a1acf 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -950,8 +950,8 @@ let rec access_projection (access : projection_access) (env : C.env)
(* Debug *)
L.log#ldebug
(lazy
- ("access_projection:\n" ^ "p: " ^ E.show_projection p ^ "\nv.ty: "
- ^ T.show_ety v.V.ty));
+ ("access_projection:\n" ^ "- p: " ^ E.show_projection p ^ "\n- v: "
+ ^ V.show_typed_value v));
(* For looking up/updating shared loans *)
let ek : exploration_kind =
{ enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -1084,7 +1084,11 @@ let rec access_projection (access : projection_access) (env : C.env)
else Error (FailSharedLoan bids))
| ( _,
( V.Concrete _ | V.Adt _ | V.Tuple _ | V.Bottom | V.Assumed _
- | V.Borrow _ ) ) ->
+ | V.Borrow _ ) ) as r ->
+ let pe, v = r in
+ let pe = "- pe: " ^ E.show_projection_elem pe in
+ let v = "- v:\n" ^ V.show_value v in
+ L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v);
failwith "Inconsistent projection")
(** Generic function to access (read/write) the value at a given place.
@@ -2106,7 +2110,9 @@ let eval_box_deref_mut_or_shared (config : C.config)
assert (input_ty = boxed_ty));
(* Borrow the boxed value *)
- let p = { E.var_id = input_var.V.index; projection = [ E.DerefBox ] } in
+ let p =
+ { E.var_id = input_var.V.index; projection = [ E.Deref; E.DerefBox ] }
+ in
let borrow_kind = if is_mut then E.Mut else E.Shared in
let rv = E.Ref (p, borrow_kind) in
match eval_rvalue config ctx rv with