diff --git a/infer/src/backend/Payloads.ml b/infer/src/backend/Payloads.ml index b0096eac1..3369341ef 100644 --- a/infer/src/backend/Payloads.ml +++ b/infer/src/backend/Payloads.ml @@ -15,7 +15,6 @@ type t = ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option ; class_loads: ClassLoadsDomain.summary option ; cost: CostDomain.summary option - ; impurity: ImpurityDomain.t option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho: LithoDomain.t option ; pulse: PulseSummary.t option @@ -44,7 +43,6 @@ let fields = ~buffer_overrun_checker:(fun f -> mk f "BufferOverrunChecker" BufferOverrunCheckerSummary.pp) ~class_loads:(fun f -> mk f "ClassLoads" ClassLoadsDomain.pp_summary) ~cost:(fun f -> mk f "Cost" CostDomain.pp_summary) - ~impurity:(fun f -> mk f "Impurity" ImpurityDomain.pp) ~litho:(fun f -> mk f "Litho" LithoDomain.pp) ~pulse:(fun f -> mk f "Pulse" PulseSummary.pp) ~purity:(fun f -> mk f "Purity" PurityDomain.pp_summary) @@ -70,7 +68,6 @@ let empty = ; buffer_overrun_checker= None ; class_loads= None ; cost= None - ; impurity= None ; lab_resource_leaks= None ; litho= None ; pulse= None diff --git a/infer/src/backend/Payloads.mli b/infer/src/backend/Payloads.mli index 764f4b5b1..48d2cf30a 100644 --- a/infer/src/backend/Payloads.mli +++ b/infer/src/backend/Payloads.mli @@ -20,7 +20,6 @@ include ; buffer_overrun_checker: BufferOverrunCheckerSummary.t option ; class_loads: ClassLoadsDomain.summary option ; cost: CostDomain.summary option - ; impurity: ImpurityDomain.t option ; lab_resource_leaks: ResourceLeakDomain.summary option ; litho: LithoDomain.t option ; pulse: PulseSummary.t option diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index e01f96611..8b559df35 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -16,12 +16,6 @@ let debug fmt = L.(debug Analysis Verbose fmt) (* An impurity analysis that relies on pulse to determine how the state changes *) -module Payload = SummaryPayload.Make (struct - type t = ImpurityDomain.t - - let field = Payloads.Fields.impurity -end) - let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractAddress.t list option = match List.fold2 ~init:(Some []) @@ -146,8 +140,7 @@ let checker ({Callbacks.summary} as callback) : Summary.t = let modified = extract_impurity (Summary.get_proc_desc summary) pre_post in ImpurityDomain.join acc modified ) in - report_errors summary modified ; - Payload.update_summary modified summary + report_errors summary modified ; summary | None -> debug "@\n\n[WARNING] Couldn't find any Pulse summary to extract impurity information." ; summary diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 446ce103b..a7a27fe41 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -29,17 +29,6 @@ let is_pure {modified_globals; modified_params} = ModifiedVarSet.is_empty modified_globals && ModifiedVarSet.is_empty modified_params -let pp fmt ({modified_globals; modified_params} as astate) = - if is_pure astate then F.fprintf fmt "@\n pure @\n" - else if ModifiedVarSet.is_empty modified_params then - F.fprintf fmt "@\n impure, modified globals :%a @\n" ModifiedVarSet.pp modified_globals - else if ModifiedVarSet.is_empty modified_globals then - F.fprintf fmt "@\n impure, modified params :%a @\n" ModifiedVarSet.pp modified_params - else - F.fprintf fmt "@\n impure, modified params :%a, modified globals :%a @\n" ModifiedVarSet.pp - modified_params ModifiedVarSet.pp modified_globals - - let pure = {modified_params= ModifiedVarSet.empty; modified_globals= ModifiedVarSet.empty} let join astate1 astate2 = diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 2dc89b743..8c8bca1c8 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -34,6 +34,4 @@ val add_to_errlog : -> Errlog.loc_trace_elem sexp_list -> Errlog.loc_trace_elem sexp_list -val pp : Format.formatter -> t -> unit - val join : t -> t -> t