[racerd] stop reporting on locals

Summary: There has never been a sufficient formal basis for soundness nor completeness of reports on locals.  This diff changes the domain to effectively concern only expressions rooted at formals or globals.

Reviewed By: ezgicicek

Differential Revision: D19769201

fbshipit-source-id: 36ae04d8c

infer/src/concurrency/RacerD.ml

@@ -23,10 +23,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = RacerDDomain
 
-  type extras = ProcData.no_extras
+  type extras = FormalMap.t
 
-  let add_access loc ~is_write_access locks threads ownership (proc_data : extras ProcData.t)
-      access_domain exp =
+  let add_access formals loc ~is_write_access locks threads ownership
+      (proc_data : extras ProcData.t) access_domain exp =
     let open Domain in
     let rec add_field_accesses prefix_path acc = function
       | [] ->
@@ -41,7 +41,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let is_write = List.is_empty access_list && is_write_access in
             let access = TraceElem.make_field_access prefix_path' ~is_write loc in
             let pre = OwnershipDomain.get_precondition prefix_path ownership in
-            let snapshot_opt = AccessSnapshot.make access locks threads pre in
+            let snapshot_opt = AccessSnapshot.make formals access locks threads pre in
             let access_acc' = AccessDomain.add_opt snapshot_opt acc in
             add_field_accesses prefix_path' access_acc' access_list
     in
@@ -50,7 +50,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         add_field_accesses base acc accesses )
 
 
-  let make_container_access ret_base callee_pname ~is_write receiver_ap callee_loc tenv
+  let make_container_access formals ret_base callee_pname ~is_write receiver_ap callee_loc tenv
       (astate : Domain.t) =
     let open Domain in
     if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then None
@@ -60,7 +60,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc
         in
         let ownership_pre = OwnershipDomain.get_precondition receiver_ap astate.ownership in
-        AccessSnapshot.make container_access astate.locks astate.threads ownership_pre
+        AccessSnapshot.make formals container_access astate.locks astate.threads ownership_pre
       in
       let ownership_value = OwnershipDomain.get_owned receiver_ap astate.ownership in
       let ownership =
@@ -70,15 +70,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       Some {astate with accesses; ownership}
 
 
-  let add_reads exps loc ({accesses; locks; threads; ownership} as astate : Domain.t) proc_data =
+  let add_reads formals exps loc ({accesses; locks; threads; ownership} as astate : Domain.t)
+      proc_data =
     let accesses' =
       List.fold exps ~init:accesses
-        ~f:(add_access loc ~is_write_access:false locks threads ownership proc_data)
+        ~f:(add_access formals loc ~is_write_access:false locks threads ownership proc_data)
     in
     {astate with accesses= accesses'}
 
 
-  let expand_actuals actuals accesses pdesc =
+  let expand_actuals formals actuals accesses pdesc =
     let open Domain in
     if AccessDomain.is_empty accesses then accesses
     else
@@ -108,13 +109,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
       in
       let add snapshot acc =
         let access' = TraceElem.map ~f:expand_exp snapshot.AccessSnapshot.access in
-        let snapshot_opt' = AccessSnapshot.make_from_snapshot access' snapshot in
+        let snapshot_opt' = AccessSnapshot.make_from_snapshot formals access' snapshot in
         AccessDomain.add_opt snapshot_opt' acc
       in
       AccessDomain.fold add accesses AccessDomain.empty
 
 
-  let add_callee_accesses (caller_astate : Domain.t) callee_accesses locks threads actuals
+  let add_callee_accesses formals (caller_astate : Domain.t) callee_accesses locks threads actuals
       callee_pname loc =
     let open Domain in
     let conjoin_ownership_precondition actual_indexes actual_exp :
@@ -166,7 +167,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         (* discard accesses to owned memory *)
         acc
       else
-        let snapshot_opt = AccessSnapshot.make access locks thread ownership_precondition in
+        let snapshot_opt = AccessSnapshot.make formals access locks thread ownership_precondition in
         AccessDomain.add_opt snapshot_opt acc
     in
     AccessDomain.fold update_callee_access callee_accesses caller_astate.accesses
@@ -220,11 +221,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     else astate
 
 
-  let treat_call_acquiring_ownership ret_base procname actuals loc ({ProcData.tenv} as proc_data)
-      astate () =
+  let treat_call_acquiring_ownership ret_base procname actuals loc
+      ({ProcData.tenv; extras} as proc_data) astate () =
     let open Domain in
     if RacerDModels.acquires_ownership procname tenv then
-      let astate = add_reads actuals loc astate proc_data in
+      let astate = add_reads extras actuals loc astate proc_data in
       let ownership =
         OwnershipDomain.add (AccessExpression.base ret_base) OwnershipAbstractValue.owned
           astate.ownership
@@ -233,7 +234,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     else None
 
 
-  let treat_container_accesses ret_base callee_pname actuals loc {ProcData.tenv} astate () =
+  let treat_container_accesses ret_base callee_pname actuals loc {ProcData.tenv; extras} astate () =
     let open RacerDModels in
     Option.bind (get_container_access callee_pname tenv) ~f:(fun container_access ->
         match List.hd actuals with
@@ -241,14 +242,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             let is_write =
               match container_access with ContainerWrite -> true | ContainerRead -> false
             in
-            make_container_access ret_base callee_pname ~is_write receiver_expr loc tenv astate
+            make_container_access extras ret_base callee_pname ~is_write receiver_expr loc tenv
+              astate
         | _ ->
             L.internal_error "Call to %a is marked as a container write, but has no receiver"
               Procname.pp callee_pname ;
             None )
 
 
-  let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; summary}
+  let do_proc_call ret_base callee_pname actuals call_flags loc {ProcData.tenv; summary; extras}
       (astate : Domain.t) () =
     let open Domain in
     let open RacerDModels in
@@ -256,7 +258,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     let ret_access_exp = AccessExpression.base ret_base in
     let astate =
       if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then
-        Domain.add_unannotated_call_access callee_pname loc astate
+        Domain.add_unannotated_call_access extras callee_pname loc astate
       else astate
     in
     let astate =
@@ -311,7 +313,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               |> Option.map ~f:(fun summary ->
                      let rebased_accesses =
                        Ondemand.get_proc_desc callee_pname
-                       |> Option.fold ~init:summary.accesses ~f:(expand_actuals actuals)
+                       |> Option.fold ~init:summary.accesses ~f:(expand_actuals extras actuals)
                      in
                      {summary with accesses= rebased_accesses} )
             in
@@ -321,7 +323,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks
                 in
                 let accesses =
-                  add_callee_accesses astate accesses locks threads actuals callee_pname loc
+                  add_callee_accesses extras astate accesses locks threads actuals callee_pname loc
                 in
                 let ownership =
                   OwnershipDomain.propagate_return ret_access_exp return_ownership actuals
@@ -355,11 +357,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     {astate_callee with ownership; attribute_map}
 
 
-  let do_assignment lhs_access_exp rhs_exp loc ({ProcData.tenv} as proc_data) (astate : Domain.t) =
+  let do_assignment lhs_access_exp rhs_exp loc ({ProcData.tenv; extras} as proc_data)
+      (astate : Domain.t) =
     let open Domain in
     let rhs_accesses =
-      add_access loc ~is_write_access:false astate.locks astate.threads astate.ownership proc_data
-        astate.accesses rhs_exp
+      add_access extras loc ~is_write_access:false astate.locks astate.threads astate.ownership
+        proc_data astate.accesses rhs_exp
     in
     let rhs_access_exprs = HilExp.get_access_exprs rhs_exp in
     let is_functional =
@@ -382,8 +385,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
            report spurious read/write races *)
         rhs_accesses
       else
-        add_access loc ~is_write_access:true astate.locks astate.threads astate.ownership proc_data
-          rhs_accesses (HilExp.AccessExpression lhs_access_exp)
+        add_access extras loc ~is_write_access:true astate.locks astate.threads astate.ownership
+          proc_data rhs_accesses (HilExp.AccessExpression lhs_access_exp)
     in
     let ownership = OwnershipDomain.propagate_assignment lhs_access_exp rhs_exp astate.ownership in
     let attribute_map =
@@ -392,7 +395,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     {astate with accesses; ownership; attribute_map}
 
 
-  let do_assume assume_exp loc proc_data (astate : Domain.t) =
+  let do_assume formals assume_exp loc proc_data (astate : Domain.t) =
     let open Domain in
     let add_choice bool_value (acc : Domain.t) = function
       | Choice.LockHeld ->
@@ -408,8 +411,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           {acc with threads}
     in
     let accesses =
-      add_access loc ~is_write_access:false astate.locks astate.threads astate.ownership proc_data
-        astate.accesses assume_exp
+      add_access formals loc ~is_write_access:false astate.locks astate.threads astate.ownership
+        proc_data astate.accesses assume_exp
     in
     let astate' =
       match HilExp.get_access_exprs assume_exp with
@@ -426,10 +429,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     {astate' with accesses}
 
 
-  let exec_instr (astate : Domain.t) ({ProcData.summary} as proc_data) _ (instr : HilInstr.t) =
+  let exec_instr (astate : Domain.t) ({ProcData.summary; extras} as proc_data) _
+      (instr : HilInstr.t) =
     match instr with
     | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
-        let astate = add_reads actuals loc astate proc_data in
+        let astate = add_reads extras actuals loc astate proc_data in
         treat_call_acquiring_ownership ret_base callee_pname actuals loc proc_data astate ()
         |> IOption.if_none_evalopt
              ~f:(treat_container_accesses ret_base callee_pname actuals loc proc_data astate)
@@ -442,7 +446,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Assign (lhs_access_expr, rhs_exp, loc) ->
         do_assignment lhs_access_expr rhs_exp loc proc_data astate
     | Assume (assume_exp, _, _, loc) ->
-        do_assume assume_exp loc proc_data astate
+        do_assume extras assume_exp loc proc_data astate
     | Metadata _ ->
         astate
 
@@ -465,7 +469,7 @@ let analyze_procedure {Callbacks.exe_env; summary} =
   let open RacerDDomain in
   if should_analyze_proc tenv proc_name then
     let formal_map = FormalMap.make proc_desc in
-    let proc_data = ProcData.make summary tenv ProcData.empty_extras in
+    let proc_data = ProcData.make summary tenv (FormalMap.make proc_desc) in
     let initial =
       let locks =
         if Procdesc.is_java_synchronized proc_desc then LocksDomain.(acquire_lock bottom)

infer/src/concurrency/RacerDDomain.ml

@@ -65,6 +65,19 @@ module Access = struct
         None
 
 
+  let should_keep formals access =
+    match get_access_exp access with
+    | None ->
+        true
+    | Some acc_exp -> (
+        let ((root, _) as base) = AccessExpression.get_base acc_exp in
+        match root with
+        | Var.LogicalVar _ ->
+            false
+        | Var.ProgramVar pvar ->
+            Pvar.is_global pvar || FormalMap.is_formal base formals )
+
+
   let map ~f access =
     match access with
     | Read {exp} ->
@@ -127,6 +140,8 @@ module TraceElem = struct
 
   let is_container_write {elem} = Access.is_container_write elem
 
+  let should_keep formals {elem} = Access.should_keep formals elem
+
   let map ~f trace_elem = map ~f:(Access.map ~f) trace_elem
 
   let make_container_access access_exp pname ~is_write loc =
@@ -268,19 +283,21 @@ module AccessSnapshot = struct
     ; ownership_precondition: OwnershipPrecondition.t }
   [@@deriving compare]
 
-  let make_if_not_owned access lock thread ownership_precondition =
-    if not (OwnershipPrecondition.is_true ownership_precondition) then
-      Some {access; lock; thread; ownership_precondition}
+  let make_if_not_owned formals access lock thread ownership_precondition =
+    if
+      (not (OwnershipPrecondition.is_true ownership_precondition))
+      && TraceElem.should_keep formals access
+    then Some {access; lock; thread; ownership_precondition}
     else None
 
 
-  let make access lock thread ownership_precondition =
+  let make formals access lock thread ownership_precondition =
     let lock = LocksDomain.is_locked lock in
-    make_if_not_owned access lock thread ownership_precondition
+    make_if_not_owned formals access lock thread ownership_precondition
 
 
-  let make_from_snapshot access {lock; thread; ownership_precondition} =
-    make_if_not_owned access lock thread ownership_precondition
+  let make_from_snapshot formals access {lock; thread; ownership_precondition} =
+    make_if_not_owned formals access lock thread ownership_precondition
 
 
   let is_unprotected {thread; lock; ownership_precondition} =
@@ -579,7 +596,7 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map} =
     ownership AttributeMapDomain.pp attribute_map
 
 
-let add_unannotated_call_access pname loc (astate : t) =
+let add_unannotated_call_access formals pname loc (astate : t) =
   let access = TraceElem.make_unannotated_call_access pname loc in
-  let snapshot = AccessSnapshot.make access astate.locks astate.threads False in
+  let snapshot = AccessSnapshot.make formals access astate.locks astate.threads False in
   {astate with accesses= AccessDomain.add_opt snapshot astate.accesses}

infer/src/concurrency/RacerDDomain.mli

@@ -107,9 +107,15 @@ module AccessSnapshot : sig
 
   include PrettyPrintable.PrintableOrderedType with type t := t
 
-  val make : TraceElem.t -> LocksDomain.t -> ThreadsDomain.t -> OwnershipPrecondition.t -> t option
+  val make :
+       FormalMap.t
+    -> TraceElem.t
+    -> LocksDomain.t
+    -> ThreadsDomain.t
+    -> OwnershipPrecondition.t
+    -> t option
 
-  val make_from_snapshot : TraceElem.t -> t -> t option
+  val make_from_snapshot : FormalMap.t -> TraceElem.t -> t -> t option
 
   val is_unprotected : t -> bool
   (** return true if not protected by lock, thread, or ownership *)
@@ -218,4 +224,4 @@ include AbstractDomain.WithBottom with type t := t
 
 val pp_summary : F.formatter -> summary -> unit
 
-val add_unannotated_call_access : Procname.t -> Location.t -> t -> t
+val add_unannotated_call_access : FormalMap.t -> Procname.t -> Location.t -> t -> t

infer/tests/codetoanalyze/cpp/racerd/issues.exp

@@ -8,8 +8,6 @@ codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::call1, 51, LOC
 codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`]
 codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`]
 codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic::test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`,<Write trace>,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`]
-codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership::test2_bad, 49, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `x->f`,<Write trace>,access to `x->f`]
-codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership::test3_bad, 65, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `x->f`,<Write trace>,access to `x->f`]
 codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::get2, 34, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_written`,<Write trace>,access to `this->suspiciously_written`]
 codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::get4, 40, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]
 codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::test1, 44, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this->suspiciously_read`,<Write trace>,access to `this->suspiciously_read`]

infer/tests/codetoanalyze/cpp/racerd/locals_ownership.cpp

@@ -41,7 +41,7 @@ class Ownership {
     return x.f;
   }
 
-  int test2_bad() {
+  int FN_test2_bad() {
     X* x = &current;
     mutex_.lock();
     x->f = 7;
@@ -57,7 +57,7 @@ class Ownership {
     return x.f;
   }
 
-  int test3_bad(X* xformal) {
+  int FN_test3_bad(X* xformal) {
     X* x = xformal;
     mutex_.lock();
     x->f = 7;

infer/tests/codetoanalyze/java/racerd/DeepOwnership.java

@@ -16,7 +16,7 @@ class DeepOwnership {
     global.next = null;
   }
 
-  void reassignBaseToGlobalBad() {
+  void FN_reassignBaseToGlobalBad() {
     DeepOwnership x = new DeepOwnership();
     x = global;
     x.next = null;

infer/tests/codetoanalyze/java/racerd/Ownership.java

@@ -157,7 +157,7 @@ public class Ownership {
     writeToFormal(o);
   }
 
-  public void writeToNotOwnedInCalleeBad2() {
+  public void FN_writeToNotOwnedInCalleeBad2() {
     Obj o = getMaybeUnownedObj();
     writeToFormal(o);
   }
@@ -339,7 +339,7 @@ public class Ownership {
     castThenCall(o);
   }
 
-  void castThenCallBad() {
+  void FN_castThenCallBad() {
     Obj o = getMaybeUnownedObj();
     castThenCall(o);
   }
@@ -507,7 +507,7 @@ public class Ownership {
     conditionalAlias(new Obj(), new Obj());
   }
 
-  void conditionalAliasBad(Obj unowned) {
+  void FN_conditionalAliasBad(Obj unowned) {
     conditionalAlias(new Obj(), unowned);
   }
 }

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

@@ -47,7 +47,6 @@ codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Container
 codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.poolBad():void, 298, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [Write to container `this.simplePool` via call to `release`]
 codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.readSimpleArrayMap():int, 284, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,Read of container `this.si_map` via call to `get`,<Write trace>,Write to container `this.si_map` via call to `put`]
 codetoanalyze/java/racerd/DeepOwnership.java, DeepOwnership.globalNotOwnedBad():void, 16, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `DeepOwnership.global.next`]
-codetoanalyze/java/racerd/DeepOwnership.java, DeepOwnership.reassignBaseToGlobalBad():void, 22, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `x.next`]
 codetoanalyze/java/racerd/Dispatch.java, codetoanalyze.java.checkers.Dispatch.callUnannotatedInterfaceBad(codetoanalyze.java.checkers.UnannotatedInterface):void, 49, INTERFACE_NOT_THREAD_SAFE, no_bucket, WARNING, [Call to un-annotated interface method void UnannotatedInterface.foo()]
 codetoanalyze/java/racerd/Dispatch.java, codetoanalyze.java.checkers.Dispatch.callUnannotatedInterfaceIndirectBad(codetoanalyze.java.checkers.NotThreadSafe,codetoanalyze.java.checkers.UnannotatedInterface):void, 53, INTERFACE_NOT_THREAD_SAFE, no_bucket, WARNING, [call to void NotThreadSafe.notThreadSafeOk(UnannotatedInterface),Call to un-annotated interface method void UnannotatedInterface.foo()]
 codetoanalyze/java/racerd/Dispatch.java, codetoanalyze.java.checkers.ThreadConfinedField.interfaceCallOnNormalFieldBad():void, 102, INTERFACE_NOT_THREAD_SAFE, no_bucket, WARNING, [Call to un-annotated interface method void UnannotatedInterface.foo()]
@@ -73,18 +72,14 @@ codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.unownedR
 codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.useLockInCalleeBad():void, 221, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.<init>(codetoanalyze.java.checkers.Obj,java.lang.Object), 66, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `obj.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.cantOwnThisBad():void, 171, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.setField(Obj),access to `this.field`]
-codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.castThenCallBad():void, 344, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to `s.f`]
-codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.conditionalAliasBad(codetoanalyze.java.checkers.Obj):void, 511, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.conditionalAlias(Obj,Obj),access to `alias.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notOwnedInCalleeBad(codetoanalyze.java.checkers.Obj):void, 233, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.mutateIfNotNull(Obj),access to `o.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(codetoanalyze.java.checkers.Obj):void, 421, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 428, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.field`,<Write trace>,call to void Ownership.setField(Obj),access to `this.field`]
-codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad():void, 430, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `m.g`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.ownInOneBranchBad(codetoanalyze.java.checkers.Obj,boolean):void, 82, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.readGlobalBad():int, 403, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `checkers.Ownership.global`,<Write trace>,access to `checkers.Ownership.global`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 87, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `formal.g`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 88, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `formal.g`,<Write trace>,access to `formal.g`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad1(codetoanalyze.java.checkers.Obj):void, 157, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`]
-codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad2():void, 162, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.writeToFormal(Obj),access to `o.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad3(codetoanalyze.java.checkers.Obj):void, 166, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `o.f`]
 codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToOwnedInCalleeOk2():void, 183, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`]
 codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional2_bad(boolean):void, 130, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.ff`]