diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 67c3ebd46..fbf8eba37 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -145,7 +145,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> false in - (* TODO: simplify this with AccessPath.truncate *) let rec add_field_accesses prefix_path access_acc = function | [] -> access_acc @@ -160,7 +159,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else let is_write = if List.is_empty access_list then is_write_access else false in let access = TraceElem.make_field_access prefix_path' ~is_write loc in - match OwnershipDomain.get_owned prefix_path ownership with + (* use ownership value of base: if base is owned, treat suffixes as owned too *) + let base_path = (fst prefix_path, []) in + match OwnershipDomain.get_owned base_path ownership with | OwnershipAbstractValue.OwnedIf formal_indexes -> let pre = AccessSnapshot.make access locks threads diff --git a/infer/tests/codetoanalyze/java/racerd/Builders.java b/infer/tests/codetoanalyze/java/racerd/Builders.java index 5a954d770..94d4023bb 100644 --- a/infer/tests/codetoanalyze/java/racerd/Builders.java +++ b/infer/tests/codetoanalyze/java/racerd/Builders.java @@ -104,3 +104,22 @@ class TopLevelBuilder { } } + +class MyBuilder { + Obj mObj; + + public static MyBuilder create() { + return new MyBuilder(); + } + + public MyBuilder setNestedPath(int i) { + this.mObj.f = i; + return this; + } + + @ThreadSafe + static void setNestedPathOk(int i) { + MyBuilder.create().setNestedPath(1); + } + +} diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index fae96dbdc..9effe24f6 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -81,6 +81,7 @@ codetoanalyze/java/racerd/Ownership.java, void Ownership.notPropagatingOwnership codetoanalyze/java/racerd/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 5, THREAD_SAFETY_VIOLATION, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignParamToUnownedBad(), 1, THREAD_SAFETY_VIOLATION, ERROR, [call to void Ownership.reassignParamToUnowned(Obj),access to `o.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 2, THREAD_SAFETY_VIOLATION, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.g`] +codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.g.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 3, THREAD_SAFETY_VIOLATION, ERROR, [,access to `formal.codetoanalyze.java.checkers.Obj.g`,,access to `formal.codetoanalyze.java.checkers.Obj.g`] codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad1(Obj), 1, THREAD_SAFETY_VIOLATION, ERROR, [call to void Ownership.writeToFormal(Obj),access to `formal.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, ERROR, [call to void Ownership.writeToFormal(Obj),access to `formal.codetoanalyze.java.checkers.Obj.f`]