diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 5739a8c83..cacc9e25a 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -662,7 +662,7 @@ module Report = struct L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ; L.(debug BufferOverrun Verbose) "@[Pre-state : @,%a" Dom.Mem.pp pre ; L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ; - L.(debug BufferOverrun Verbose) "@[@\n@\n%a" PO.ConditionSet.pp cond_set ; + L.(debug BufferOverrun Verbose) "@\n@\n@[%a" PO.ConditionSet.pp cond_set ; L.(debug BufferOverrun Verbose) "@]@\n" ; L.(debug BufferOverrun Verbose) "================================@\n@." diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 603041961..61d1b5b51 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -851,9 +851,9 @@ module ConditionSet = struct let pp : Format.formatter -> t -> unit = fun fmt condset -> - let pp_sep fmt () = F.fprintf fmt ",@," in + let pp_sep fmt () = F.fprintf fmt ",@;" in F.fprintf fmt "Safety conditions:@;@[{ %a }@]" - (F.pp_print_list ~pp_sep ConditionWithTrace.pp) + (IList.pp_print_list ~max:30 ~pp_sep ConditionWithTrace.pp) condset diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index a3a370a58..23bd5b81c 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -171,3 +171,17 @@ let remove_first = if f hd then Some (List.rev_append rev_front tl) else aux tl ~f (hd :: rev_front) in fun list ~f -> aux list ~f [] + + +let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf = + let rec aux n = function + | [] -> + () + | v :: rest -> + if n >= max then Format.fprintf ppf " ..." + else ( + pp_sep ppf () ; + pp_v ppf v ; + aux (n + 1) rest ) + in + function [] -> () | [v] -> pp_v ppf v | v :: rest -> pp_v ppf v ; aux 1 rest diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli index 9c4e9be9e..ed01e0a50 100644 --- a/infer/src/istd/IList.mli +++ b/infer/src/istd/IList.mli @@ -41,3 +41,11 @@ val opt_cons : 'a option -> 'a list -> 'a list (** [opt_cons None l] returns [l]. [opt_cons (Some x) l] returns [x :: l]*) val remove_first : 'a list -> f:('a -> bool) -> 'a list option + +val pp_print_list : + max:int + -> ?pp_sep:(Format.formatter -> unit -> unit) + -> (Format.formatter -> 'a -> unit) + -> Format.formatter + -> 'a list + -> unit