[inferbo] Print reachability of proof obligation in debug mode

Reviewed By: mbouaziz

Differential Revision: D13781124

fbshipit-source-id: f6b1138db

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -986,6 +986,8 @@ module Reachability = struct
 
   let equal = M.equal
 
+  let pp = M.pp
+
   (* It keeps only symbolic pruned values, because non-symbolic ones are useless to see the
      reachability. *)
   let add v x = if PrunedVal.is_symbolic v then M.add v x else x

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -708,10 +708,16 @@ module ConditionWithTrace = struct
     {cond; trace; reported= None; reachability= Dom.Reachability.make latest_prune}
 
 
-  let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace
+  let pp fmt {cond; trace; reachability} =
+    F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace ;
+    if Config.bo_debug >= 3 then
+      F.fprintf fmt " reachable when %a" Dom.Reachability.pp reachability
+
 
-  let pp_summary fmt {cond; trace} =
+  let pp_summary fmt {cond; trace; reachability} =
-    F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp_summary trace
+    F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp_summary trace ;
+    if Config.bo_debug >= 3 then
+      F.fprintf fmt " reachable when %a" Dom.Reachability.pp reachability
 
 
   let have_same_bounds {cond= cond1} {cond= cond2} = Condition.equal cond1 cond2