Monitor and demonitor call sites.
A monitor is a promise the runtime keeps: once Process.monitor/1
returns, a {:DOWN, ref, :process, object, reason} message will arrive
unless the monitor is cancelled. Nothing in the calling code says so, and
the message can arrive arbitrarily later — after a receive gave up
waiting, after the state machine moved on, after the reason stopped
meaning anything.
Two consequences, and both are structural.
Process.demonitor(ref) cancels, but a {:DOWN, ...} already in the
mailbox stays there; only Process.demonitor(ref, [:flush]) removes it.
So the flush option is recorded separately — it is the difference between
cancelling a future message and cancelling a message that has already been
sent.
And a process that monitors is a process that receives :DOWN. That makes
"will this specific message arrive?" answerable for once, where in general
it is not: the analysis need not guess what lands in a mailbox if the code
asked for it.
Emitted facts
monitor_call(id, func, target)— a monitor is establishedmonitor_ref_dropped(id, func)— the reference that monitor returned is discarded at the call site, so nothing can ever demonitor itdemonitor_call(id, func, flush)—flushis"flush"or"no_flush"matches_down(func)— the function's clause heads (or acaseon an argument, before any call) compare to:DOWN, so it is (part of) a :DOWN handler; unlikecallback_tagthis is emitted for every function, because a gen_statem funnels its :info events into private helpers that no callback name identifies
Whether the ref is dropped is read from the instructions after the
call, along every path: the ref arrives in {x, 0}, and it is dropped
when on each path the next thing to happen to that register is a write
that does not read it — a move of something else into it, a zero-arity
call, a tuple built into it from other registers, a test_heap
declaring no live registers. A read on any path, a return, and anything
the scan does not understand count as kept, which is the direction
that keeps the fact honest.