diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index e46d46183..a2949b285 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -108,9 +108,16 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s let underlying_node = Node.underlying_node node in NodePrinter.start_session ~pp_name underlying_node ; let left, right, result = match op with `Join lrr | `Widen (_, lrr) -> lrr in + let pp_right f = + if phys_equal right left then F.pp_print_string f "= LEFT" else Domain.pp f right + in + let pp_result f = + if phys_equal result left then F.pp_print_string f "= LEFT" + else if phys_equal result right then F.pp_print_string f "= RIGHT" + else Domain.pp f result + in L.d_strln - ( Format.asprintf "LEFT: %a@.RIGHT: %a@.RESULT: %a@." Domain.pp left Domain.pp right - Domain.pp result + ( Format.asprintf "LEFT: %a@.RIGHT: %t@.RESULT: %t@." Domain.pp left pp_right pp_result |> Escape.escape_xml ) ; NodePrinter.finish_session underlying_node @@ -143,9 +150,13 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s in if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly then ( + let pp_post f = + if phys_equal astate_post pre then F.pp_print_string f "= PRE" + else Domain.pp f astate_post + in L.d_strln - ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre - (Instrs.pp Pp.text) instrs Domain.pp astate_post + ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %t@]@." Domain.pp pre + (Instrs.pp Pp.text) instrs pp_post |> Escape.escape_xml ) ; NodePrinter.finish_session (Node.underlying_node node) ) ; InvariantMap.add node_id {State.pre; post= astate_post; visit_count} inv_map diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index b2c87820d..62065517c 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -33,9 +33,13 @@ struct if Config.write_html then ( let underyling_node = CFG.Node.underlying_node node in NodePrinter.start_session ~pp_name:(pp_session_name node) underyling_node ; + let pp_post f = + if phys_equal post pre then Format.pp_print_string f "= PRE" + else TransferFunctions.Domain.pp f post + in L.d_strln - ( Format.asprintf "PRE: %a@.INSTR: %a@.POST: %a@." TransferFunctions.Domain.pp pre - HilInstr.pp hil_instr TransferFunctions.Domain.pp post + ( Format.asprintf "PRE: %a@.INSTR: %a@.POST: %t@." TransferFunctions.Domain.pp pre + HilInstr.pp hil_instr pp_post |> Escape.escape_xml ) ; NodePrinter.finish_session underyling_node )