Module Concurrency__StarvationDomain.ThreadDomain
Domain for thread-type. The main goals are
- Track code paths that are explicitly on UI/BG thread (via annotations, or assertions).
- Maintain UI/BG-thread-ness through the call stack (if a caller is of unknown status and callee is on UI/BG thread then caller must be on the UI/BG thread too).
- Traces with "UI-thread" status cannot interleave but all other combinations can.
- Top is AnyThread, which means that there are executions on both UI and BG threads on this method.
- Bottom is UnknownThread, and used as initial state.
include Absint.AbstractDomain.WithBottom with type t := t
include Absint.AbstractDomain.S
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val bottom : t
The bottom value of the domain.
val is_bottom : t -> bool
Return true if this is the bottom value