Module Nullsafe.Models
module Hashtbl = IStdlib.IStd.Caml.Hashtblval match_method_name : IR.Procname.t -> IStdlib.IStd.String.t -> boolval table_has_procedure : (string, 'a) Hashtbl.t -> IR.Procname.t -> boolval get_unique_repr : IR.Procname.t -> ThirdPartyMethod.unique_repr optionval to_modelled_nullability : ThirdPartyMethod.nullability -> bool * bool listval get_special_method_modelled_nullability : IR.Tenv.t -> IR.Procname.t -> (bool * bool list) optionval get_modelled_annotated_signature : is_callee_in_trust_list:bool -> IR.Tenv.t -> IR.ProcAttributes.t -> AnnotatedSignature.tReturn the annotated signature of the procedure, taking into account models. External models take precedence over internal ones.
val is_check_not_null : IR.Procname.t -> boolCheck if the procedure is one of the known methods asserting nullability of the object. Nullsafe should understand that both the argument and return value are non-nullable after the call.
val get_check_not_null_parameter : IR.Procname.t -> int optionParameter number (starting from 1) for a procedure known to produce a non-nullable assertion.
Noneif the function is not known to be an aseertion OR the parameter number is not known
val is_check_state : IR.Procname.t -> boolCheck if the procedure is one of the known Preconditions.checkState.
val is_check_argument : IR.Procname.t -> boolCheck if the procedure is one of the known Preconditions.checkArgument.
val is_noreturn : IR.Procname.t -> boolCheck if the procedure does not return.
val is_true_on_null : IR.Procname.t -> boolCheck if the procedure returns true on null.
val is_false_on_null : IR.Procname.t -> boolCheck if the procedure returns false on null.
val is_containsKey : IR.Procname.t -> boolCheck if the procedure is Map.containsKey().
val is_mapPut : IR.Procname.t -> boolCheck if the procedure is Map.put().
val find_nonnullable_alternative : IR.Procname.t -> ModelTables.nonnull_alternative_method optionCheck if a (nullable) method has a non-nullable alternative: A method that does the same as
proc_namebut asserts the result is not null before returning to the caller.