Struct AbstractInterpretation 

pub struct AbstractInterpretation {
    pub domain: HashMap<String, IntervalDomain>,
}

Abstract interpretation engine using the interval domain.

Fields

domain: HashMap<String, IntervalDomain>

Abstract domain for each tracked variable.

Implementations

impl AbstractInterpretation

pub fn new() -> Self

Create a new abstract interpreter with no variable bindings.

pub fn bind(&mut self, var: impl Into<String>, value: f64)

Bind a variable to a concrete value (singleton interval).

pub fn bind_interval( &mut self, var: impl Into<String>, interval: IntervalDomain, )

Bind a variable to an abstract interval.

pub fn get(&self, var: &str) -> IntervalDomain

Return the abstract value of a variable, or top() if unknown.

pub fn analyze_loop( &mut self, var: &str, delta: IntervalDomain, max_iter: usize, ) -> IntervalDomain

Analyze a simple loop that adds delta to var each iteration for at most max_iter iterations, using widening to ensure termination.

Returns the post-loop interval for var.

pub fn widening( &self, prev: &IntervalDomain, next: &IntervalDomain, ) -> IntervalDomain

Widening operator: extends the interval to ensure convergence.

If the lower bound decreases it goes to -∞; if the upper bound increases it goes to +∞.

pub fn narrowing( &self, prev: &IntervalDomain, next: &IntervalDomain, ) -> IntervalDomain

Narrowing operator: refines an over-approximation using additional concrete information.

pub fn is_non_negative(&self, var: &str) -> bool

Check that var is always non-negative under the current abstraction.

pub fn is_bounded(&self, var: &str) -> bool

Check that var is bounded (finite interval bounds).

Trait Implementations

impl Clone for AbstractInterpretation

fn clone(&self) -> AbstractInterpretation

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AbstractInterpretation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for AbstractInterpretation

fn default() -> Self

Returns the “default value” for a type.