Expand description
Checkers for InBound and NonOverlap.
Bounds are discharged from has_checked_bounds facts, layout field-offset
invariants, or an SMT coverage check over allocation base/size.
NonOverlap uses provenance-distinctness and range-overlap reasoning.