diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 941ed7103..255fc1acf 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -96,7 +96,13 @@ struct else astate_pre in if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue) - else update_inv_map widened_pre (old_state.visit_count + 1) + else + let visit_count' = old_state.visit_count + 1 in + if visit_count' > Config.max_widens then + failwithf + "Exceeded max widening threshold %d while analyzing %a. Please check your widening operator or increase the threshold" + Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ; + update_inv_map widened_pre visit_count' else (* first time visiting this node *) let visit_count = 1 in diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 511abf24c..f4bf9ce86 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -189,6 +189,11 @@ let manual_threadsafety = "THREADSAFETY CHECKER OPTIONS" (** Maximum level of recursion during the analysis, after which a timeout is generated *) let max_recursion = 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 *) +let max_widens = 10000 + (** Flag to tune the level of applying the meet operator for preconditions during the footprint analysis: 0 = do not use the meet diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 4a8f350b8..c166fea49 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -153,6 +153,8 @@ val log_dir_name : string val max_recursion : int +val max_widens : int + val meet_level : int val models_dir : string