Struct ArrayBoundsAnalysis 

pub struct ArrayBoundsAnalysis {
    pub index_bounds: HashMap<String, IntervalDomain>,
    pub array_sizes: HashMap<String, IntervalDomain>,
}

Array bounds analysis: interval analysis for array indices.

Fields

index_bounds: HashMap<String, IntervalDomain>

Variable → index interval

array_sizes: HashMap<String, IntervalDomain>

Array name → size (as interval)

Implementations

impl ArrayBoundsAnalysis

pub fn new() -> Self

Create a new empty array bounds analysis.

pub fn is_safe_access(&self, array: &str, idx_var: &str) -> bool

Check if access array[idx_var] is provably safe.

Trait Implementations

impl Default for ArrayBoundsAnalysis

fn default() -> Self

Returns the “default value” for a type.