pub struct Options {
pub logical_depth: u32,
pub recompute_depth: u32,
pub refinements: usize,
pub budget: u64,
}Expand description
The limits, all three of which exist because the thing they bound is otherwise unbounded.
Fields§
§logical_depth: u32How deep into a condition the edge calculation looks, and how far back along the chain from a condition to a value the inversion walks.
GCC’s ranger-logical-depth, whose default at gcc/params.opt:998 is also six.
recompute_depth: u32How many dominating edges one query walks before it stops narrowing.
GCC’s ranger-recompute-depth at gcc/params.opt:1003 bounds a related walk with the
same default of five. The two are not the same walk, so the number is borrowed and the
meaning is not.
refinements: usizeHow many block-specific answers the cache keeps for one value.
Section 10.6’s one threshold. A query past it gets the range at the definition.
budget: u64How many definitions one set of queries works out before it stops narrowing.
The other three bound one walk each and none of them bounds what a function’s worth of questions adds up to. What makes that a real number rather than a theoretical one is the cycle rule: a range worked out while a cycle was open was worked out under an assumption, so it is not cached, so the next question about it does the whole cycle again. Eight blocks that dispatch to each other through a computed goto are eight values in one cycle and every question about any of them walks all eight, which multiplies rather than adds.
Past this every answer is the whole of the type. That is what a range knowing nothing is,
so what a program over the limit loses is code quality and not correctness, and
Counts::exhausted is how it is found out about rather than guessed at.