diff --git a/Makefile b/Makefile
index 00d0d4d55..71d53b4cb 100644
--- a/Makefile
+++ b/Makefile
@@ -163,7 +163,6 @@ DIRECT_TESTS += \
   java_racerd \
   java_starvation \
   java_topl \
-  java_tracing \
 
 ifeq ($(IS_FACEBOOK_TREE),yes)
 DIRECT_TESTS += java_fb-performance
diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt
index 608ebb323..196ee4964 100644
--- a/infer/man/man1/infer-full.txt
+++ b/infer/man/man1/infer-full.txt
@@ -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
 
diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml
index 6c3c5af9b..e9961e352 100644
--- a/infer/src/IR/Localise.ml
+++ b/infer/src/IR/Localise.ml
@@ -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
diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli
index 25020cf2b..707d4d72d 100644
--- a/infer/src/IR/Localise.mli
+++ b/infer/src/IR/Localise.mli
@@ -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 *)
 
diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml
index e7cad8017..68409cd75 100644
--- a/infer/src/absint/PatternMatch.ml
+++ b/infer/src/absint/PatternMatch.ml
@@ -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"
 
diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli
index b2e4e90f9..dbe2ab4f5 100644
--- a/infer/src/absint/PatternMatch.mli
+++ b/infer/src/absint/PatternMatch.mli
@@ -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*)
diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml
index d028bd40c..d4091523f 100644
--- a/infer/src/base/Config.ml
+++ b/infer/src/base/Config.ml
@@ -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
diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli
index 24df99b3d..26005c38a 100644
--- a/infer/src/base/Config.mli
+++ b/infer/src/base/Config.mli
@@ -704,8 +704,6 @@ val trace_rearrange : bool
 
 val trace_topl : bool
 
-val tracing : bool
-
 val tv_commit : string option
 
 val tv_limit : int
diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml
index 5715168c0..5b3a850c5 100644
--- a/infer/src/biabduction/Abs.ml
+++ b/infer/src/biabduction/Abs.ml
@@ -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 ->
diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml
index 4aae3aeeb..16355a503 100644
--- a/infer/src/biabduction/SymExec.ml
+++ b/infer/src/biabduction/SymExec.ml
@@ -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
diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml
index b476909ce..7f5d91d6c 100644
--- a/infer/src/biabduction/interproc.ml
+++ b/infer/src/biabduction/interproc.ml
@@ -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
 
 
diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml
index 35ad91ad0..5fcc4f272 100644
--- a/infer/src/checkers/annotations.ml
+++ b/infer/src/checkers/annotations.ml
@@ -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
diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli
index a3c2a929c..5871d2c00 100644
--- a/infer/src/checkers/annotations.mli
+++ b/infer/src/checkers/annotations.mli
@@ -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
diff --git a/infer/src/java/jConfig.ml b/infer/src/java/jConfig.ml
index fe3aa65d5..a8882e817 100644
--- a/infer/src/java/jConfig.ml
+++ b/infer/src/java/jConfig.ml
@@ -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
diff --git a/infer/src/java/jConfig.mli b/infer/src/java/jConfig.mli
index 7494728ca..98c9a200b 100644
--- a/infer/src/java/jConfig.mli
+++ b/infer/src/java/jConfig.mli
@@ -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
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index 41c3269be..46627fd40 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -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
diff --git a/infer/tests/codetoanalyze/java/tracing/.inferconfig b/infer/tests/codetoanalyze/java/tracing/.inferconfig
deleted file mode 100644
index 85ac12b5b..000000000
--- a/infer/tests/codetoanalyze/java/tracing/.inferconfig
+++ /dev/null
@@ -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_"
-    }
-  ]
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java
deleted file mode 100644
index 6f9772bfd..000000000
--- a/infer/tests/codetoanalyze/java/tracing/ArrayIndexOutOfBoundsExceptionExample.java
+++ /dev/null
@@ -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);
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/ArrayOutOfBounds.java b/infer/tests/codetoanalyze/java/tracing/ArrayOutOfBounds.java
deleted file mode 120000
index 4834b4d54..000000000
--- a/infer/tests/codetoanalyze/java/tracing/ArrayOutOfBounds.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/ArrayOutOfBounds.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/ClassCastExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/ClassCastExceptionExample.java
deleted file mode 100644
index 719d20369..000000000
--- a/infer/tests/codetoanalyze/java/tracing/ClassCastExceptionExample.java
+++ /dev/null
@@ -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;
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/ClassCastExceptions.java b/infer/tests/codetoanalyze/java/tracing/ClassCastExceptions.java
deleted file mode 120000
index d3bc93083..000000000
--- a/infer/tests/codetoanalyze/java/tracing/ClassCastExceptions.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/ClassCastExceptions.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/CloseableAsResourceExample.java b/infer/tests/codetoanalyze/java/tracing/CloseableAsResourceExample.java
deleted file mode 120000
index 1410eb022..000000000
--- a/infer/tests/codetoanalyze/java/tracing/CloseableAsResourceExample.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/CloseableAsResourceExample.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java b/infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java
deleted file mode 100644
index c4a5478d8..000000000
--- a/infer/tests/codetoanalyze/java/tracing/LazyDynamicDispatchExample.java
+++ /dev/null
@@ -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();
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/LocallyDefinedExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/LocallyDefinedExceptionExample.java
deleted file mode 100644
index b088cf533..000000000
--- a/infer/tests/codetoanalyze/java/tracing/LocallyDefinedExceptionExample.java
+++ /dev/null
@@ -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;
-      }
-    }
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/Makefile b/infer/tests/codetoanalyze/java/tracing/Makefile
deleted file mode 100644
index defde903d..000000000
--- a/infer/tests/codetoanalyze/java/tracing/Makefile
+++ /dev/null
@@ -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
diff --git a/infer/tests/codetoanalyze/java/tracing/NeverNullSource.java b/infer/tests/codetoanalyze/java/tracing/NeverNullSource.java
deleted file mode 120000
index 321604bad..000000000
--- a/infer/tests/codetoanalyze/java/tracing/NeverNullSource.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/NeverNullSource.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java
deleted file mode 100644
index 2f5814d14..000000000
--- a/infer/tests/codetoanalyze/java/tracing/NullPointerExceptionExample.java
+++ /dev/null
@@ -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);
-    }
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/tracing/NullPointerExceptions.java
deleted file mode 120000
index 6396d3f82..000000000
--- a/infer/tests/codetoanalyze/java/tracing/NullPointerExceptions.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/NullPointerExceptions.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/ReportOnMainExample.java b/infer/tests/codetoanalyze/java/tracing/ReportOnMainExample.java
deleted file mode 100644
index 19345b5d4..000000000
--- a/infer/tests/codetoanalyze/java/tracing/ReportOnMainExample.java
+++ /dev/null
@@ -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();
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/SkippedSourceFile.java b/infer/tests/codetoanalyze/java/tracing/SkippedSourceFile.java
deleted file mode 120000
index f5238c9ef..000000000
--- a/infer/tests/codetoanalyze/java/tracing/SkippedSourceFile.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/SkippedSourceFile.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/SomeLibrary.java b/infer/tests/codetoanalyze/java/tracing/SomeLibrary.java
deleted file mode 120000
index 69f36e7ae..000000000
--- a/infer/tests/codetoanalyze/java/tracing/SomeLibrary.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/SomeLibrary.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/T.java b/infer/tests/codetoanalyze/java/tracing/T.java
deleted file mode 120000
index 41bf7ace8..000000000
--- a/infer/tests/codetoanalyze/java/tracing/T.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/T.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/T2.java b/infer/tests/codetoanalyze/java/tracing/T2.java
deleted file mode 100644
index 4bde6b12e..000000000
--- a/infer/tests/codetoanalyze/java/tracing/T2.java
+++ /dev/null
@@ -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() {}
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/UnavoidableExceptionExample.java b/infer/tests/codetoanalyze/java/tracing/UnavoidableExceptionExample.java
deleted file mode 100644
index 89070d844..000000000
--- a/infer/tests/codetoanalyze/java/tracing/UnavoidableExceptionExample.java
+++ /dev/null
@@ -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();
-  }
-}
diff --git a/infer/tests/codetoanalyze/java/tracing/Utils.java b/infer/tests/codetoanalyze/java/tracing/Utils.java
deleted file mode 120000
index f39bb1c18..000000000
--- a/infer/tests/codetoanalyze/java/tracing/Utils.java
+++ /dev/null
@@ -1 +0,0 @@
-../infer/Utils.java
\ No newline at end of file
diff --git a/infer/tests/codetoanalyze/java/tracing/issues.exp b/infer/tests/codetoanalyze/java/tracing/issues.exp
deleted file mode 100644
index 6bfbeeab9..000000000
--- a/infer/tests/codetoanalyze/java/tracing/issues.exp
+++ /dev/null
@@ -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)]