[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
master
Jeremy Dubreil 8 years ago committed by Facebook Github Bot
parent acb7cf8dfe
commit 29d42a5e32

@ -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;

Loading…
Cancel
Save