From a65176de2247aff56fc33c8a09b6c123fbba9aaa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 12 Mar 2020 06:06:51 -0700 Subject: [PATCH] [pulse] Print SkippedCalls Summary: Let's also print skipped calls in `pp` to ease debugging both for summary and intermediate steps. Reviewed By: jvillard Differential Revision: D20417852 fbshipit-source-id: 7da03ae81 --- infer/src/pulse/PulseAbductiveDomain.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 6e28d307b..5a04e84e7 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -95,7 +95,10 @@ let get_post {post} = (post :> BaseDomain.t) let get_skipped_calls {skipped_calls} = skipped_calls -let pp f {post; pre} = F.fprintf f "@[%a@;PRE=[%a]@]" Domain.pp post PreDomain.pp pre +let pp f {post; pre; skipped_calls} = + F.fprintf f "@[%a@;PRE=[%a]@;skipped_calls=%a@]" Domain.pp post PreDomain.pp pre + SkippedCalls.pp skipped_calls + let leq ~lhs ~rhs = SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls @@ -523,9 +526,10 @@ module PrePost = struct ; rev_subst= AddressMap.add addr_caller addr_callee call_state.rev_subst } ) - let pp f {pre; post} = + let pp f {pre; post; skipped_calls} = F.fprintf f "PRE:@\n @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ; - F.fprintf f "POST:@\n @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) + F.fprintf f "POST:@\n @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ; + F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls (* {3 reading the pre from the current state} *)