Verifies @pure true contracts (see Argus.Purity).
Every other argus analysis looks for a bug nobody claimed was absent. This one checks a claim the author made, which changes what a finding means: not "this looks suspicious" but "you said this function has no side effects, and here is the call that gives it one".
It is also the only analysis here that has to be sound rather than merely useful. A missed supervision smell costs a warning; a purity check that reports "verified" for a function that writes to ETS has actively misled someone into depending on it. So there are three outcomes, not two:
purity_violated— reaches a call with a known observable effect.purity_unprovable— reaches a call that cannot be followed (a fun value,apply) or that the effect model has no entry for.purity_verified— everything reachable is known to be effect-free.
The third is emitted on purpose. A contract is only worth having if you can tell it was actually checked, and an analysis that reports only failures cannot distinguish "verified" from "never looked at".