[biabduction] kill guarded by check

Summary: RacerD now has a check for this, so remove.

Reviewed By: jberdine

Differential Revision: D19974163

fbshipit-source-id: 06d7a203d

infer/man/man1/infer-full.txt

@@ -498,7 +498,6 @@ OPTIONS
            default),
              UNINITIALIZED_VALUE (enabled by default),
              UNREACHABLE_CODE (enabled by default),
-             UNSAFE_GUARDED_BY_ACCESS (enabled by default),
              UNTRUSTED_BUFFER_ACCESS (disabled by default),
              UNTRUSTED_DESERIALIZATION (enabled by default),
              UNTRUSTED_DESERIALIZATION_RISK (enabled by default),

infer/man/man1/infer-report.txt

@@ -227,7 +227,6 @@ OPTIONS
            default),
              UNINITIALIZED_VALUE (enabled by default),
              UNREACHABLE_CODE (enabled by default),
-             UNSAFE_GUARDED_BY_ACCESS (enabled by default),
              UNTRUSTED_BUFFER_ACCESS (disabled by default),
              UNTRUSTED_DESERIALIZATION (enabled by default),
              UNTRUSTED_DESERIALIZATION_RISK (enabled by default),

infer/man/man1/infer.txt

@@ -498,7 +498,6 @@ OPTIONS
            default),
              UNINITIALIZED_VALUE (enabled by default),
              UNREACHABLE_CODE (enabled by default),
-             UNSAFE_GUARDED_BY_ACCESS (enabled by default),
              UNTRUSTED_BUFFER_ACCESS (disabled by default),
              UNTRUSTED_DESERIALIZATION (enabled by default),
              UNTRUSTED_DESERIALIZATION_RISK (enabled by default),

infer/src/IR/Exceptions.ml

@@ -126,8 +126,6 @@ exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * L.
 
 exception Unknown_proc
 
-exception Unsafe_guarded_by_access of Localise.error_desc * L.ocaml_pos
-
 exception Wrong_argument_number of L.ocaml_pos
 
 type t =
@@ -525,13 +523,6 @@ let recognize_exception exn =
       ; visibility= Exn_developer
       ; severity= None
       ; category= Nocat }
-  | Unsafe_guarded_by_access (desc, ocaml_pos) ->
-      { name= IssueType.unsafe_guarded_by_access
-      ; description= desc
-      ; ocaml_pos= Some ocaml_pos
-      ; visibility= Exn_user
-      ; severity= None
-      ; category= Prover }
   | Wrong_argument_number ocaml_pos ->
       { name= IssueType.wrong_argument_number
       ; description= Localise.no_desc

infer/src/IR/Exceptions.mli

@@ -128,8 +128,6 @@ exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * Lo
 
 exception Unknown_proc
 
-exception Unsafe_guarded_by_access of Localise.error_desc * Logging.ocaml_pos
-
 exception Wrong_argument_number of Logging.ocaml_pos
 
 val severity_string : severity -> string

infer/src/IR/Localise.ml

@@ -309,25 +309,6 @@ let deref_str_array_bound size_opt index_opt =
   ; problem_str= "could be accessed with " ^ index_str ^ " out of bounds" }
 
 
-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 = Fieldname.to_string accessed_fld in
-  let annot_str = Printf.sprintf "@GuardedBy(\"%s\")" guarded_by_str in
-  let syncronized_str =
-    MF.monospaced_to_string (Printf.sprintf "synchronized(%s)" guarded_by_str)
-  in
-  let msg =
-    Format.asprintf
-      "The field %a is annotated with %a, but the lock %a is not held during the access to the \
-       field %s. Since the current method is non-private, it can be called from outside the \
-       current class without synchronization. Consider wrapping the access in a %s block or making \
-       the method private."
-      MF.pp_monospaced accessed_fld_str MF.pp_monospaced annot_str MF.pp_monospaced guarded_by_str
-      line_info syncronized_str
-  in
-  {no_desc with descriptions= [msg]}
-
-
 let desc_custom_error loc : error_desc =
   {no_desc with descriptions= ["detected"; at_line (Tags.create ()) loc]}
 

infer/src/IR/Localise.mli

@@ -158,8 +158,6 @@ val desc_inherently_dangerous_function : Procname.t -> error_desc
 val desc_unary_minus_applied_to_unsigned_expression :
   string option -> string -> Location.t -> error_desc
 
-val desc_unsafe_guarded_by_access : Fieldname.t -> string -> Location.t -> error_desc
-
 val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc
 
 val access_desc : access option -> string list

infer/src/base/Config.ml

@@ -168,9 +168,6 @@ let classnames_dir_name = "classnames"
 
 let costs_report_json = "costs-report.json"
 
-(** Experimental: if true do some specialized analysis of concurrent constructs. *)
-let csl_analysis = true
-
 let default_failure_name = "ASSERTION_FAILURE"
 
 let default_in_zip_results_dir = "infer"

infer/src/base/Config.mli

@@ -71,8 +71,6 @@ val classpath : string option
 
 val costs_report_json : string
 
-val csl_analysis : bool
-
 val default_failure_name : string
 
 val default_in_zip_results_dir : string

infer/src/base/IssueType.ml

@@ -468,8 +468,6 @@ let unknown_proc = register_from_string "Unknown_proc" ~hum:"Unknown Procedure"
 
 let unreachable_code_after = register_from_string "UNREACHABLE_CODE"
 
-let unsafe_guarded_by_access = register_from_string "UNSAFE_GUARDED_BY_ACCESS"
-
 let use_after_delete = register_from_string "USE_AFTER_DELETE"
 
 let use_after_free = register_from_string "USE_AFTER_FREE"

infer/src/base/IssueType.mli

@@ -320,8 +320,6 @@ val unknown_proc : t
 
 val unreachable_code_after : t
 
-val unsafe_guarded_by_access : t
-
 val use_after_delete : t
 
 val use_after_free : t

infer/src/biabduction/Rearrange.ml

@@ -701,336 +701,6 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
   Prop.prop_iter_set_state iter offsets_default
 
 
-(** If [lexp] is an access to a field that is annotated with @GuardedBy, add constraints to [prop]
-    expressing the safety conditions for the access. Complain if these conditions cannot be met. *)
-let add_guarded_by_constraints tenv prop lexp pdesc =
-  let lookup = Tenv.lookup tenv in
-  let pname = Procdesc.get_proc_name pdesc in
-  let excluded_guardedby_string str =
-    (* nothing with a space in it can be a valid Java expression, shouldn't warn *)
-    let is_invalid_exp_str str = String.contains str ' ' in
-    (* don't warn on @GuardedBy("ui_thread") in any form *)
-    let is_ui_thread str =
-      let lowercase_str = String.lowercase str in
-      String.equal lowercase_str "ui_thread"
-      || String.equal lowercase_str "ui-thread"
-      || String.equal lowercase_str "uithread"
-    in
-    is_invalid_exp_str str || is_ui_thread str
-  in
-  let guarded_by_str_is_this guarded_by_str = String.is_suffix ~suffix:"this" guarded_by_str in
-  let guarded_by_str_is_class guarded_by_str class_str =
-    let dollar_normalize s = String.map s ~f:(function '$' -> '.' | c -> c) in
-    String.is_suffix ~suffix:(dollar_normalize guarded_by_str)
-      (dollar_normalize (class_str ^ ".class"))
-  in
-  let guarded_by_str_is_current_class guarded_by_str = function
-    | Procname.Java java_pname ->
-        (* programmers write @GuardedBy("MyClass.class") when the field is guarded by the class *)
-        guarded_by_str_is_class guarded_by_str (Procname.Java.get_class_name java_pname)
-    | _ ->
-        false
-  in
-  let guarded_by_str_is_class_this class_name guarded_by_str =
-    let fully_qualified_this = Printf.sprintf "%s.this" class_name in
-    String.is_suffix ~suffix:guarded_by_str fully_qualified_this
-  in
-  (* return true if [guarded_by_str] is a suffix of "<name_of_super_class>.this" *)
-  let guarded_by_str_is_super_class_this guarded_by_str pname =
-    match pname with
-    | Procname.Java java_pname ->
-        let current_class_type_name = Procname.Java.get_class_type_name java_pname in
-        let comparison class_type_name _ =
-          guarded_by_str_is_class_this (Typ.Name.to_string class_type_name) guarded_by_str
-        in
-        PatternMatch.supertype_exists tenv comparison current_class_type_name
-    | _ ->
-        false
-  in
-  (* return true if [guarded_by_str] is as suffix of "<name_of_current_class>.this" *)
-  let guarded_by_str_is_current_class_this guarded_by_str = function
-    | Procname.Java java_pname ->
-        guarded_by_str_is_class_this (Procname.Java.get_class_name java_pname) guarded_by_str
-    | _ ->
-        false
-  in
-  let extract_guarded_by_str item_annot =
-    let annot_extract_guarded_by_str ((annot : Annot.t), _) =
-      if Annotations.annot_ends_with annot Annotations.guarded_by then
-        match annot.parameters with
-        | [Annot.{value= Str guarded_by_str}] when not (excluded_guardedby_string guarded_by_str) ->
-            Some guarded_by_str
-        | _ ->
-            None
-      else None
-    in
-    List.find_map ~f:annot_extract_guarded_by_str item_annot
-  in
-  let extract_suppress_warnings_str item_annot =
-    let annot_suppress_warnings_str ((annot : Annot.t), _) =
-      if Annotations.annot_ends_with annot Annotations.suppress_lint then
-        (* TODO: @SuppressLint's param is an array of strings, thus we need to match on
-           array. But generally logic here is still broken since it only expects 1 value. *)
-        match annot.parameters with
-        | [Annot.{value= Array [Str suppr_str; _]}] ->
-            Some suppr_str
-        | _ ->
-            None
-      else None
-    in
-    List.find_map ~f:annot_suppress_warnings_str item_annot
-  in
-  (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *)
-  let get_guarded_by_fld_str fld typ =
-    match Struct.get_field_type_and_annotation ~lookup fld typ with
-    | Some (_, item_annot) -> (
-      match extract_guarded_by_str item_annot with
-      | Some "this" ->
-          (* expand "this" into <classname>.this *)
-          Some (Printf.sprintf "%s.this" (Typ.Name.name (Fieldname.get_class_name fld)))
-      | guarded_by_str_opt ->
-          guarded_by_str_opt )
-    | _ ->
-        None
-  in
-  (* find A.guarded_by_fld_str |-> B and return Some B, or None if there is no such hpred *)
-  let find_guarded_by_exp guarded_by_str0 sigma =
-    let is_guarded_by_fld guarded_by_str fld _ =
-      (* this comparison needs to be somewhat fuzzy, since programmers are free to write
-         @GuardedBy("mLock"), @GuardedBy("MyClass.mLock"), or use other conventions *)
-      String.equal (Fieldname.get_field_name fld) guarded_by_str
-      || String.equal (Fieldname.to_string fld) guarded_by_str
-    in
-    let get_fld_strexp_and_typ typ f flds =
-      let match_one (fld, strexp) =
-        match Struct.get_field_type_and_annotation ~lookup fld typ with
-        | Some (fld_typ, _) when f fld fld_typ ->
-            Some (strexp, fld_typ)
-        | _ ->
-            None
-      in
-      List.find_map ~f:match_one flds
-    in
-    (* sometimes, programmers will write @GuardedBy("T.f") with the meaning "guarded by the field f
-       of the object of type T in the current state." note that this is ambiguous when there are
-       multiple objects of type T, but let's try to respect the intention *)
-    let match_on_field_type typ flds =
-      match String.rsplit2 guarded_by_str0 ~on:'.' with
-      | Some (class_part, field_part) -> (
-          let typ_matches_guarded_by _ {Typ.desc} =
-            match desc with
-            | Typ.Tptr (ptr_typ, _) ->
-                String.is_suffix ~suffix:class_part (Typ.to_string ptr_typ)
-            | _ ->
-                false
-          in
-          match get_fld_strexp_and_typ typ typ_matches_guarded_by flds with
-          | Some (Predicates.Eexp (matching_exp, _), _) ->
-              List.find_map
-                ~f:(function
-                  | Predicates.Hpointsto (lhs_exp, Estruct (matching_flds, _), Sizeof {typ= fld_typ})
-                    when Exp.equal lhs_exp matching_exp ->
-                      get_fld_strexp_and_typ fld_typ (is_guarded_by_fld field_part) matching_flds
-                  | _ ->
-                      None )
-                sigma
-          | _ ->
-              None )
-      | _ ->
-          None
-    in
-    List.find_map
-      ~f:(fun hpred ->
-        (* FIXME: silenced warning may be legit *)
-        match[@warning "-57"] hpred with
-        | Predicates.Hpointsto ((Const (Cclass clazz) as lhs_exp), _, Exp.Sizeof {typ})
-        | Predicates.Hpointsto
-            (_, Predicates.Eexp ((Const (Cclass clazz) as lhs_exp), _), Exp.Sizeof {typ})
-          when guarded_by_str_is_class guarded_by_str0 (Ident.name_to_string clazz) ->
-            Some (Predicates.Eexp (lhs_exp, Predicates.inst_none), typ)
-        | Predicates.Hpointsto (_, Estruct (flds, _), Exp.Sizeof {typ}) -> (
-          (* first, try to find a field that exactly matches the guarded-by string *)
-          match get_fld_strexp_and_typ typ (is_guarded_by_fld guarded_by_str0) flds with
-          | None when guarded_by_str_is_this guarded_by_str0 ->
-              (* if the guarded-by string is "OuterClass.this", look for "this$n" for some n.
-                 note that this is a bit sketchy when there are mutliple this$n's, but there's
-                 nothing we can do to disambiguate them. *)
-              get_fld_strexp_and_typ typ (fun f _ -> Fieldname.is_java_outer_instance f) flds
-          | None ->
-              (* can't find an exact match. try a different convention. *)
-              match_on_field_type typ flds
-          | Some _ as res_opt ->
-              res_opt )
-        | Predicates.Hpointsto (Lvar pvar, rhs_exp, Exp.Sizeof {typ})
-          when ( guarded_by_str_is_current_class_this guarded_by_str0 pname
-               || guarded_by_str_is_super_class_this guarded_by_str0 pname )
-               && Pvar.is_this pvar ->
-            Some (rhs_exp, typ)
-        | _ ->
-            None )
-      sigma
-  in
-  (* warn if the access to [lexp] is not protected by the [guarded_by_fld_str] lock *)
-  let enforce_guarded_access_ accessed_fld guarded_by_str prop =
-    (* return true if [pdesc] has an annotation that matches [guarded_by_str] *)
-    let proc_has_matching_annot pdesc guarded_by_str =
-      match extract_guarded_by_str (Annotations.pdesc_get_return_annot pdesc) with
-      | Some proc_guarded_by_str ->
-          (* the lock is not held, but the procedure is annotated with @GuardedBy *)
-          String.equal proc_guarded_by_str guarded_by_str
-      | None ->
-          false
-    in
-    let is_synchronized_on_class guarded_by_str =
-      guarded_by_str_is_current_class guarded_by_str pname
-      && Procdesc.is_java_synchronized pdesc
-      &&
-      match pname with Procname.Java java_pname -> Procname.Java.is_static java_pname | _ -> false
-    in
-    let warn accessed_fld guarded_by_str =
-      let loc = State.get_loc_exn () in
-      let err_desc = Localise.desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc in
-      let exn = Exceptions.Unsafe_guarded_by_access (err_desc, __POS__) in
-      Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn
-    in
-    let rec is_read_write_lock typ =
-      let str_is_read_write_lock str =
-        String.is_suffix ~suffix:"ReadWriteUpdateLock" str
-        || String.is_suffix ~suffix:"ReadWriteLock" str
-      in
-      match typ.Typ.desc with
-      | Typ.Tstruct name ->
-          str_is_read_write_lock (Typ.Name.name name)
-      | Typ.Tptr (typ, _) ->
-          is_read_write_lock typ
-      | _ ->
-          false
-    in
-    let has_lock guarded_by_exp =
-      ( guarded_by_str_is_current_class_this guarded_by_str pname
-      || guarded_by_str_is_super_class_this guarded_by_str pname )
-      && Procdesc.is_java_synchronized pdesc
-      || ( guarded_by_str_is_current_class guarded_by_str pname
-         && Procdesc.is_java_synchronized pdesc
-         &&
-         match pname with
-         | Procname.Java java_pname ->
-             Procname.Java.is_static java_pname
-         | _ ->
-             false )
-      || (* or the prop says we already have the lock *)
-      List.exists
-        ~f:(function Predicates.Apred (Alocked, _) -> true | _ -> false)
-        (Attribute.get_for_exp tenv prop guarded_by_exp)
-    in
-    let guardedby_is_self_referential =
-      String.equal "itself" (String.lowercase guarded_by_str)
-      || String.is_suffix ~suffix:guarded_by_str (Fieldname.to_string accessed_fld)
-    in
-    let proc_has_suppress_guarded_by_annot pdesc =
-      match extract_suppress_warnings_str (Annotations.pdesc_get_return_annot pdesc) with
-      | Some suppression_str ->
-          String.equal suppression_str "InvalidAccessToGuardedField"
-      | None ->
-          false
-    in
-    let should_warn pdesc =
-      (* adding this check implements "by reference" semantics for guarded-by rather than "by value"
-         semantics. if this access is through a local L or field V.f
-         (where f is not the @GuardedBy field!), we will not warn.
-      *)
-      let is_accessible_through_local_ref exp =
-        List.exists
-          ~f:(function
-            | Predicates.Hpointsto (Lvar _, Eexp (rhs_exp, _), _) ->
-                Exp.equal exp rhs_exp
-            | Predicates.Hpointsto (_, Estruct (flds, _), _) ->
-                List.exists
-                  ~f:(fun (fld, strexp) ->
-                    match strexp with
-                    | Predicates.Eexp (rhs_exp, _) ->
-                        Exp.equal exp rhs_exp && not (Fieldname.equal fld accessed_fld)
-                    | _ ->
-                        false )
-                  flds
-            | _ ->
-                false )
-          prop.Prop.sigma
-      in
-      (not (PredSymb.equal_access (Procdesc.get_access pdesc) Private))
-      && (not (Annotations.pdesc_return_annot_ends_with pdesc Annotations.visibleForTesting))
-      && (not
-            ( match Procdesc.get_proc_name pdesc with
-            | Procname.Java java_pname ->
-                Procname.Java.is_access_method java_pname
-            | _ ->
-                false ))
-      && (not (is_accessible_through_local_ref lexp))
-      && (not guardedby_is_self_referential)
-      && not (proc_has_suppress_guarded_by_annot pdesc)
-    in
-    match find_guarded_by_exp guarded_by_str prop.Prop.sigma with
-    | Some (Predicates.Eexp (guarded_by_exp, _), typ) ->
-        if is_read_write_lock typ then
-          (* TODO: model/understand read-write locks rather than ignoring them *)
-          prop
-        else if has_lock guarded_by_exp then
-          (* we have the lock; no need to add a proof obligation *)
-          (* TODO: materialize [fld], but don't add [fld] to the footprint. *)
-          prop
-        else if (* we don't know if we have the lock or not. *)
-                should_warn pdesc then (
-          (* non-private method; can't ensure that the lock is held. warn. *)
-          warn accessed_fld guarded_by_str ;
-          prop )
-        else
-          (* private method. add locked proof obligation to [pdesc] *)
-          Attribute.add tenv ~footprint:true prop Alocked [guarded_by_exp]
-    | _ ->
-        if
-          (not
-             ( proc_has_matching_annot pdesc guarded_by_str
-             || is_synchronized_on_class guarded_by_str ))
-          && should_warn pdesc
-        then
-          (* can't find the object the annotation refers to, and procedure is not annotated. warn *)
-          warn accessed_fld guarded_by_str
-        else
-          (* procedure has same GuardedBy annotation as the field. we would like to add a proof
-             obligation, but we can't (because we can't find an expression corresponding to the
-             lock in the current prop). so just be silent. *)
-          () ;
-        prop
-  in
-  let enforce_guarded_access fld typ prop =
-    match get_guarded_by_fld_str fld typ with
-    | Some guarded_by_fld_str ->
-        enforce_guarded_access_ fld guarded_by_fld_str prop
-    | None ->
-        prop
-  in
-  let check_fld_locks typ prop_acc (fld, strexp) =
-    match strexp with
-    | Predicates.Eexp (exp, _) when Exp.equal exp lexp ->
-        enforce_guarded_access fld typ prop_acc
-    | _ ->
-        prop_acc
-  in
-  let hpred_check_flds prop_acc = function
-    | Predicates.Hpointsto (_, Estruct (flds, _), Sizeof {typ}) ->
-        List.fold ~f:(check_fld_locks typ) ~init:prop_acc flds
-    | _ ->
-        prop_acc
-  in
-  match lexp with
-  | Exp.Lfield (_, fld, typ) ->
-      (* check for direct access to field annotated with @GuardedBy *)
-      enforce_guarded_access fld typ prop
-  | _ ->
-      (* check for access via alias *)
-      List.fold ~f:hpred_check_flds ~init:prop prop.Prop.sigma
-
-
 (** Add a pointsto for [root(lexp): typ] to the iterator and to the
     footprint, if it's compatible with the allowed footprint
     variables. This function ensures that [root(lexp): typ] is the
@@ -1724,22 +1394,12 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
   L.d_ln () ;
   if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc_exn ()) ;
   let pname = Procdesc.get_proc_name pdesc in
-  let prop' =
-    match pname with
-    | Procname.Java java_pname
-      when Config.csl_analysis && !BiabductionConfig.footprint
-           && not (Procname.is_constructor pname || Procname.Java.is_class_initializer java_pname)
-      ->
-        add_guarded_by_constraints tenv prop lexp pdesc
-    | _ ->
-        prop
-  in
-  match Prop.prop_iter_create prop' with
+  match Prop.prop_iter_create prop with
   | None ->
       if !BiabductionConfig.footprint then
-        [prop_iter_add_hpred_footprint_to_prop pname tenv prop' (nlexp, typ) inst]
+        [prop_iter_add_hpred_footprint_to_prop pname tenv prop (nlexp, typ) inst]
       else (
         pp_rearrangement_error "sigma is empty" prop nlexp ;
         raise (Exceptions.Symexec_memory_error __POS__) )
   | Some iter ->
-      iter_rearrange pname tenv nlexp typ prop' iter inst
+      iter_rearrange pname tenv nlexp typ prop iter inst

infer/src/checkers/annotations.mli

@@ -114,9 +114,6 @@ val ia_is_worker_thread : Annot.Item.t -> bool
 
 val ia_is_uithread_equivalent : Annot.Item.t -> bool
 
-val pdesc_get_return_annot : Procdesc.t -> Annot.Item.t
-(** get the list of annotations on the return value of [pdesc] *)
-
 val pdesc_has_return_annot : Procdesc.t -> (Annot.Item.t -> bool) -> bool
 (** return true if the given predicate evaluates to true on the annotation of [pdesc]'s return value *)
 

infer/tests/build_systems/ant/issues.exp

@@ -50,46 +50,26 @@ codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.
 codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.gzipOutputStreamNotClosedAfterFlush():void, 4, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure gzipOutputStreamNotClosedAfterFlush(),exception java.io.IOException]
 codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.inflaterOutputStreamNotClosedAfterWrite():void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure inflaterOutputStreamNotClosedAfterWrite(),exception java.io.IOException]
 codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.printStreamNotClosedAfterWrite():void, 5, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure printStreamNotClosedAfterWrite()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$3.readFromInnerClassBad1():java.lang.String, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad1()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$4.readFromInnerClassBad2():java.lang.String, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad2()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$Sub.badSub():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badSub()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$Sub.badSub():void, 491, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Write on unknown thread>,access to `this.xForSub`,<Write on background thread>,access to `this.xForSub`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByNormalLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByNormalLock()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByNormalLock():void, 526, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Write on unknown thread>,access to `this.guardedbynl`,<Write on background thread>,access to `this.guardedbynl`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByReentrantLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByReentrantLock()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByReentrantLock():void, 530, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Write on unknown thread>,access to `this.guardedbyrel`,<Write on background thread>,access to `this.guardedbyrel`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.byRefTrickyBad():java.lang.Object, 4, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure byRefTrickyBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.byRefTrickyBad():java.lang.Object, 281, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.g`,<Write trace>,access to `this.g`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 573, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Write on unknown thread>,access to `this.guardedByLock1`,<Write on background thread>,access to `this.guardedByLock1`]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 574, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Write on unknown thread>,access to `this.guardedByLock2`,<Write on background thread>,access to `this.guardedByLock2`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFAfterBlockBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFAfterBlockBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBad():void, 66, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadButSuppressed():void, 71, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadButSuppressedOther():void, 76, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongAnnotation():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongAnnotation()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongAnnotation():void, 109, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongLock()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongLock():void, 85, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFOkMethodAnnotated():void, 114, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFOkSynchronized():void, 127, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readGFromCopyOk():void, 267, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.mCopyOfG`,<Write trace>,access to `this.mCopyOfG`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBadSynchronizedMethodShouldntHelp():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBadSynchronizedMethodShouldntHelp()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.reassignCopyOk():void, 149, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.mCopyOfG`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodReadBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodReadBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodReadBad():void, 138, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodWriteBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodWriteBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedOnThisBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedOnThisBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedOnThisBad():void, 205, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `infer.GuardedByExample.sGuardedByClass`,<Write trace>,access to `infer.GuardedByExample.sGuardedByClass`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFAfterBlockBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFAfterBlockBad():void, 104, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBad()]
 codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBad():void, 80, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Write on unknown thread>,access to `this.f`,<Write on background thread>,access to `this.f`]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBadWrongLock()]
 codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure getAfterClearBad()]
 codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure getAfterRemovingTheKeyBad()]
 codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getFromKeySetGood_FP(java.util.HashMap):void, 1, INEFFICIENT_KEYSET_ITERATOR, no_bucket, ERROR, [Accessing a value using a key that was retrieved from a `keySet` iterator. It is more efficient to use an iterator on the `entrySet` of the map, avoiding the extra `HashMap.get(key)` lookup.]

infer/tests/codetoanalyze/java/infer/issues.exp

@@ -72,26 +72,6 @@ codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.
 codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.gzipOutputStreamNotClosedAfterFlush():void, 4, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure gzipOutputStreamNotClosedAfterFlush(),exception java.io.IOException]
 codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.inflaterOutputStreamNotClosedAfterWrite():void, 7, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure inflaterOutputStreamNotClosedAfterWrite(),exception java.io.IOException]
 codetoanalyze/java/infer/FilterOutputStreamLeaks.java, codetoanalyze.java.infer.FilterOutputStreamLeaks.printStreamNotClosedAfterWrite():void, 5, RESOURCE_LEAK, no_bucket, ERROR, [start of procedure printStreamNotClosedAfterWrite()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$3.readFromInnerClassBad1():java.lang.String, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad1()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$4.readFromInnerClassBad2():java.lang.String, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFromInnerClassBad2()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample$Sub.badSub():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badSub()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByNormalLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByNormalLock()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.badGuardedByReentrantLock():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure badGuardedByReentrantLock()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.byRefTrickyBad():java.lang.Object, 4, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure byRefTrickyBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.guardedByTypeSyntaxBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure guardedByTypeSyntaxBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFAfterBlockBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongAnnotation():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongAnnotation()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readFBadWrongLock()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBad():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.readHBadSynchronizedMethodShouldntHelp():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure readHBadSynchronizedMethodShouldntHelp()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodReadBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodReadBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedMethodWriteBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedMethodWriteBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.synchronizedOnThisBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure synchronizedOnThisBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFAfterBlockBad():void, 2, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFAfterBlockBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBad():void, 0, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBad()]
-codetoanalyze/java/infer/GuardedByExample.java, codetoanalyze.java.infer.GuardedByExample.writeFBadWrongLock():void, 1, UNSAFE_GUARDED_BY_ACCESS, no_bucket, ERROR, [start of procedure writeFBadWrongLock()]
 codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure getAfterClearBad()]
 codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure getAfterRemovingTheKeyBad()]
 codetoanalyze/java/infer/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getFromKeySetGood_FP(java.util.HashMap):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure getFromKeySetGood_FP(...),Taking true branch]