From f659aa10045cd84760df57c9f208e9ac915e5a03 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 11 Apr 2019 03:55:18 -0700 Subject: [PATCH] [pulse] lower max disjuncts to 20 and loop unrollings to 3 Summary: This is ~2.5x wall clock faster, ~5x user time faster, and finds 98% of the bugs. Not very scientific yet but seems better than the previous non-scientific arbitrary default. Reviewed By: ngorogiannis Differential Revision: D14753494 fbshipit-source-id: b72cdd613 --- infer/man/man1/infer-full.txt | 4 ++-- infer/src/base/Config.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 6c486cfc7..9c3e2c842 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1381,10 +1381,10 @@ INTERNAL OPTIONS --pulse-max-disjuncts int Under-approximate after int disjunctions in the domain (default: - 50) + 20) --pulse-widen-threshold int - Under-approximate after int loop iterations (default: 5) + Under-approximate after int loop iterations (default: 3) --reactive-capture Activates: Compile source files only when required by analyzer diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index d6f2a8646..6944a1950 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1846,12 +1846,12 @@ and project_root = and pulse_max_disjuncts = - CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:50 + CLOpt.mk_int ~long:"pulse-max-disjuncts" ~default:20 "Under-approximate after $(i,int) disjunctions in the domain" and pulse_widen_threshold = - CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:5 + CLOpt.mk_int ~long:"pulse-widen-threshold" ~default:3 "Under-approximate after $(i,int) loop iterations"