Laundering gives an integer converted back to a pointer the capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees. of the pointer it came from, as Fil-C does when its analysis can follow the integer: through arithmetic, promotable local variables and phis, never through memory or a call, and only from one pointer (launder:launder_func/4launder.pllaunder_func+F₀, +Records₀, -F, -RecordsdetF is the function F0 with each itop of an integer computed from one capability given that capability (this module's header), and Records is its context Records0 with instruction sites moved accordingly., m4.md, Pointer-as-int laundering). Otherwise the pointer gets no capability and dereferencing it traps.

Upstream it is FilPizlonator's pointer-as-int laundering: an abstract interpreter over the integer SSA values, in which each ptrtoint starts as its pointer, loads and calls as nothing, and a value reached from two pointers as conflicting.

Laundering rewrites the IR before checking; the model sees only its result. An unlaundered itop yields a pointer with CNone (Itop). launder.pl's capability shadowshadow nanofilA shadow is a slot that holds a copy on the side, in two unrelated places. In the backends, a phi's shadow slot holds the incoming value during a parallel copy (it may be a home). In launder.pl, a local integer's capability shadow is a pointer slot that holds the capability of the value last stored in the integer (launder:launder_func/4, launder). is a different use of the word.