diff --git a/infer/src/checkers/Trace.ml b/infer/src/checkers/Trace.ml index 23e03834d..9d76d7bef 100644 --- a/infer/src/checkers/Trace.ml +++ b/infer/src/checkers/Trace.ml @@ -188,7 +188,10 @@ module Make (Spec : Spec) = struct {known; footprint} let pp fmt {known; footprint} = - F.fprintf fmt "Known: %a@\nFootprint: %a@\n" Known.pp known Footprint.pp footprint + if Known.is_empty known then + if Footprint.is_empty footprint then F.fprintf fmt "{}" + else F.fprintf fmt "Footprint(%a)" Footprint.pp footprint + else F.fprintf fmt "%a + Footprint(%a)" Known.pp known Footprint.pp footprint let empty = {known= Known.empty; footprint= Footprint.empty} diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index aee840962..d2f174f21 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -329,4 +329,11 @@ module Make (TraceDomain : AbstractDomain.WithBottom) = struct let pp fmt base_tree = BaseMap.pp ~pp_value:pp_node fmt base_tree end -module PathSet = Make (AbstractDomain.BooleanOr) +module PathSet = struct + include Make (AbstractDomain.BooleanOr) + + (* print as a set of paths rather than a map of paths to bools *) + let pp fmt tree = + let collect_path acc access_path (is_mem, _) = if is_mem then access_path :: acc else acc in + fold collect_path tree [] |> PrettyPrintable.pp_collection ~pp_item:AccessPath.Abs.pp fmt +end