pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[java tracing] goodbye

Browse Source 
Summary: Unused and in the way.

Reviewed By: jvillard

Differential Revision: D17878363

fbshipit-source-id: 1b6410e08
master
Nikos Gorogiannis 5 years ago committed by Facebook Github Bot
parent 432d391a32
commit 9dbe55c419
36 changed files with 2 additions and 674 deletions
Show Stats Download Patch File Download Diff File

1
Makefile
Unescape View File

@ -163,7 +163,6 @@ DIRECT_TESTS += \
java_racerd \
java_starvation \
java_topl \
java_tracing \
ifeq ($(IS_FACEBOOK_TREE),yes)
DIRECT_TESTS += java_fb-performance

6
infer/man/man1/infer-full.txt
Unescape View File

@ -1781,12 +1781,6 @@ INTERNAL OPTIONS
Activates: Detailed tracing information during TOPL analysis
(Conversely: --no-trace-topl)
--tracing
Activates: Report error traces for runtime exceptions (Java only):
generate preconditions for runtimeexceptions in Java and report
errors for public methods which throw runtime exceptions
(Conversely: --no-tracing)
--tv-commit commit
Commit hash to submit to Traceview

9
infer/src/IR/Localise.ml
Unescape View File

@ -317,15 +317,6 @@ let deref_str_array_bound size_opt index_opt =
; problem_str= "could be accessed with " ^ index_str ^ " out of bounds" }
(** Java unchecked exceptions errors *)
let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc =
{ no_desc with
descriptions=
[ MF.monospaced_to_string (Typ.Procname.to_string proc_name)
; "can throw " ^ MF.monospaced_to_string (Typ.Name.name exn_name)
; "whenever " ^ pre_str ] }
let desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc =
let line_info = at_line (Tags.create ()) loc in
let accessed_fld_str = Typ.Fieldname.to_string accessed_fld in

2
infer/src/IR/Localise.mli
Unescape View File

@ -142,8 +142,6 @@ val desc_leak :
val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
val java_unchecked_exn_desc : Typ.Procname.t -> Typ.Name.t -> string -> error_desc
val desc_custom_error : Location.t -> error_desc
(** Create human-readable error description for assertion failures *)

5
infer/src/absint/PatternMatch.ml
Unescape View File

@ -425,11 +425,6 @@ let get_fields_nullified procdesc =
nullified_flds
(** Checks if the exception is an unchecked exception *)
let is_runtime_exception tenv typename =
is_subtype_of_str tenv typename "java.lang.RuntimeException"
(** Checks if the class name is a Java exception *)
let is_throwable tenv typename = is_subtype_of_str tenv typename "java.lang.Throwable"

4
infer/src/absint/PatternMatch.mli
Unescape View File

@ -141,10 +141,6 @@ val get_fields_nullified : Procdesc.t -> Typ.Fieldname.Set.t
val is_throwable : Tenv.t -> Typ.Name.t -> bool
(** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *)
val is_runtime_exception : Tenv.t -> Typ.Name.t -> bool
(** [is_runtime_exception tenv class_name] checks if classname is
of type java.lang.RuntimeException *)
val check_class_attributes : (Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> bool
(** tests whether any class attributes (e.g., @ThreadSafe) pass check of first argument,
including supertypes*)

8
infer/src/base/Config.ml
Unescape View File

@ -2380,12 +2380,6 @@ and trace_topl =
CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during TOPL analysis"
and tracing =
CLOpt.mk_bool ~deprecated:["tracing"] ~long:"tracing"
"Report error traces for runtime exceptions (Java only): generate preconditions for \
runtimeexceptions in Java and report errors for public methods which throw runtime exceptions"
and tv_commit =
CLOpt.mk_string_opt ~long:"tv-commit" ~meta:"commit" "Commit hash to submit to Traceview"
@ -3237,8 +3231,6 @@ and trace_rearrange = !trace_rearrange
and trace_topl = !trace_topl
and tracing = !tracing
and tv_commit = !tv_commit
and tv_limit = !tv_limit

2
infer/src/base/Config.mli
Unescape View File

@ -704,8 +704,6 @@ val trace_rearrange : bool
val trace_topl : bool
val tracing : bool
val tv_commit : string option
val tv_limit : int

2
infer/src/biabduction/Abs.ml
Unescape View File

@ -1093,8 +1093,6 @@ let check_junk pname tenv prop =
(Language.curr_language_is Java, exn_leak)
| Some _, Rignore ->
(true, exn_leak)
| Some _, Rfile when Config.tracing ->
(true, exn_leak)
| Some _, Rfile ->
(false, exn_leak)
| Some _, Rlock ->

2
infer/src/biabduction/SymExec.ml
Unescape View File

@ -1302,7 +1302,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
| _ ->
()
in
if not (Config.tracing || Typ.Procname.is_java current_pname) then
if not (Typ.Procname.is_java current_pname) then
check_already_dereferenced tenv current_pname cond prop__ ;
check_condition_always_true_false () ;
let n_cond, prop = check_arith_norm_exp tenv current_pname cond prop__ in

54
infer/src/biabduction/interproc.ml
Unescape View File

@ -926,23 +926,6 @@ let reset_global_values proc_desc =
set_current_language proc_desc
(* Collect all pairs of the kind (precondition, runtime exception) from a summary *)
let exception_preconditions tenv pname summary =
let collect_exceptions pre (exns, all_post_exn) (prop, _) =
match Tabulation.prop_get_exn_name pname prop with
| Some exn_name when PatternMatch.is_runtime_exception tenv exn_name ->
((pre, exn_name) :: exns, all_post_exn)
| _ ->
(exns, false)
in
let collect_spec errors spec =
List.fold
~f:(collect_exceptions spec.BiabductionSummary.pre)
~init:errors spec.BiabductionSummary.posts
in
List.fold ~f:collect_spec ~init:([], true) (Tabulation.get_specs_from_payload summary)
(* Collect all pairs of the kind (precondition, custom error) from a summary *)
let custom_error_preconditions summary =
let collect_errors pre (errors, all_post_error) (prop, _) =
@ -996,41 +979,6 @@ let is_unavoidable tenv pre =
false
(** Detects if there are specs of the form {precondition} proc {runtime exception} and report
an error in that case, generating the trace that lead to the runtime exception if the method is
called in the context { precondition } *)
let report_runtime_exceptions tenv pdesc summary =
let pname = Summary.get_proc_name summary in
let is_public_method =
PredSymb.equal_access (Summary.get_attributes summary).access PredSymb.Public
in
let is_main =
is_public_method
&&
match pname with
| Typ.Procname.Java pname_java ->
Typ.Procname.Java.is_static pname_java
&& String.equal (Typ.Procname.Java.get_method pname_java) "main"
| _ ->
false
in
let is_annotated pdesc = Annotations.pdesc_has_return_annot pdesc Annotations.ia_is_verify in
let exn_preconditions, all_post_exn = exception_preconditions tenv pname summary in
let should_report pre =
all_post_exn || is_main || is_annotated pdesc || is_unavoidable tenv pre
in
let report (pre, runtime_exception) =
if should_report pre then
let pre_str =
F.asprintf "%a" (Prop.pp_prop Pp.text) (BiabductionSummary.Jprop.to_prop pre)
in
let exn_desc = Localise.java_unchecked_exn_desc pname runtime_exception pre_str in
let exn = Exceptions.Java_runtime_exception (runtime_exception, pre_str, exn_desc) in
Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn
in
List.iter ~f:report exn_preconditions
let report_custom_errors tenv summary =
let pname = Summary.get_proc_name summary in
let error_preconditions, all_post_error = custom_error_preconditions summary in
@ -1150,8 +1098,6 @@ let analyze_proc summary exe_env tenv proc_cfg : Summary.t =
let updated_summary = update_summary tenv summary specs phase res in
if Language.curr_language_is Clang && Config.report_custom_error then
report_custom_errors tenv updated_summary ;
if Language.curr_language_is Java && Config.tracing then
report_runtime_exceptions tenv proc_desc updated_summary ;
updated_summary

4
infer/src/checkers/annotations.ml
Unescape View File

@ -103,8 +103,6 @@ let true_on_null = "TrueOnNull"
let ui_thread = "UiThread"
let verify_annotation = "com.facebook.infer.annotation.Verify"
let visibleForTesting = "VisibleForTesting"
let volatile = "volatile"
@ -223,8 +221,6 @@ let ia_is_field_injector_readwrite ia =
List.exists ~f:(ia_ends_with ia) field_injector_readwrite_list
let ia_is_verify ia = ia_contains ia verify_annotation
let ia_is_expensive ia = ia_ends_with ia expensive
let ia_is_functional ia = ia_ends_with ia functional

2
infer/src/checkers/annotations.mli
Unescape View File

@ -78,8 +78,6 @@ val ia_is_nullable : Annot.Item.t -> bool
val ia_is_true_on_null : Annot.Item.t -> bool
val ia_is_verify : Annot.Item.t -> bool
val ia_is_expensive : Annot.Item.t -> bool
val ia_is_functional : Annot.Item.t -> bool

6
infer/src/java/jConfig.ml
Unescape View File

@ -14,12 +14,6 @@ let builtins_package = "com.facebook.infer.builtins"
let infer_builtins_cl = builtins_package ^ ".InferBuiltins"
let npe_cl = "java.lang.NullPointerException"
let cce_cl = "java.lang.ClassCastException"
let out_of_bound_cl = "java.lang.ArrayIndexOutOfBoundsException"
(** {2 Names of special variables, constants and method names} *)
let this = Mangled.this

6
infer/src/java/jConfig.mli
Unescape View File

@ -54,9 +54,3 @@ val field_cst : string
val field_st : Mangled.t
val infer_builtins_cl : string
val npe_cl : string
val out_of_bound_cl : string
val cce_cl : string

179
infer/src/java/jTrans.ml
Unescape View File

@ -457,8 +457,6 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name =
None
let builtin_new = Exp.Const (Const.Cfun BuiltinDecl.__new)
let builtin_get_array_length = Exp.Const (Const.Cfun BuiltinDecl.__get_array_length)
let create_sil_deref exp ~root_typ ~typ loc =
@ -641,7 +639,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let instrs =
let is_non_constructor_call = match invoke_code with I_Special -> false | _ -> true in
match sil_obj_expr with
| Exp.Var _ when is_non_constructor_call && not Config.tracing ->
| Exp.Var _ when is_non_constructor_call ->
let obj_typ_no_ptr =
match sil_obj_type.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> sil_obj_type
in
@ -808,18 +806,6 @@ type translation =
| Prune of Procdesc.Node.t * Procdesc.Node.t
| Loop of Procdesc.Node.t * Procdesc.Node.t * Procdesc.Node.t
let is_this expr =
match expr with
| JBir.Var (_, var) -> (
match JBir.var_name_debug var with
| None ->
false
| Some name_opt ->
String.equal (Mangled.to_string JConfig.this) name_opt )
| _ ->
false
let assume_not_null loc sil_expr =
let builtin_infer_assume = Exp.Const (Const.Cfun BuiltinDecl.__infer_assume) in
let not_null_expr = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
@ -1101,166 +1087,6 @@ let instruction (context : JContext.t) pc instr : translation =
let node_kind = create_node_kind callee_procname in
let call_node = create_node node_kind (instrs @ call_instrs) in
Instr call_node
| Check (CheckNullPointer expr) when Config.tracing && is_this expr ->
(* TODO #6509339: refactor the boilerplate code in the translation of JVM checks *)
let instrs, sil_expr, _ = expression context pc expr in
let this_not_null_node =
create_node (Procdesc.Node.Stmt_node ThisNotNull)
(instrs @ [assume_not_null loc sil_expr])
in
Instr this_not_null_node
| Check (CheckNullPointer expr) when Config.tracing ->
let instrs, sil_expr, _ = expression context pc expr in
let not_null_node =
let sil_not_null = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
let sil_prune_not_null = Sil.Prune (sil_not_null, loc, true, Sil.Ik_if)
and not_null_kind = Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_NotNull) in
create_node not_null_kind (instrs @ [sil_prune_not_null])
in
let throw_npe_node =
let sil_is_null = Exp.BinOp (Binop.Eq, sil_expr, Exp.null) in
let sil_prune_null = Sil.Prune (sil_is_null, loc, true, Sil.Ik_if)
and npe_kind = Procdesc.Node.Stmt_node ThrowNPE
and npe_cn = JBasics.make_cn JConfig.npe_cl in
let class_type = JTransType.get_class_type program tenv npe_cn
and class_type_np = JTransType.get_class_type_no_pointer program tenv npe_cn in
let sizeof_exp =
Exp.Sizeof
{typ= class_type_np; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
in
let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in
let new_instr =
Sil.Call ((ret_id, class_type), builtin_new, args, loc, CallFlags.default)
in
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let _, call_instrs =
let ret_opt = Some (Exp.Var ret_id, class_type) in
method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special
Typ.Procname.Java.Static
in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in
create_node npe_kind npe_instrs
in
Prune (not_null_node, throw_npe_node)
| Check (CheckArrayBound (array_expr, index_expr)) when Config.tracing ->
let instrs, _, sil_length_expr, sil_index_expr =
let array_instrs, sil_array_expr, _ = expression context pc array_expr
and length_instrs, sil_length_expr, _ =
expression context pc (JBir.Unop (JBir.ArrayLength, array_expr))
and index_instrs, sil_index_expr, _ = expression context pc index_expr in
let instrs = array_instrs @ index_instrs @ length_instrs in
(instrs, sil_array_expr, sil_length_expr, sil_index_expr)
in
let in_bound_node =
let in_bound_node_kind =
Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_InBound)
in
let sil_assume_in_bound =
let sil_in_bound =
let sil_positive_index =
Exp.BinOp (Binop.Ge, sil_index_expr, Exp.Const (Const.Cint IntLit.zero))
and sil_less_than_length = Exp.BinOp (Binop.Lt, sil_index_expr, sil_length_expr) in
Exp.BinOp (Binop.LAnd, sil_positive_index, sil_less_than_length)
in
Sil.Prune (sil_in_bound, loc, true, Sil.Ik_if)
in
create_node in_bound_node_kind (instrs @ [sil_assume_in_bound])
and throw_out_of_bound_node =
let out_of_bound_node_kind = Procdesc.Node.Stmt_node OutOfBound in
let sil_assume_out_of_bound =
let sil_out_of_bound =
let sil_negative_index =
Exp.BinOp (Binop.Lt, sil_index_expr, Exp.Const (Const.Cint IntLit.zero))
and sil_greater_than_length =
Exp.BinOp (Binop.Gt, sil_index_expr, sil_length_expr)
in
Exp.BinOp (Binop.LOr, sil_negative_index, sil_greater_than_length)
in
Sil.Prune (sil_out_of_bound, loc, true, Sil.Ik_if)
in
let out_of_bound_cn = JBasics.make_cn JConfig.out_of_bound_cl in
let class_type = JTransType.get_class_type program tenv out_of_bound_cn
and class_type_np = JTransType.get_class_type_no_pointer program tenv out_of_bound_cn in
let sizeof_exp =
Exp.Sizeof
{typ= class_type_np; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
in
let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in
let new_instr =
Sil.Call ((ret_id, ret_type), builtin_new, args, loc, CallFlags.default)
in
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let _, call_instrs =
method_invocation context loc pc None out_of_bound_cn constr_ms
(Some (Exp.Var ret_id, class_type))
[] I_Special Typ.Procname.Java.Static
in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let out_of_bound_instrs =
instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr]
in
create_node out_of_bound_node_kind out_of_bound_instrs
in
Prune (in_bound_node, throw_out_of_bound_node)
| Check (CheckCast (expr, object_type)) when Config.tracing ->
let sil_type = JTransType.expr_type context expr
and instrs, sil_expr, _ = expression context pc expr
and ret_id = Ident.create_fresh Ident.knormal
and sizeof_expr =
JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof
in
let check_cast = Exp.Const (Const.Cfun BuiltinDecl.__instanceof) in
let args = [(sil_expr, sil_type); (sizeof_expr, Typ.mk Tvoid)] in
let call = Sil.Call ((ret_id, ret_type), check_cast, args, loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in
let is_instance_node =
let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in
let asssume_instance_of = Sil.Prune (check_is_false, loc, true, Sil.Ik_if)
and instance_of_kind =
Procdesc.Node.Prune_node (true, Sil.Ik_if, PruneNodeKind_IsInstance)
in
create_node instance_of_kind (instrs @ [call; asssume_instance_of])
and throw_cast_exception_node =
let check_is_true = Exp.BinOp (Binop.Ne, res_ex, Exp.one) in
let asssume_not_instance_of = Sil.Prune (check_is_true, loc, true, Sil.Ik_if)
and throw_cast_exception_kind = Procdesc.Node.Stmt_node ClassCastException
and cce_cn = JBasics.make_cn JConfig.cce_cl in
let class_type = JTransType.get_class_type program tenv cce_cn
and class_type_np = JTransType.get_class_type_no_pointer program tenv cce_cn in
let sizeof_exp =
Exp.Sizeof
{typ= class_type_np; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
in
let args = [(sizeof_exp, class_type)] in
let ret_id = Ident.create_fresh Ident.knormal in
let new_instr =
Sil.Call ((ret_id, ret_type), builtin_new, args, loc, CallFlags.default)
in
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
let _, call_instrs =
method_invocation context loc pc None cce_cn constr_ms
(Some (Exp.Var ret_id, class_type))
[] I_Special Typ.Procname.Java.Static
in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let cce_instrs =
instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr]
in
create_node throw_cast_exception_kind cce_instrs
in
Prune (is_instance_node, throw_cast_exception_node)
| MonitorEnter expr ->
trans_monitor_enter_exit context expr pc loc BuiltinDecl.__set_locked_attribute
MonitorEnter
@ -1274,9 +1100,6 @@ let instruction (context : JContext.t) pc instr : translation =
flags '~formula:false' *)
Skip
| Check _ ->
(* Infer only considers 3 kinds of runtime error exceptions
currently: NullPointer, ArrayBound, Cast. And only when
Config.tracing=true. *)
Skip
| MayInit _ ->
(* Infer ignores Sawja MayInit instruction. This instruction

23
infer/tests/codetoanalyze/java/tracing/.inferconfig
Unescape View File

@ -1,23 +0,0 @@
{
"force-delete-results-dir": true,
"never-returning-null": [
{
"language": "Java",
"source_contains": "_AUTOMATICALLY_GENERATED_"
},
{
"language": "Java",
"class": "codetoanalyze.java.infer.SomeLibrary",
"method": "get"
}
],
"report-blacklist-files-containing": [
"@generated"
],
"skip-translation": [
{
"language": "Java",
"source_contains": "_SHOULD_BE_SKIPPED_"
}
]
}

43
infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java
Unescape View File

@ -1,43 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
import com.facebook.infer.annotation.Verify;
public class ArrayIndexOutOfBoundsExceptionExample {
void callMethodFromArray(T2[] array, int index) {
if (array[index] != null) {
array[index].f();
}
}
@Verify
public void missingCheckOnIndex(T2[] array, int index) {
if (array != null) {
if (index < array.length) {
callMethodFromArray(array, index);
}
}
}
void callOutOfBound() {
T2[] array = new T2[42];
callMethodFromArray(array, -5);
}
void withFixedIndex(T2[] array) {
int index = 9;
callMethodFromArray(array, index);
}
void arrayIndexOutOfBoundsInCallee() {
T2[] array = new T2[8];
withFixedIndex(array);
}
}

1
infer/tests/codetoanalyze/java/tracing/ArrayOutOfBounds.java
Unescape View File

@ -1 +0,0 @@
../infer/ArrayOutOfBounds.java

35
infer/tests/codetoanalyze/java/tracing/ClassCastExceptionExample.java
Unescape View File

@ -1,35 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
import com.facebook.infer.annotation.Verify;
class S extends T2 {}
public class ClassCastExceptionExample {
S cast(T2 t) {
return (S) t;
}
void foo() {
T2 t = new T2();
S s = cast(t);
s.toString();
}
T2 m;
@Verify
public S bar(int x) {
if (x < 4 && m != null) {
return (S) m;
}
return null;
}
}

1
infer/tests/codetoanalyze/java/tracing/ClassCastExceptions.java
Unescape View File

@ -1 +0,0 @@
../infer/ClassCastExceptions.java

1
infer/tests/codetoanalyze/java/tracing/CloseableAsResourceExample.java
Unescape View File

@ -1 +0,0 @@
../infer/CloseableAsResourceExample.java

52
infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java
Unescape View File

@ -1,52 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
interface I {
T2 get();
}
class A implements I {
public T2 get() {
return new T2();
}
}
class B extends A {
public T2 get() {
return null;
}
}
public class LazyDynamicDispatchExample {
static T2 fromSupertype(A a) {
return a.get();
}
static T2 fromInterface(I i) {
return i.get();
}
static void callWithSubtype() {
B b = new B();
fromSupertype(b).f();
}
static void shouldNotReportLocalVarTypeIsKnown() {
A a = new A();
fromInterface(a).f();
}
static void shouldReportLocalVarTypeIsKnown() {
B b = new B();
fromInterface(b).f();
}
}

42
infer/tests/codetoanalyze/java/tracing/LocallyDefinedExceptionExample.java
Unescape View File

@ -1,42 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
import com.facebook.infer.annotation.Verify;
class LocallyDefinedException extends RuntimeException {
public LocallyDefinedException(String message) {
super(message);
}
}
public class LocallyDefinedExceptionExample {
T2 t;
public LocallyDefinedExceptionExample() {
this.t = new T2();
this.t.x = 42;
}
void setT(T2 t) {
this.t = t;
}
@Verify
void fieldInvariant() {
if (this.t != null) {
if (this.t.x != 42) {
throw new LocallyDefinedException("Field expected to be equal to 42");
} else {
this.t.x = 0;
}
}
}
}

12
infer/tests/codetoanalyze/java/tracing/Makefile
Unescape View File

@ -1,12 +0,0 @@
# Copyright (c) Facebook, Inc. and its affiliates.
#
# This source code is licensed under the MIT license found in the
# LICENSE file in the root directory of this source tree.
TESTS_DIR = ../../..
INFER_OPTIONS = --biabduction-only --tracing --debug-exceptions
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.java)
include $(TESTS_DIR)/javac.make

1
infer/tests/codetoanalyze/java/tracing/NeverNullSource.java
Unescape View File

@ -1 +0,0 @@
../infer/NeverNullSource.java

40
infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java
Unescape View File

@ -1,40 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
import com.facebook.infer.annotation.Verify;
public class NullPointerExceptionExample {
void deref(T2 t) {
t.f();
}
@Verify
void callDeref(T2 t, boolean condition) {
if (condition) {
deref(t);
}
}
void callDoesNotLeadToNpe() {
callDeref(null, false);
}
void callLeadToNpe() {
callDeref(null, true);
}
void npeOnBothBranches(int x) {
if (x < 2) {
callDeref(null, x < 3);
} else {
callDeref(null, true);
}
}
}

1
infer/tests/codetoanalyze/java/tracing/NullPointerExceptions.java
Unescape View File

@ -1 +0,0 @@
../infer/NullPointerExceptions.java

27
infer/tests/codetoanalyze/java/tracing/ReportOnMainExample.java
Unescape View File

@ -1,27 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
public class ReportOnMainExample {
T2 t;
native boolean test();
void foo() {
if (test() && t == null) {
return;
}
t.f();
}
public static void main(String[] args) {
ReportOnMainExample example = new ReportOnMainExample();
example.foo();
}
}

1
infer/tests/codetoanalyze/java/tracing/SkippedSourceFile.java
Unescape View File

@ -1 +0,0 @@
../infer/SkippedSourceFile.java

1
infer/tests/codetoanalyze/java/tracing/SomeLibrary.java
Unescape View File

@ -1 +0,0 @@
../infer/SomeLibrary.java

1
infer/tests/codetoanalyze/java/tracing/T.java
Unescape View File

@ -1 +0,0 @@
../infer/T.java

14
infer/tests/codetoanalyze/java/tracing/T2.java
Unescape View File

@ -1,14 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
public class T2 {
int x;
void f() {}
}

30
infer/tests/codetoanalyze/java/tracing/UnavoidableExceptionExample.java
Unescape View File

@ -1,30 +0,0 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.tracing;
public class UnavoidableExceptionExample {
static T2 create() {
return null;
}
static void cannotAvoidNPE() {
T2 t = create();
t.f();
}
static void unavoidableNPEWithParameter(boolean b) {
T2 t = create();
t.f();
}
void virtualMethodWithUnavoidableNPE(boolean b) {
T2 t = create();
t.f();
}
}

1
infer/tests/codetoanalyze/java/tracing/Utils.java
Unescape View File

@ -1 +0,0 @@
../infer/Utils.java

57
infer/tests/codetoanalyze/java/tracing/issues.exp
Unescape View File

@ -1,57 +0,0 @@
codetoanalyze/java/infer/ArrayOutOfBounds.java, codetoanalyze.java.infer.ArrayOutOfBounds.arrayOutOfBounds():int, 2, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure arrayOutOfBounds(),Taking true branch,exception java.lang.ArrayIndexOutOfBoundsException,return from a call to int ArrayOutOfBounds.arrayOutOfBounds()]
codetoanalyze/java/infer/ArrayOutOfBounds.java, codetoanalyze.java.infer.ArrayOutOfBounds.switchedArrsOutOfBounds():void, 2, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure switchedArrsOutOfBounds(),start of procedure buggyIter(...),Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking false branch,return from a call to void ArrayOutOfBounds.buggyIter(int[],int[]),return from a call to void ArrayOutOfBounds.switchedArrsOutOfBounds()]
codetoanalyze/java/infer/ClassCastExceptions.java, codetoanalyze.java.infer.ClassCastExceptions.classCastException():void, 3, java.lang.ClassCastException, no_bucket, ERROR, [start of procedure classCastException(),start of procedure SubClassA(),start of procedure SuperClass(),return from a call to SuperClass.<init>(),return from a call to SubClassA.<init>(),Skipping ClassCastException(): unknown method,exception java.lang.ClassCastException,return from a call to void ClassCastExceptions.classCastException()]
codetoanalyze/java/infer/ClassCastExceptions.java, codetoanalyze.java.infer.ClassCastExceptions.classCastExceptionImplementsInterface():int, 0, java.lang.ClassCastException, no_bucket, ERROR, [start of procedure classCastExceptionImplementsInterface(),start of procedure AnotherImplementationOfInterface(),return from a call to AnotherImplementationOfInterface.<init>(),start of procedure classCastExceptionImplementsInterfaceCallee(...),Skipping ClassCastException(): unknown method,exception java.lang.ClassCastException,return from a call to int ClassCastExceptions.classCastExceptionImplementsInterfaceCallee(AnotherImplementationOfInterface),exception java.lang.ClassCastException,return from a call to int ClassCastExceptions.classCastExceptionImplementsInterface()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure npeWithDollars(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.addNullToImmutableListBuilderBad():void, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure addNullToImmutableListBuilderBad(),Skipping builder(): unknown method,start of procedure getObject(),return from a call to Object NullPointerExceptions.getObject(),Taking true branch]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.addNullToImmutableListBuilderBad():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure addNullToImmutableListBuilderBad(),Skipping builder(): unknown method,start of procedure getObject(),return from a call to Object NullPointerExceptions.getObject(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.addNullToImmutableListBuilderBad()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE():void, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure badCheckShouldCauseNPE(),start of procedure getBool(),Skipping test(): unknown method,Definition of test(),Taking true branch,return from a call to Boolean NullPointerExceptions.getBool(),Taking true branch,start of procedure getObj(),Skipping test(): unknown method,Definition of test(),Taking true branch,return from a call to Object NullPointerExceptions.getObj(),Taking true branch,return from a call to void NullPointerExceptions.badCheckShouldCauseNPE()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.deferenceNullableMethodCallingSkippedMethodBad():void, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure deferenceNullableMethodCallingSkippedMethodBad(),start of procedure wrapUnknownFuncWithNullable(),Skipping unknownFunc(): unknown method,Definition of unknownFunc(),return from a call to Object NullPointerExceptions.wrapUnknownFuncWithNullable(),Taking true branch,return from a call to void NullPointerExceptions.deferenceNullableMethodCallingSkippedMethodBad()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNonThisGetterAfterCheckShouldNotCauseNPE():void, 5, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure derefNonThisGetterAfterCheckShouldNotCauseNPE(),start of procedure NullPointerExceptions(),return from a call to NullPointerExceptions.<init>(),Taking true branch,start of procedure getObj(),Skipping test(): unknown method,Definition of test(),Taking true branch,return from a call to Object NullPointerExceptions.getObj(),Taking true branch,Taking true branch,start of procedure getObj(),Skipping test(): unknown method,Definition of test(),Taking true branch,return from a call to Object NullPointerExceptions.getObj(),Taking true branch,return from a call to void NullPointerExceptions.derefNonThisGetterAfterCheckShouldNotCauseNPE()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNull():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure derefNull(),start of procedure derefUndefinedCallee(),start of procedure retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.retUndefined(),exception java.lang.NullPointerException,return from a call to Object NullPointerExceptions.derefUndefinedCallee(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.derefNull()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper(),Taking true branch,return from a call to void NullPointerExceptions.derefUndefNullableRetWrapper()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefinedCallee():java.lang.Object, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure derefUndefinedCallee(),start of procedure retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.retUndefined(),Taking true branch,return from a call to Object NullPointerExceptions.derefUndefinedCallee()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterLoopOnList(NullPointerExceptions$L)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 5, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock1(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock1(Lock)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 5, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock1(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock1(Lock)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 7, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock2(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock2(Lock)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 7, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock2(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.dereferenceAfterUnlock2(Lock)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dontReportOnNullableIndirectReassignmentToUnknown(java.lang.Object):void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure dontReportOnNullableIndirectReassignmentToUnknown(...),start of procedure callUnknownFunc(),Skipping unknownFunc(): unknown method,Definition of unknownFunc(),return from a call to Object NullPointerExceptions.callUnknownFunc(),Taking true branch,return from a call to void NullPointerExceptions.dontReportOnNullableIndirectReassignmentToUnknown(Object)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullListFiles(java.lang.String):int, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullListFiles(...),Skipping File(...): unknown method,Taking true branch,exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullListFiles(String)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerException():int, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerException(),exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerException()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionArrayLength():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionArrayLength(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionArrayLength()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionCallArrayReadMethod():void, 2, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure nullPointerExceptionCallArrayReadMethod(),Taking true branch,Taking true branch]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor():void, 9, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),Taking true branch,return from a call to void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor():void, 8, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionFromFaillingResourceConstructor(),Taking true branch,return from a call to void NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionInterProc():int, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionInterProc(),start of procedure canReturnNullObject(...),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.<init>(NullPointerExceptions),Taking false branch,return from a call to NullPointerExceptions$A NullPointerExceptions.canReturnNullObject(boolean),exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerExceptionInterProc()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionUnlessFrameFails():void, 6, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.<init>(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),Taking true branch,return from a call to Object NullPointerExceptions.id_generics(NullPointerExceptions$A),Taking true branch,return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch,exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionUnlessFrameFails()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionWithAChainOfFields(codetoanalyze.java.infer.NullPointerExceptions$C):int, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionWithAChainOfFields(...),start of procedure NullPointerExceptions$B(...),return from a call to NullPointerExceptions$B.<init>(NullPointerExceptions),exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerExceptionWithAChainOfFields(NullPointerExceptions$C)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionWithAChainOfFields(codetoanalyze.java.infer.NullPointerExceptions$C):int, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionWithAChainOfFields(...),start of procedure NullPointerExceptions$B(...),return from a call to NullPointerExceptions$B.<init>(NullPointerExceptions),exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerExceptionWithAChainOfFields(NullPointerExceptions$C)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionWithArray():int, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionWithArray(),Taking true branch,Taking true branch,Taking true branch,Taking true branch,exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerExceptionWithArray()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionWithExceptionHandling(boolean):int, 5, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionWithExceptionHandling(...),Taking true branch,exception java.lang.Exception,Switch condition is true. Entering switch case,exception java.lang.NullPointerException,return from a call to int NullPointerExceptions.nullPointerExceptionWithExceptionHandling(boolean)]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionWithNullArrayParameter():void, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionWithNullArrayParameter(),start of procedure expectNotNullArrayParameter(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.expectNotNullArrayParameter(codetoanalyze.java.infer.NullPointerExceptions$A[]),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionWithNullArrayParameter()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionWithNullObjectParameter():void, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure nullPointerExceptionWithNullObjectParameter(),start of procedure expectNotNullObjectParameter(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.expectNotNullObjectParameter(NullPointerExceptions$A),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.nullPointerExceptionWithNullObjectParameter()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.preconditionCheckStateTest(codetoanalyze.java.infer.NullPointerExceptions$D):int, 1, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure preconditionCheckStateTest(...),Taking false branch]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.someNPEAfterResourceLeak():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure someNPEAfterResourceLeak(),start of procedure sourceOfNullWithResourceLeak(),start of procedure SomeResource(),return from a call to SomeResource.<init>(),return from a call to T CloseableAsResourceExample.sourceOfNullWithResourceLeak(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions.someNPEAfterResourceLeak()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP():void, 11, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure stringConstantEqualsFalseNotNPE_FP(),Taking true branch,Taking true branch,Taking true branch,return from a call to void NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.testSystemGetPropertyArgument():java.lang.String, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure testSystemGetPropertyArgument()]
codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.testSystemGetPropertyReturn():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure testSystemGetPropertyReturn(),Taking true branch,return from a call to void NullPointerExceptions.testSystemGetPropertyReturn()]
codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java, codetoanalyze.java.tracing.ArrayIndexOutOfBoundsExceptionExample.arrayIndexOutOfBoundsInCallee():void, 3, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure arrayIndexOutOfBoundsInCallee(),start of procedure withFixedIndex(...),start of procedure callMethodFromArray(...),Taking true branch,Taking true branch,Taking false branch,return from a call to void ArrayIndexOutOfBoundsExceptionExample.callMethodFromArray(codetoanalyze.java.tracing.T2[],int),return from a call to void ArrayIndexOutOfBoundsExceptionExample.withFixedIndex(codetoanalyze.java.tracing.T2[]),return from a call to void ArrayIndexOutOfBoundsExceptionExample.arrayIndexOutOfBoundsInCallee()]
codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java, codetoanalyze.java.tracing.ArrayIndexOutOfBoundsExceptionExample.callOutOfBound():void, 2, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure callOutOfBound()]
codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java, codetoanalyze.java.tracing.ArrayIndexOutOfBoundsExceptionExample.callOutOfBound():void, 3, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure callOutOfBound(),start of procedure callMethodFromArray(...),Taking true branch,exception java.lang.ArrayIndexOutOfBoundsException,return from a call to void ArrayIndexOutOfBoundsExceptionExample.callMethodFromArray(codetoanalyze.java.tracing.T2[],int),exception java.lang.ArrayIndexOutOfBoundsException,return from a call to void ArrayIndexOutOfBoundsExceptionExample.callOutOfBound()]
codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java, codetoanalyze.java.tracing.ArrayIndexOutOfBoundsExceptionExample.missingCheckOnIndex(codetoanalyze.java.tracing.T2[],int):void, 3, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure missingCheckOnIndex(...),Taking true branch,Taking true branch,Taking true branch]
codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java, codetoanalyze.java.tracing.ArrayIndexOutOfBoundsExceptionExample.missingCheckOnIndex(codetoanalyze.java.tracing.T2[],int):void, 6, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure missingCheckOnIndex(...),Taking false branch,return from a call to void ArrayIndexOutOfBoundsExceptionExample.missingCheckOnIndex(codetoanalyze.java.tracing.T2[],int)]
codetoanalyze/java/tracing/ClassCastExceptionExample.java, codetoanalyze.java.tracing.ClassCastExceptionExample.bar(int):codetoanalyze.java.tracing.S, 4, java.lang.ClassCastException, no_bucket, ERROR, [start of procedure bar(...),Taking false branch,return from a call to S ClassCastExceptionExample.bar(int)]
codetoanalyze/java/tracing/ClassCastExceptionExample.java, codetoanalyze.java.tracing.ClassCastExceptionExample.foo():void, 4, java.lang.ClassCastException, no_bucket, ERROR, [start of procedure foo(),start of procedure T2(),return from a call to T2.<init>(),start of procedure cast(...),exception java.lang.ClassCastException,return from a call to S ClassCastExceptionExample.cast(T2),exception java.lang.ClassCastException,return from a call to void ClassCastExceptionExample.foo()]
codetoanalyze/java/tracing/LazyDynamicDispatchExample.java, codetoanalyze.java.tracing.LazyDynamicDispatchExample.callWithSubtype():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure callWithSubtype(),start of procedure B(),start of procedure A(),return from a call to A.<init>(),return from a call to B.<init>(),start of procedure fromSupertype(...),Taking true branch,start of procedure get(),return from a call to T2 B.get(),return from a call to T2 LazyDynamicDispatchExample.fromSupertype(B),exception java.lang.NullPointerException,return from a call to void LazyDynamicDispatchExample.callWithSubtype()]
codetoanalyze/java/tracing/LazyDynamicDispatchExample.java, codetoanalyze.java.tracing.LazyDynamicDispatchExample.shouldReportLocalVarTypeIsKnown():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure shouldReportLocalVarTypeIsKnown(),start of procedure B(),start of procedure A(),return from a call to A.<init>(),return from a call to B.<init>(),start of procedure fromInterface(...),Taking true branch,start of procedure get(),return from a call to T2 B.get(),return from a call to T2 LazyDynamicDispatchExample.fromInterface(B),exception java.lang.NullPointerException,return from a call to void LazyDynamicDispatchExample.shouldReportLocalVarTypeIsKnown()]
codetoanalyze/java/tracing/LocallyDefinedExceptionExample.java, codetoanalyze.java.tracing.LocallyDefinedExceptionExample.fieldInvariant():void, 8, codetoanalyze.java.tracing.LocallyDefinedException, no_bucket, ERROR, [start of procedure fieldInvariant(),Taking false branch,return from a call to void LocallyDefinedExceptionExample.fieldInvariant()]
codetoanalyze/java/tracing/NullPointerExceptionExample.java, codetoanalyze.java.tracing.NullPointerExceptionExample.callDeref(codetoanalyze.java.tracing.T2,boolean):void, 4, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure callDeref(...),Taking false branch,return from a call to void NullPointerExceptionExample.callDeref(T2,boolean)]
codetoanalyze/java/tracing/NullPointerExceptionExample.java, codetoanalyze.java.tracing.NullPointerExceptionExample.callLeadToNpe():void, 2, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure callLeadToNpe(),start of procedure callDeref(...),Taking true branch,start of procedure deref(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.deref(T2),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.callDeref(T2,boolean),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.callLeadToNpe()]
codetoanalyze/java/tracing/NullPointerExceptionExample.java, codetoanalyze.java.tracing.NullPointerExceptionExample.npeOnBothBranches(int):void, 6, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure npeOnBothBranches(...),Taking true branch,Taking true branch,Taking true branch,start of procedure callDeref(...),Taking true branch,start of procedure deref(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.deref(T2),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.callDeref(T2,boolean),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.npeOnBothBranches(int)]
codetoanalyze/java/tracing/NullPointerExceptionExample.java, codetoanalyze.java.tracing.NullPointerExceptionExample.npeOnBothBranches(int):void, 6, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure npeOnBothBranches(...),Taking true branch,Taking true branch,Taking true branch,start of procedure callDeref(...),Taking true branch,start of procedure deref(...),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.deref(T2),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.callDeref(T2,boolean),exception java.lang.NullPointerException,return from a call to void NullPointerExceptionExample.npeOnBothBranches(int)]
codetoanalyze/java/tracing/ReportOnMainExample.java, codetoanalyze.java.tracing.ReportOnMainExample.main(java.lang.String[]):void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure main(...),start of procedure ReportOnMainExample(),return from a call to ReportOnMainExample.<init>(),Taking true branch,start of procedure foo(),Skipping test(): unknown method,Definition of test(),Taking true branch,Taking true branch,return from a call to void ReportOnMainExample.foo(),return from a call to void ReportOnMainExample.main(java.lang.String[])]
codetoanalyze/java/tracing/UnavoidableExceptionExample.java, codetoanalyze.java.tracing.UnavoidableExceptionExample.cannotAvoidNPE():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure cannotAvoidNPE(),start of procedure create(),return from a call to T2 UnavoidableExceptionExample.create(),exception java.lang.NullPointerException,return from a call to void UnavoidableExceptionExample.cannotAvoidNPE()]
codetoanalyze/java/tracing/UnavoidableExceptionExample.java, codetoanalyze.java.tracing.UnavoidableExceptionExample.unavoidableNPEWithParameter(boolean):void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure unavoidableNPEWithParameter(...),start of procedure create(),return from a call to T2 UnavoidableExceptionExample.create(),exception java.lang.NullPointerException,return from a call to void UnavoidableExceptionExample.unavoidableNPEWithParameter(boolean)]
codetoanalyze/java/tracing/UnavoidableExceptionExample.java, codetoanalyze.java.tracing.UnavoidableExceptionExample.virtualMethodWithUnavoidableNPE(boolean):void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure virtualMethodWithUnavoidableNPE(...),start of procedure create(),return from a call to T2 UnavoidableExceptionExample.create(),exception java.lang.NullPointerException,return from a call to void UnavoidableExceptionExample.virtualMethodWithUnavoidableNPE(boolean)]
Write Preview
Loading…
Cancel
Save