[racerd] fix bug in ownership transitivity

Reviewed By: jvillard

Differential Revision: D13488078

fbshipit-source-id: 9d40d75bc
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent d2600795db
commit 002e470137

@ -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

@ -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, [<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, 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, [<Read trace>,access to `formal.g`,<Write trace>,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`]

Loading…
Cancel
Save