Module range_check 

Interval bound check for VSA results.

Build a range-check Program:

use weir::range_check::range_check;

let program = range_check(4, "interval_hi", "bound", "out");

range_check - interval-VSA bound check. Composes the per-node interval table with a comparison against a known bound.

Per node n, write 1 to out[n] iff interval(n).hi < bound[n]. Dataflow consumers use this for CWE-787 / CWE-190 to assert “size is bounded by destination buffer length.”

Structs

RangeCheck

Soundness marker for range_check.

Functions

range_check

Build a range-check Program. Inputs: