diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Print.ml | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/Print.ml b/src/Print.ml index f714e847..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 @@ -390,7 +393,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 @@ -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 @@ -973,6 +986,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 |