diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index a54ac6aab..7d211257c 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -93,11 +93,12 @@ struct end module MakeAbstractInterpreterWithConfig + (MakeAbstractInterpreter : AbstractInterpreter.Make) (HilConfig : HilConfig) (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) = struct - module Interpreter = AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG)) + module Interpreter = MakeAbstractInterpreter (Make (MakeTransferFunctions) (HilConfig) (CFG)) let compute_post ({ProcData.pdesc; tenv} as proc_data) ~initial = Preanal.do_preanalysis pdesc tenv ; @@ -116,4 +117,5 @@ struct Interpreter.compute_post ~pp_instr proc_data ~initial:initial' |> Option.map ~f:fst end -module MakeAbstractInterpreter = MakeAbstractInterpreterWithConfig (DefaultConfig) +module MakeAbstractInterpreter = + MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig) diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index 8ac331123..abb9eb352 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -35,6 +35,7 @@ end (** Wrapper around Interpreter to prevent clients from having to deal with IdAccessPathMapDomain *) module MakeAbstractInterpreterWithConfig + (MakeAbstractInterpreter : AbstractInterpreter.Make) (HilConfig : HilConfig) (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig @@ -54,5 +55,6 @@ module MakeAbstractInterpreter (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig include module type of - MakeAbstractInterpreterWithConfig (DefaultConfig) (CFG) (MakeTransferFunctions) + MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (DefaultConfig) (CFG) + (MakeTransferFunctions) end diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index c72a474c1..01e47d518 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -125,7 +125,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = + LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (LowerHil.DefaultConfig) + (ProcCfg.Exceptional) + (TransferFunctions) let checker {Callbacks.proc_desc; tenv; summary} = let proc_data = ProcData.make proc_desc tenv summary in diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index b91111207..0efa19f70 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -744,7 +744,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct end module Analyzer = - LowerHil.MakeAbstractInterpreterWithConfig (HilConfig) (ProcCfg.Exceptional) + LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeRPO) (HilConfig) + (ProcCfg.Exceptional) (TransferFunctions) (* sanity checks for summaries. should only be used in developer mode *) diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 52b4e508a..cbc06a661 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,5 +1,5 @@ codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 58, column 5 here,accessed `*(ptr)` here] -codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `*(ptr)` here] +codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete ptr` at line 68, column 7 here,accessed `ptr` here] codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 12, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete result` at line 21, column 5 here,accessed `*(result)` here] codetoanalyze/cpp/pulse/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete x` at line 112, column 3 here,accessed `x` here] codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidated by call to `delete s` at line 57, column 5 here,accessed `s` here]