diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 1f7ab8509..e34b85d44 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -155,9 +155,9 @@ let extract_impurity tenv pdesc (exec_state : ExecutionDomain.t) : ImpurityDomai in let modified_globals = get_modified_globals pre_heap post post_stack in let skipped_calls = - AbductiveDomain.get_skipped_calls astate - |> SkippedCalls.filter (fun proc_name _ -> - Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) + SkippedCalls.filter + (fun proc_name _ -> Purity.should_report proc_name && not (is_modeled_pure tenv proc_name)) + astate.AbductiveDomain.skipped_calls in {modified_globals; modified_params; skipped_calls; exited} diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index bce78a3b3..cec65e66d 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -416,5 +416,3 @@ let of_post pdesc astate = let get_pre {pre} = (pre :> BaseDomain.t) let get_post {post} = (post :> BaseDomain.t) - -let get_skipped_calls {skipped_calls} = skipped_calls diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 1997b7f29..d277e09aa 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -67,8 +67,6 @@ val get_pre : t -> BaseDomain.t val get_post : t -> BaseDomain.t -val get_skipped_calls : t -> SkippedCalls.t - (** stack operations like {!BaseStack} but that also take care of propagating facts to the precondition *) module Stack : sig