diff options
author | Son Ho | 2022-01-07 11:00:05 +0100 |
---|---|---|
committer | Son Ho | 2022-01-07 11:00:05 +0100 |
commit | dbbb01630190d999d3932fabd8a181b4f826f64f (patch) | |
tree | 0011dda53aaeb88919b3354a9be5b21dca2aa45a /src/InterpreterExpansion.ml | |
parent | a310c6036568d8f62e09804c67064686d106afd4 (diff) |
Improve logging and introduce eval_operands_prepare
Diffstat (limited to 'src/InterpreterExpansion.ml')
-rw-r--r-- | src/InterpreterExpansion.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 345c3df3..aebcda3c 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -16,6 +16,9 @@ open InterpreterUtils open InterpreterProjectors open InterpreterBorrows +(** The local logger *) +let log = L.expansion_log + (** Projector kind *) type proj_kind = LoanProj | BorrowProj @@ -366,6 +369,8 @@ let expand_symbolic_value_borrow (config : C.config) let expand_symbolic_value_no_branching (config : C.config) (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = + (* Remember the initial context for printing purposes *) + let ctx0 = ctx in (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) let original_sv = sp in @@ -424,6 +429,14 @@ let expand_symbolic_value_no_branching (config : C.config) failwith ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) in + (* Debugging *) + (* Debug *) + log#ldebug + (lazy + ("expand_symbolic_value: " + ^ symbolic_value_to_string ctx0 sp + ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); (* Return *) |