diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index d0dbcf2b6..605d83a77 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -88,8 +88,7 @@ struct module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig)) - let compute_post ?(debug= Config.debug_mode) proc_data ~initial = + let compute_post proc_data ~initial = let initial' = (initial, IdAccessPathMapDomain.empty) in - Option.map ~f:fst (Interpreter.compute_post ~debug proc_data ~initial:initial') - + Option.map ~f:fst (Interpreter.compute_post ~debug:false proc_data ~initial:initial') end diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index e6112df79..8a6fda889 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -41,7 +41,7 @@ module MakeAbstractInterpreter module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (DefaultConfig)) val compute_post : - ?debug:bool -> Interpreter.TransferFunctions.extras ProcData.t + Interpreter.TransferFunctions.extras ProcData.t -> initial:MakeTransferFunctions(CFG).Domain.astate -> MakeTransferFunctions(CFG).Domain.astate option (** compute and return the postcondition for the given procedure starting from [initial]. If diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml index 9e3c7caba..14bf99c34 100644 --- a/infer/src/checkers/NullabilityCheck.ml +++ b/infer/src/checkers/NullabilityCheck.ml @@ -135,6 +135,5 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (Transf let checker {Callbacks.summary; proc_desc; tenv} = let initial = Domain.empty in let proc_data = ProcData.make proc_desc tenv summary in - ignore (Analyzer.compute_post proc_data ~initial ~debug:false) ; + ignore (Analyzer.compute_post proc_data ~initial) ; summary - diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index e1fc32d20..d08bb70ea 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -185,7 +185,7 @@ let checker {Callbacks.summary; proc_desc; tenv} = (* Assume all fields are not null in the beginning *) let initial = Domain.empty in let proc_data = ProcData.make_default proc_desc tenv in - match Analyzer.compute_post proc_data ~initial ~debug:false with + match Analyzer.compute_post proc_data ~initial with | Some post -> report post proc_data ; summary | None -> diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index b8f306db2..954a1bb67 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -1144,7 +1144,7 @@ let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = in {RacerDDomain.empty with ownership; threads} in - match Analyzer.compute_post proc_data ~initial ~debug:false with + match Analyzer.compute_post proc_data ~initial with | Some {threads; locks; accesses; ownership; attribute_map} -> let return_var_ap = AccessPath.of_pvar @@ -1883,4 +1883,3 @@ let file_analysis {Callbacks.procedures} = else (module MayAliasQuotientedAccessListMap) ) class_env)) (aggregate_by_class procedures) - diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 19b4b3323..66243bc9b 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -118,7 +118,7 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary = in let extras = FormalMap.make proc_desc in let proc_data = ProcData.make proc_desc tenv extras in - match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial ~debug:false with + match Analyzer.compute_post proc_data ~initial:ResourceLeakDomain.initial with | Some post -> (* 1(f) *) report post proc_data ; @@ -127,4 +127,3 @@ let checker {Callbacks.summary; proc_desc; tenv} : Specs.summary = L.(die InternalError) "Analyzer failed to compute post for %a" Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) -