From dbbb01630190d999d3932fabd8a181b4f826f64f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 11:00:05 +0100
Subject: Improve logging and introduce eval_operands_prepare

---
 src/Print.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src/Print.ml')

diff --git a/src/Print.ml b/src/Print.ml
index f714e847..ce31338d 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -390,7 +390,7 @@ module Values = struct
         ^ typed_avalue_to_string fmt av
         ^ ")"
     | AEndedIgnoredMutLoan ml ->
-        "@ended_ignored_mut_borrow{ given_back="
+        "@ended_ignored_mut_loan{ given_back="
         ^ typed_avalue_to_string fmt ml.given_back
         ^ "; child: "
         ^ typed_avalue_to_string fmt ml.child
@@ -973,6 +973,12 @@ module EvalCtxCfimAst = struct
     let fmt = PC.ctx_to_rtype_formatter fmt in
     PT.rty_to_string fmt t
 
+  let symbolic_value_to_string (ctx : C.eval_ctx) (sv : V.symbolic_value) :
+      string =
+    let fmt = PC.eval_ctx_to_ctx_formatter ctx in
+    let fmt = PC.ctx_to_rtype_formatter fmt in
+    PV.symbolic_value_to_string fmt sv
+
   let typed_value_to_string (ctx : C.eval_ctx) (v : V.typed_value) : string =
     let fmt = PC.eval_ctx_to_ctx_formatter ctx in
     PV.typed_value_to_string fmt v
-- 
cgit v1.2.3


From 8917bf6aca4465873e7e7642719c70789d97590c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 12:39:58 +0100
Subject: Add an optional borrow identifier to AIgnoredMutBorrow, introduce the
 AEndedIgnoredMutBorrow variant and fix a couple of bugs

---
 src/Print.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'src/Print.ml')

diff --git a/src/Print.ml b/src/Print.ml
index ce31338d..5ae722b9 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -7,6 +7,9 @@ module A = CfimAst
 module C = Contexts
 module M = Modules
 
+let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
+  match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
+
 (** Pretty-printing for types *)
 module Types = struct
   let type_var_to_string (tv : T.type_var) : string = tv.name
@@ -406,8 +409,18 @@ module Values = struct
         ^ typed_avalue_to_string fmt av
         ^ ")"
     | ASharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
-    | AIgnoredMutBorrow av ->
-        "@ignored_mut_borrow(" ^ typed_avalue_to_string fmt av ^ ")"
+    | AIgnoredMutBorrow (opt_bid, av) ->
+        "@ignored_mut_borrow("
+        ^ option_to_string V.BorrowId.to_string opt_bid
+        ^ ", "
+        ^ typed_avalue_to_string fmt av
+        ^ ")"
+    | AEndedIgnoredMutBorrow { given_back_loans_proj; child } ->
+        "@ended_ignored_mut_borrow{ given_back_loans_proj="
+        ^ typed_avalue_to_string fmt given_back_loans_proj
+        ^ "; child="
+        ^ typed_avalue_to_string fmt child
+        ^ ")"
     | AProjSharedBorrow sb ->
         "@ignored_shared_borrow("
         ^ abstract_shared_borrows_to_string fmt sb
-- 
cgit v1.2.3