From 29d42a5e3287853638a027ba48bf12e0d365de06 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 14 Jun 2017 15:17:32 -0700 Subject: [PATCH] [infer][backend] Only call the prover to check that an expression being dereferenced is not null after checking if the expression is associated with @Nullable Summary: I tested on Fresco and this reduced the number of calls to Prover.check_disequal by 30%. Reviewed By: cristianoc Differential Revision: D5237774 fbshipit-source-id: 377545e --- infer/src/backend/rearrange.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index adce1fe50..0dc01e1a6 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -1368,8 +1368,9 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = let is_deref_of_nullable = let is_definitely_non_null exp prop = Prover.check_disequal tenv prop exp Exp.zero in - Config.report_nullable_inconsistency && not (is_definitely_non_null root prop) - && Option.is_some nullable_var_opt in + Config.report_nullable_inconsistency + && Option.is_some nullable_var_opt + && not (is_definitely_non_null root prop) in let relevant_attributes_getters = [ Attribute.get_resource tenv; Attribute.get_undef tenv;