diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 14 |
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 |