diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index e04626081..ab1fcc774 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1346,6 +1346,13 @@ INTERNAL OPTIONS --profiler-samples-reset Cancel the effect of --profiler-samples. + --pulse-max-disjuncts int + Under-approximate after int disjunctions in the domain (default: + 50) + + --pulse-widen-threshold int + Under-approximate after int loop iterations (default: 5) + --reactive-capture Activates: Compile source files only when required by analyzer (clang only) (Conversely: --no-reactive-capture) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 0f450c70d..9685336f7 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1800,6 +1800,16 @@ and project_root = ~meta:"dir" "Specify the root directory of the project" +and pulse_max_disjuncts = + CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:50 + "Under-approximate after $(i,int) disjunctions in the domain" + + +and pulse_widen_threshold = + CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:5 + "Under-approximate after $(i,int) loop iterations" + + and quandary_endpoints = CLOpt.mk_json ~long:"quandary-endpoints" ~in_help:InferCommand.[(Analyze, manual_quandary)] @@ -2837,6 +2847,10 @@ and project_root = !project_root and pulse = !pulse +and pulse_max_disjuncts = !pulse_max_disjuncts + +and pulse_widen_threshold = !pulse_widen_threshold + and purity = !purity and quandary = !quandary diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 79827f329..eb805e08f 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -547,6 +547,10 @@ val progress_bar : [`MultiLine | `Plain | `Quiet] val pulse : bool +val pulse_max_disjuncts : int + +val pulse_widen_threshold : int + val purity : bool val quandary : bool diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index fd673afc0..3df62c286 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -141,9 +141,11 @@ module DisjunctiveTransferFunctions = (struct type domain_t = PulseDomain.t [@@deriving compare] - let join_policy = `JoinAfter 1 + let join_policy = + match Config.pulse_max_disjuncts with 0 -> `NeverJoin | n -> `UnderApproximateAfter n - let widen_policy = `UnderApproximateAfterNumIterations 5 + + let widen_policy = `UnderApproximateAfterNumIterations Config.pulse_widen_threshold end) module DisjunctiveAnalyzer =