pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[racerd] modulo loc

Browse Source 
Reviewed By: jvillard

Differential Revision: D14616104

fbshipit-source-id: 314a14069
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent 4700f7684c
commit fdcd4cf591
3 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File

6
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -120,8 +120,10 @@ module Access = struct
end end
module TraceElem = struct module TraceElem = struct
(* FIXME evaluate modulo location functor *) (** This choice means the comparator is insensitive to the location access.
include ExplicitTrace.MakeTraceElem (Access) This preserves correctness only if the overlying comparator (AccessSnapshot)
takes into account the characteristics of the access (eg lock status). *)
include ExplicitTrace.MakeTraceElemModuloLocation (Access)
let is_write {elem} = Access.is_write elem let is_write {elem} = Access.is_write elem

4
infer/tests/build_systems/racerd_dedup/issues.exp
Unescape View File

@ -2,7 +2,7 @@ DeDup.java, build_systems.threadsafety.DeDup.colocated_read_write():void, 63, TH
DeDup.java, build_systems.threadsafety.DeDup.separate_write_to_colocated_read():void, 68, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.colocated_read`] DeDup.java, build_systems.threadsafety.DeDup.separate_write_to_colocated_read():void, 68, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.colocated_read`]
DeDup.java, build_systems.threadsafety.DeDup.twoWritesOneInCaller():void, 50, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.writeToField(),access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.twoWritesOneInCaller():void, 50, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.writeToField(),access to `this.field`]
DeDup.java, build_systems.threadsafety.DeDup.two_fields():void, 20, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.foo(),access to `this.fielda`] DeDup.java, build_systems.threadsafety.DeDup.two_fields():void, 20, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.foo(),access to `this.fielda`]
DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 38, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 37, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`]
DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 31, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 30, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`]
DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`]
DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 45, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 45, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`]

5
infer/tests/codetoanalyze/java/racerd/issues.exp
Unescape View File

@ -25,7 +25,6 @@ codetoanalyze/java/racerd/Constructors.java, Constructors.FP_singleton2Ok():Cons
codetoanalyze/java/racerd/Constructors.java, Constructors.singleton1Bad():Constructors, 57, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to Constructors.<init>(Object),access to `Constructors.staticField`] codetoanalyze/java/racerd/Constructors.java, Constructors.singleton1Bad():Constructors, 57, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to Constructors.<init>(Object),access to `Constructors.staticField`]
codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 63, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `Constructors.sSingleton2`,<Write trace>,access to `Constructors.sSingleton2`] codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 63, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `Constructors.sSingleton2`,<Write trace>,access to `Constructors.sSingleton2`]
codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 64, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `Constructors.sSingleton2`] codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 64, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `Constructors.sSingleton2`]
codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 66, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `Constructors.sSingleton2`,<Write trace>,access to `Constructors.sSingleton2`]
codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSimpleArrayMapBad(android.support.v4.util.SimpleArrayMap):void, 279, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `map` via call to `put`] codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSimpleArrayMapBad(android.support.v4.util.SimpleArrayMap):void, 279, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `map` via call to `put`]
codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSparseArrayBad(android.util.SparseArray):void, 269, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `sparseArray` via call to `put`] codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSparseArrayBad(android.util.SparseArray):void, 269, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `sparseArray` via call to `put`]
codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSparseArrayCompatBad(android.support.v4.util.SparseArrayCompat):void, 260, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `sparseArray` via call to `put`] codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSparseArrayCompatBad(android.support.v4.util.SparseArrayCompat):void, 260, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `sparseArray` via call to `put`]
@ -93,9 +92,9 @@ codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.R
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isMainThread_Negation_Bad():void, 168, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isMainThread_Negation_Bad():void, 168, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.ff`]
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad():void, 162, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad():void, 162, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.ff`]
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.confusedAssertBad(boolean):void, 191, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.mFld`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.confusedAssertBad(boolean):void, 191, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.mFld`]
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.readProtectedUnthreadedBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.readProtectedUnthreadedBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.f`,<Write trace>,call to void RaceWithMainThread.main_thread_OK(),access to `this.f`]
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded1_Bad():void, 64, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.f1`,<Write trace>,access to `this.f1`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded1_Bad():void, 64, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.f1`,<Write trace>,access to `this.f1`]
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded_Bad():void, 59, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.f`,<Write trace>,access to `this.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded_Bad():void, 59, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.f`,<Write trace>,call to void RaceWithMainThread.main_thread_OK(),access to `this.f`]
codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.writeAfterConditionalMainThreadInCalleeBad():void, 228, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.mSharedField`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.writeAfterConditionalMainThreadInCalleeBad():void, 228, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.mSharedField`]
codetoanalyze/java/racerd/ReadWriteRaces.java, codetoanalyze.java.checkers.ReadWriteRaces.callUnprotecteReadInCallee():java.lang.Object, 74, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `this.field1`,<Write trace>,access to `this.field1`] codetoanalyze/java/racerd/ReadWriteRaces.java, codetoanalyze.java.checkers.ReadWriteRaces.callUnprotecteReadInCallee():java.lang.Object, 74, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `this.field1`,<Write trace>,access to `this.field1`]
codetoanalyze/java/racerd/ReadWriteRaces.java, codetoanalyze.java.checkers.ReadWriteRaces.m1():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.racy`,<Write trace>,access to `this.racy`] codetoanalyze/java/racerd/ReadWriteRaces.java, codetoanalyze.java.checkers.ReadWriteRaces.m1():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.racy`,<Write trace>,access to `this.racy`]

Write Preview
Loading…
Cancel
Save