diff --git a/infer/src/eradicate/models.ml b/infer/src/eradicate/models.ml index 62d001632..3befd261c 100644 --- a/infer/src/eradicate/models.ml +++ b/infer/src/eradicate/models.ml @@ -107,6 +107,14 @@ end (* Inference *) +let match_method_name pn name = + match pn with + | Typ.Procname.Java pn_java -> + String.equal (Typ.Procname.Java.get_method pn_java) name + | _ -> + false + + let table_has_procedure table proc_name = let proc_id = Typ.Procname.to_unique_id proc_name in try @@ -167,12 +175,16 @@ let is_modelled_nullable proc_name = (** Check if the procedure is one of the known Preconditions.checkNotNull. *) -let is_check_not_null proc_name = table_has_procedure check_not_null_table proc_name +let is_check_not_null proc_name = + table_has_procedure check_not_null_table proc_name || match_method_name proc_name "checkNotNull" + (** Parameter number for a procedure known to be a checkNotNull *) let get_check_not_null_parameter proc_name = let proc_id = Typ.Procname.to_unique_id proc_name in - try Hashtbl.find check_not_null_parameter_table proc_id with Not_found -> 0 + try Hashtbl.find check_not_null_parameter_table proc_id with Not_found -> + (* Assume the check is on the first parameter unless modeled otherwise *) + 1 (** Check if the procedure is one of the known Preconditions.checkState. *) diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 567413adc..a6df563f8 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -843,22 +843,14 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get TypeState.set_extension typestate1 extension' else typestate1 in - let has_method pn name = - match pn with - | Typ.Procname.Java pn_java -> - String.equal (Typ.Procname.Java.get_method pn_java) name - | _ -> - false - in if Models.is_check_not_null callee_pname then - do_preconditions_check_not_null - (Models.get_check_not_null_parameter callee_pname) - ~is_vararg:false typestate2 - else if has_method callee_pname "checkNotNull" - && Typ.Procname.Java.is_vararg callee_pname_java - then - let last_parameter = List.length call_params in - do_preconditions_check_not_null last_parameter ~is_vararg:true typestate2 + if Typ.Procname.Java.is_vararg callee_pname_java then + let last_parameter = List.length call_params in + do_preconditions_check_not_null last_parameter ~is_vararg:true typestate2 + else + do_preconditions_check_not_null + (Models.get_check_not_null_parameter callee_pname) + ~is_vararg:false typestate2 else if Models.is_check_state callee_pname || Models.is_check_argument callee_pname then do_preconditions_check_state typestate2 else if Models.is_mapPut callee_pname then do_map_put typestate2 diff --git a/infer/tests/codetoanalyze/java/eradicate/MyPreconditions.java b/infer/tests/codetoanalyze/java/eradicate/MyPreconditions.java new file mode 100644 index 000000000..b639477d5 --- /dev/null +++ b/infer/tests/codetoanalyze/java/eradicate/MyPreconditions.java @@ -0,0 +1,17 @@ +/* + * Copyright (c) 2018 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +package codetoanalyze.java.eradicate; + +import javax.annotation.Nullable; + +public class MyPreconditions { + + public static native T checkNotNull(@Nullable T t); + +} diff --git a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java index 24e1409d3..548284d0a 100644 --- a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java +++ b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java @@ -294,4 +294,10 @@ public class NullMethodCall { nullableParameter.toString(); } } + + String customPreconditionsCheckNotNullOkay() { + MyPreconditions.checkNotNull(nullableField); + return nullableField.toString(); + } + }