Module Absint.ConcurrencyModels

type lock_effect =
  1. | Lock of HilExp.t list
    (*

    simultaneously acquire a list of locks

    *)
  2. | Unlock of HilExp.t list
    (*

    simultaneously release a list of locks

    *)
  3. | LockedIfTrue of HilExp.t list
    (*

    simultaneously attempt to acquire a list of locks

    *)
  4. | GuardConstruct of {
    1. guard : HilExp.t;
    2. lock : HilExp.t;
    3. acquire_now : bool;
    }
    (*

    mutex guard construction - clang only

    *)
  5. | GuardLock of HilExp.t
    (*

    lock underlying mutex via guard - clang only

    *)
  6. | GuardLockedIfTrue of HilExp.t
    (*

    lock underlying mutex if true via guard - clang only

    *)
  7. | GuardUnlock of HilExp.t
    (*

    unlock underlying mutex via guard - clang only

    *)
  8. | GuardDestroy of HilExp.t
    (*

    destroy guard and unlock underlying mutex - clang only

    *)
  9. | NoEffect
    (*

    function call has no lock-relevant effect

    *)

effect of call plus Hil expressions being un/locked, if known

type thread =
  1. | BackgroundThread
  2. | MainThread
  3. | MainThreadIfTrue
  4. | UnknownThread
val get_lock_effect : IR.Procname.t -> HilExp.t list -> lock_effect

describe how this procedure behaves with respect to locking

val get_thread_assert_effect : IR.Procname.t -> thread

In Java, certain methods can be used to assert execution on a specific kind of thread, or return a boolean equivalent to such a fact.

val get_current_class_and_annotated_superclasses : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> (IR.Typ.name * IR.Typ.name list) option
val is_recursive_lock_type : IR.Typ.name -> bool
type annotation_trail =
  1. | DirectlyAnnotated
    (*

    the method is directly annotated as such

    *)
  2. | Override of IR.Procname.t
    (*

    it overrides a method annotated in a super class

    *)
  3. | SuperClass of IR.Typ.name
    (*

    the method's class or a super class of that is annotated as such

    *)

Type documenting why a method is considered as annotated with a certain annotation

val compare_annotation_trail : annotation_trail -> annotation_trail -> int
val find_override_or_superclass_annotated : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> annotation_trail option

check if a method's transitive annotations satisfy the given predicate

val annotated_as_worker_thread : IR.Tenv.t -> IR.Procname.t -> bool
val annotated_as_named_thread : IR.Procname.t -> string option
val runs_on_ui_thread : IR.Tenv.t -> IR.Procname.t -> bool

is method not transitively annotated @WorkerThread and is modeled or annotated @UIThread or equivalent?

val is_android_lifecycle_method : IR.Tenv.t -> IR.Procname.t -> bool

is method a known Android UI thread callback (eg Activity.onCreate)