diff --git a/infer/src/pulse/PulseCallOperations.ml b/infer/src/pulse/PulseCallOperations.ml index 8635a9a004..4e544b340e 100644 --- a/infer/src/pulse/PulseCallOperations.ml +++ b/infer/src/pulse/PulseCallOperations.ml @@ -527,7 +527,9 @@ let call_aux disjunct_limit ({InterproceduralAnalysis.tenv} as analysis_data) pa (not path.PathContext.is_non_disj) && ( Option.exists disjunct_limit ~f:(fun limit -> List.length posts >= limit) || (should_keep_at_most_one_disjunct && not (List.is_empty posts)) ) - then (posts, contradiction) + then ( + L.d_printfln "disjunct limit reached, stop applying callee pre/posts" ; + (posts, contradiction) ) else ( (* apply one pre/post spec, check for timeouts in-between each pre/post spec from the callee *) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 04197ceb00..776baaa9d8 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -74,7 +74,7 @@ let pp_header kind fmt = function | AbortProgram _ -> Pp.with_color kind Red F.pp_print_string fmt "AbortProgram" | ContinueProgram _ -> - () + F.pp_print_string fmt "ContinueProgram" | ExceptionRaised _ -> Pp.with_color kind Orange F.pp_print_string fmt "ExceptionRaised" | ExitProgram _ -> diff --git a/infer/src/pulse/PulseResult.ml b/infer/src/pulse/PulseResult.ml index f4b49bb92c..e4e1893d91 100644 --- a/infer/src/pulse/PulseResult.ml +++ b/infer/src/pulse/PulseResult.ml @@ -6,10 +6,20 @@ *) open! IStd +module F = Format module L = Logging type ('ok, 'err) t = Ok of 'ok | Recoverable of 'ok * 'err list | FatalError of 'err * 'err list +let pp pp_ok pp_err fmt = function + | Ok ok -> + F.fprintf fmt "Ok (%a)" pp_ok ok + | Recoverable (ok, errs) -> + F.fprintf fmt "Recoverable (%a, [%a])" pp_ok ok (Pp.comma_seq pp_err) errs + | FatalError (err, errs) -> + F.fprintf fmt "FatalError (%a, [%a])" pp_err err (Pp.comma_seq pp_err) errs + + let append_errors errors result = if List.is_empty errors then result else diff --git a/infer/src/pulse/PulseResult.mli b/infer/src/pulse/PulseResult.mli index 724fdd0e86..571d1ebb6e 100644 --- a/infer/src/pulse/PulseResult.mli +++ b/infer/src/pulse/PulseResult.mli @@ -6,6 +6,7 @@ *) open! IStd +module F = Format [@@@warning "-unused-value-declaration"] @@ -13,6 +14,13 @@ open! IStd there's no point continuing the execution. *) type ('ok, 'err) t = Ok of 'ok | Recoverable of 'ok * 'err list | FatalError of 'err * 'err list +val pp : + (F.formatter -> 'ok -> unit) + -> (F.formatter -> 'err -> unit) + -> F.formatter + -> ('ok, 'err) t + -> unit + val append_errors : 'err list -> ('ok, 'err) t -> ('ok, 'err) t (** adds the given error list to the result, possibly changing an [Ok] result into a [Recoverable] one in the process *)