Skip to main content

Module must_init

Module must_init 

Source
Expand description

Must-initialization analysis.

Build a must-init query Program:

use weir::must_init::must_init;

let program = must_init(4, "def_dominates", "use_set", "out");

Must-init analysis: is variable v guaranteed initialized before use?

Composes the dominator tree with the def site set: v is must- initialized at use iff every CFG path from entry to use crosses a definition of v. Encoded as: the def set must dominate the use.

Output is a per-node bitset where bit n is set iff node n’s use of the queried variable is must-initialized.

Soundness: Exact when the supplied dominator tree is correct.

Structs§

MustInit
Soundness marker for must_init.

Functions§

must_init
Build a must-init Program. def_dominates is a host-supplied per-node bitset where bit n is set iff some def of the queried variable dominates node n. use_set is the per-node bitset of use sites. Output: bit n set iff n is in use_set AND in def_dominates.