diff options
| -rw-r--r-- | src/Interpreter.ml | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 5278cfdd..90df16ed 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -935,6 +935,11 @@ let rec access_projection (access : projection_access) (env : C.env) (* Function to (eventually) update the value we find *) (update : V.typed_value -> V.typed_value) (p : E.projection) (v : V.typed_value) : (C.env * updated_read_value) path_access_result = + (* Debug *) + L.log#ldebug + (lazy + ("access_projection:\n" ^ "p: " ^ E.show_projection p ^ "\nv.ty: " + ^ T.show_ety v.V.ty)); (* For looking up/updating shared loans *) let ek : exploration_kind = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } @@ -957,7 +962,7 @@ let rec access_projection (access : projection_access) (env : C.env) | _ -> failwith "Unreachable"); (* Actually project *) let fv = T.FieldId.nth adt.field_values field_id in - match access_projection access env update p fv with + match access_projection access env update p' fv with | Error err -> Error err | Ok (env1, res) -> (* Update the field value *) @@ -972,7 +977,7 @@ let rec access_projection (access : projection_access) (env : C.env) assert (arity = T.FieldId.length values); let fv = T.FieldId.nth values field_id in (* Project *) - match access_projection access env update p fv with + match access_projection access env update p' fv with | Error err -> Error err | Ok (env1, res) -> (* Update the field value *) @@ -1217,6 +1222,11 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) : let expand_bottom_value (config : C.config) (access : access_kind) (tyctx : T.type_def T.TypeDefId.vector) (p : E.place) (remaining_pes : int) (pe : E.projection_elem) (ty : T.ety) (env : C.env) : C.env = + (* Debugging *) + L.log#ldebug + (lazy + ("expand_bottom_value:\n" ^ "pe: " ^ E.show_projection_elem pe ^ "\n" + ^ "ty: " ^ T.show_ety ty)); (* Prepare the update: we need to take the proper prefix of the place during whose evaluation we got stuck *) let projection' = @@ -1246,10 +1256,7 @@ let expand_bottom_value (config : C.config) (access : access_kind) compute_expanded_bottom_tuple_value tys | _ -> failwith - ("Unreachable: " - ^ Print.CfimAst.projection_elem_variant_name pe - ^ ", " - ^ Print.Types.ty_variant_name ty) + ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_ety ty) in (* Update the environment by inserting the expanded value at the proper place *) match write_place config access p' nv env with |