diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 6b64e85c0..81009fb99 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -199,8 +199,10 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s else astate_pre in if - ((not is_narrowing) && Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre) - || (is_narrowing && Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre) + if is_narrowing then + (old_state.State.visit_count :> int) > Config.max_narrows + || Domain.( <= ) ~lhs:old_state.State.pre ~rhs:new_pre + else Domain.( <= ) ~lhs:new_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint) else let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 27edb8234..0687ce319 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -220,6 +220,8 @@ let manual_racerd = "RACERD CHECKER OPTIONS" let manual_siof = "SIOF CHECKER OPTIONS" +let max_narrows = 5 + (** Maximum number of widens that can be performed before the analysis will intentionally crash. Used to guard against divergence in the case that someone has implemented a bad widening operator *) diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index f9fd2ec3b..b325d450a 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -119,6 +119,8 @@ val lint_issues_dir_name : string val load_average : float option +val max_narrows : int + val max_widens : int val meet_level : int