summaryrefslogtreecommitdiff
path: root/src/InterpreterPaths.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-07 13:55:16 +0100
committerSon Ho2022-01-07 13:55:16 +0100
commit2ee5357216cc5a620dbe6d091b0081d419951a4e (patch)
tree2d90296e1e4310d7c71ccaf6fc75b21475c8a3f5 /src/InterpreterPaths.ml
parente2d71a7b813ed2fe86800f6638c4cd941991aaac (diff)
Make more modifications to logging
Diffstat (limited to '')
-rw-r--r--src/InterpreterPaths.ml11
1 files changed, 7 insertions, 4 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 07c615a0..491e4c21 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -12,6 +12,9 @@ open InterpreterBorrowsCore
open InterpreterBorrows
open InterpreterExpansion
+(** The local logger *)
+let log = L.paths_log
+
(** Paths *)
(** When we fail reading from or writing to a path, it might be because we
@@ -76,7 +79,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
let nv = update v in
(* Type checking *)
if nv.ty <> v.ty then (
- L.log#lerror
+ log#lerror
(lazy
("Not the same type:\n- nv.ty: " ^ T.show_ety nv.ty ^ "\n- v.ty: "
^ T.show_ety v.ty));
@@ -244,7 +247,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
let pe = "- pe: " ^ E.show_projection_elem pe in
let v = "- v:\n" ^ V.show_value v in
let ty = "- ty:\n" ^ T.show_ety ty in
- L.log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
+ log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
failwith "Inconsistent projection")
(** Generic function to access (read/write) the value at a given place.
@@ -314,7 +317,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
^ C.show_env ctx1.env ^ "\n\nOld environment:\n"
^ C.show_env ctx.env
in
- L.log#serror msg;
+ log#serror msg;
failwith "Unexpected environment update");
Ok read_value
@@ -402,7 +405,7 @@ let expand_bottom_value_from_projection (config : C.config)
(access : access_kind) (p : E.place) (remaining_pes : int)
(pe : E.projection_elem) (ty : T.ety) (ctx : C.eval_ctx) : C.eval_ctx =
(* Debugging *)
- L.log#ldebug
+ log#ldebug
(lazy
("expand_bottom_value_from_projection:\n" ^ "pe: "
^ E.show_projection_elem pe ^ "\n" ^ "ty: " ^ T.show_ety ty));