From 002e47013757ba6fbec096241c46575a337aa215 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 21 Dec 2018 00:52:49 -0800 Subject: [PATCH] [racerd] fix bug in ownership transitivity Reviewed By: jvillard Differential Revision: D13488078 fbshipit-source-id: 9d40d75bc --- infer/src/concurrency/RacerD.ml | 4 +--- infer/tests/codetoanalyze/java/racerd/issues.exp | 1 - 2 files changed, 1 insertion(+), 4 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index dcbc79056..ace467eef 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -91,9 +91,7 @@ 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 - (* 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 + match OwnershipDomain.get_owned prefix_path ownership with | OwnershipAbstractValue.OwnedIf formal_indexes -> let pre = AccessSnapshot.make access locks threads diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 553c43bd6..bb0487851 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -80,7 +80,6 @@ codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership. codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.readGlobalBad():int, 402, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,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, 86, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `formal.g`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 87, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `formal.g`,,access to `formal.g`] -codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.reassignToFormalBad(codetoanalyze.java.checkers.Obj):void, 87, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `formal.g.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad1(codetoanalyze.java.checkers.Obj):void, 156, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.writeToFormal(Obj),access to `formal.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad2():void, 161, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.writeToFormal(Obj),access to `formal.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.writeToNotOwnedInCalleeBad3(codetoanalyze.java.checkers.Obj):void, 165, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `formal.f`]