Module StarvationDomain.Attribute

Tracks expression attributes

type t =
| Nothing
| ThreadGuard

is boolean equivalent to whether on UI thread

| FutureDoneGuard of Absint.HilExp.AccessExpression.t

boolean equivalent to Future.isDone()

| FutureDoneState of bool

is a Future ready for non-blocking consumption

| Runnable of IR.Procname.t

is a Runnable/Callable with given "run" procname

| WorkScheduler of StarvationModels.scheduler_thread_constraint

exp is something that schedules work on the given thread

| Looper of StarvationModels.scheduler_thread_constraint

Android looper on given thread

include Absint.AbstractDomain.WithTop with type t := t
include Absint.AbstractDomain.S
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val top : t
val is_top : t -> bool