diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 2066fb1ba..f4d455a8d 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/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) diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 8209f0be0..53eb0a2a5 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/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} diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 77651b724..5790aeac0 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/cpp/racerd/issues.exp b/infer/tests/codetoanalyze/cpp/racerd/issues.exp index b8dc983e4..8473ffa2c 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/issues.exp +++ b/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, [,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->w`,,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, [,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `this->x.x1->u`,,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, [,call to dereferencing::Basic::call1,call to dereferencing::Basic::mixed_deref_race,access to `*(this->x.x2)->a.b.c`,,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, [,access to `x->f`,,access to `x->f`] -codetoanalyze/cpp/racerd/locals_ownership.cpp, locals::Ownership::test3_bad, 65, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [,access to `x->f`,,access to `x->f`] codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::get2, 34, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [,access to `this->suspiciously_written`,,access to `this->suspiciously_written`] codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::get4, 40, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [,access to `this->suspiciously_read`,,access to `this->suspiciously_read`] codetoanalyze/cpp/racerd/lock_guard.cpp, basics::LockGuard::test1, 44, LOCK_CONSISTENCY_VIOLATION, no_bucket, WARNING, [,access to `this->suspiciously_read`,,access to `this->suspiciously_read`] diff --git a/infer/tests/codetoanalyze/cpp/racerd/locals_ownership.cpp b/infer/tests/codetoanalyze/cpp/racerd/locals_ownership.cpp index 20ebeec24..6af4f2fc1 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/locals_ownership.cpp +++ b/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 = ¤t; 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; diff --git a/infer/tests/codetoanalyze/java/racerd/DeepOwnership.java b/infer/tests/codetoanalyze/java/racerd/DeepOwnership.java index 38b2d12ca..309b1a3eb 100644 --- a/infer/tests/codetoanalyze/java/racerd/DeepOwnership.java +++ b/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; diff --git a/infer/tests/codetoanalyze/java/racerd/Ownership.java b/infer/tests/codetoanalyze/java/racerd/Ownership.java index fb2f8cd25..b74dfd378 100644 --- a/infer/tests/codetoanalyze/java/racerd/Ownership.java +++ b/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); } } diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 729213174..c1ba2ffc4 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/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 of container `this.si_map` via call to `get`,,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.(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, [,access to `this.field`,,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, [,access to `checkers.Ownership.global`,,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, [,access to `formal.g`,,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, [,access to `this.field`,,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`]