Struct Budget 

pub struct Budget { /* private fields */ }

Tracks consumption against Limits and remembers the first breach.

Implementations

impl Budget

pub fn new(limits: Limits) -> Self

Start a budget; the clock starts now.

pub fn limits(&self) -> &Limits

The configured limits (reported in results).

pub fn limit_hit(&self) -> Option<ErrorCode>

The first limit that stopped the run, if any (--trace-limits).

pub fn add_states(&mut self, n: u64) -> Result<(), ErrorCode>

Account for n new states. Overflow counts as a breach.

pub fn add_memory(&mut self, bytes: u64) -> Result<(), ErrorCode>

Account for bytes of estimated memory.

pub fn check_time(&mut self) -> Result<(), ErrorCode>

Cooperative time check; call at loop boundaries.

pub fn check_repeat(&mut self, count: u64) -> Result<(), ErrorCode>

Check a counted-repetition bound before expanding it.

pub fn check_length(&mut self, len: u64) -> Result<(), ErrorCode>

Check pattern length.

pub fn check_depth(&mut self, depth: u32) -> Result<(), ErrorCode>

Check nesting depth.

pub fn check_enumerate(&mut self, count: u64) -> Result<(), ErrorCode>

Check an enumeration count.

Trait Implementations

impl Debug for Budget

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

Formats the value using the given formatter.