Struct LoopBound 

pub struct LoopBound {
    pub bound: Option<u64>,
}

Estimated loop bound: an upper bound on iteration count.

Fields

bound: Option<u64>

Estimated maximum iterations

Implementations

impl LoopBound

pub fn unknown() -> Self

Unknown bound.

pub fn finite(n: u64) -> Self

Known finite bound.

pub fn from_interval(interval: &IntervalDomain) -> Self

Estimate loop bound from interval [0, n]: bound is n+1 iterations.

pub fn terminates(&self) -> bool

Check if the loop is known to terminate.