diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index a493c3bb7..a1cbc2149 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -622,7 +622,7 @@ module Report = struct
-> Tenv.t
-> Typ.IntegerWidths.t
-> CFG.t
- -> Analyzer.invariant_map
+ -> invariant_map
-> Checks.t
-> CFG.Node.t
-> Checks.t =
@@ -636,14 +636,14 @@ module Report = struct
let check_proc :
- Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> Analyzer.invariant_map -> Checks.t =
+ Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> invariant_map -> Checks.t =
fun pdesc tenv integer_type_widths cfg inv_map ->
CFG.fold_nodes cfg
~f:(check_node pdesc tenv integer_type_widths cfg inv_map)
~init:Checks.empty
- let report_errors : Tenv.t -> Summary.t -> Checks.t -> PO.ConditionSet.t =
+ let report_errors : Tenv.t -> Summary.t -> Checks.t -> unit =
fun tenv summary {cond_set; unused_branches; unreachable_statements} ->
UnusedBranches.report tenv summary unused_branches ;
UnreachableStatements.report summary unreachable_statements ;
@@ -657,12 +657,14 @@ module Report = struct
in
Reporting.log_error summary ~loc:location ~ltr:trace issue_type (description ~markup:true)
in
- PO.ConditionSet.check_all ~report cond_set
+ PO.ConditionSet.report_errors ~report cond_set
- let forget_locs = PO.ConditionSet.forget_locs
-
- let for_summary = PO.ConditionSet.for_summary
+ let for_summary ~forget_locs
+ Checks.({ cond_set
+ ; unused_branches= _ (* intra-procedural *)
+ ; unreachable_statements= _ (* intra-procedural *) }) =
+ PO.ConditionSet.for_summary ~forget_locs cond_set
end
let extract_pre = Analyzer.extract_pre
@@ -694,11 +696,10 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
let pp_name f = F.pp_print_string f "bufferoverrun check" in
NodePrinter.start_session ~pp_name underlying_exit_node ;
let summary =
+ let checks = Report.check_proc proc_desc tenv integer_type_widths cfg inv_map in
+ Report.report_errors tenv summary checks ;
let locals = get_local_decls proc_desc in
- let cond_set =
- Report.check_proc proc_desc tenv integer_type_widths cfg inv_map
- |> Report.report_errors tenv summary |> Report.forget_locs locals |> Report.for_summary
- in
+ let cond_set = Report.for_summary ~forget_locs:locals checks in
let exit_mem =
extract_post (CFG.Node.id exit_node) inv_map
|> Option.value ~default:Bottom |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 1803d366e..d6e72cb88 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -794,26 +794,35 @@ module ConditionWithTrace = struct
{report_issue_type; propagate}
- let report ~report ((cwt, checked) as default) =
+ let report_errors ~report (cwt, checked) =
match checked.report_issue_type with
| NotIssue | SymbolicIssue ->
- default
+ ()
| Issue issue_type ->
- report cwt.cond cwt.trace issue_type ;
- if checked.propagate then ({cwt with reported= Some (Reported.make issue_type)}, checked)
- else default
-
+ report cwt.cond cwt.trace issue_type
- let forget_locs locs cwt = {cwt with cond= Condition.forget_locs locs cwt.cond}
- let for_summary cwt = {cwt with trace= ConditionTrace.for_summary cwt.trace}
+ let for_summary ~forget_locs = function
+ | _, {propagate= false} | _, {report_issue_type= NotIssue} ->
+ None
+ | {cond; trace; reported; reachability}, {report_issue_type} ->
+ let reported =
+ match report_issue_type with
+ | NotIssue ->
+ assert false
+ | SymbolicIssue ->
+ reported
+ | Issue issue_type ->
+ Some (Reported.make issue_type)
+ in
+ let cond = Condition.forget_locs forget_locs cond in
+ let trace = ConditionTrace.for_summary trace in
+ Some {cond; trace; reported; reachability}
end
module ConditionSet = struct
type 'cond_trace t0 = 'cond_trace ConditionWithTrace.t0 list
- type t = ConditionTrace.intra_cond_trace t0
-
type checked_t = (ConditionTrace.intra_cond_trace ConditionWithTrace.t0 * checked_condition) list
type summary_t = unit t0
@@ -923,10 +932,12 @@ module ConditionSet = struct
List.fold condset ~f:subst_add_cwt ~init:[]
- let check_all ~report condset =
- condset
- |> List.map ~f:(ConditionWithTrace.report ~report)
- |> List.filter_map ~f:(fun (cwt, {propagate}) -> Option.some_if propagate cwt)
+ let report_errors ~report condset =
+ List.iter condset ~f:(ConditionWithTrace.report_errors ~report)
+
+
+ let for_summary ~forget_locs condset =
+ List.filter_map condset ~f:(ConditionWithTrace.for_summary ~forget_locs)
let pp_summary : F.formatter -> _ t0 -> unit =
@@ -946,14 +957,6 @@ module ConditionSet = struct
F.fprintf fmt "Safety conditions:@;@[<hov 2>{ %a }@]"
(IList.pp_print_list ~max:30 ~pp_sep pp_elem)
condset
-
-
- let forget_locs : AbsLoc.PowLoc.t -> 'a t0 -> 'a t0 =
- fun locs x -> List.map x ~f:(ConditionWithTrace.forget_locs locs)
-
-
- let for_summary : _ t0 -> summary_t =
- fun condset -> List.map condset ~f:ConditionWithTrace.for_summary
end
let description ~markup cond trace =
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
index 6b8a7b7b0..347a01b2a 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
@@ -23,8 +23,6 @@ module ConditionTrace : sig
end
module ConditionSet : sig
- type t
-
type checked_t
type summary_t
@@ -81,12 +79,10 @@ module ConditionSet : sig
-> Location.t
-> checked_t
- val check_all : report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> t
- (** Check the conditions, call [report] on those that trigger an issue, returns those that needs to be propagated to callers. *)
-
- val for_summary : t -> summary_t
+ val report_errors :
+ report:(Condition.t -> ConditionTrace.t -> IssueType.t -> unit) -> checked_t -> unit
- val forget_locs : AbsLoc.PowLoc.t -> t -> t
+ val for_summary : forget_locs:AbsLoc.PowLoc.t -> checked_t -> summary_t
end
val description : markup:bool -> Condition.t -> ConditionTrace.t -> string