From b838b7bc4693cb05ae5a9c72028058f0617df5e0 Mon Sep 17 00:00:00 2001 From: Julian Sutherland Date: Wed, 19 Sep 2018 15:47:59 -0700 Subject: [PATCH] limited widening to 10 steps Reviewed By: mbouaziz Differential Revision: D9946335 fbshipit-source-id: d5f561f48 --- infer/src/checkers/accessTree.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/infer/src/checkers/accessTree.ml b/infer/src/checkers/accessTree.ml index 87f2481b3..9462d60d5 100644 --- a/infer/src/checkers/accessTree.ml +++ b/infer/src/checkers/accessTree.ml @@ -384,8 +384,10 @@ module Make (TraceDomain : AbstractDomain.WithBottom) (Config : Config) = struct (* try for a bit to reach a fixed point before widening aggressively *) let joins_before_widen = 3 + let max_iter = 10 + let widen ~prev ~next ~num_iters = - if phys_equal prev next then prev + if phys_equal prev next || num_iters >= max_iter then prev else if Int.( <= ) num_iters joins_before_widen then join prev next else let trace_widen prev next = TraceDomain.widen ~prev ~next ~num_iters in