diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 9bddd0db2..b320d841a 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1642,6 +1642,11 @@ INTERNAL OPTIONS --profiler-samples-reset Cancel the effect of --profiler-samples. + --pulse-intraprocedural-only + Activates: Disable inter-procedural analysis in Pulse. Used for + experimentations only. (Conversely: + --no-pulse-intraprocedural-only) + --pulse-max-disjuncts int Under-approximate after int disjunctions in the domain diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 570cdd6ff..436adb185 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1955,6 +1955,11 @@ and project_root = ~meta:"dir" "Specify the root directory of the project" +and pulse_intraprocedural_only = + CLOpt.mk_bool ~long:"pulse-intraprocedural-only" + "Disable inter-procedural analysis in Pulse. Used for experimentations only." + + and pulse_max_disjuncts = CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:20 "Under-approximate after $(i,int) disjunctions in the domain" @@ -3077,6 +3082,8 @@ and project_root = !project_root and pulse = !pulse +and pulse_intraprocedural_only = !pulse_intraprocedural_only + and pulse_max_disjuncts = !pulse_max_disjuncts and pulse_widen_threshold = !pulse_widen_threshold diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index e3733f291..383de4a0b 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -550,6 +550,8 @@ val project_root : string val pulse : bool +val pulse_intraprocedural_only : bool + val pulse_max_disjuncts : int val pulse_widen_threshold : int diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 690d9b410..53399da67 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -44,10 +44,10 @@ module PulseTransferFunctions = struct let interprocedural_call caller_summary ret call_exp actuals call_loc get_formals astate = match proc_name_of_call call_exp with - | Some callee_pname -> + | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_formals callee_pname in PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate - | None -> + | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; Ok [ PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals