Struct ContractCoverage 

pub struct ContractCoverage {
    pub stem: String,
    pub equations: usize,
    pub obligations: usize,
    pub falsification_covered: usize,
    pub kani_covered: usize,
    pub binding_implemented: usize,
    pub binding_partial: usize,
    pub binding_missing: usize,
    pub by_type: BTreeMap<String, usize>,
}

Coverage details for a single contract.

Fields

stem: String

Contract stem (filename without .yaml).

equations: usize

Total equations.

obligations: usize

Total proof obligations.

falsification_covered: usize

Obligations covered by at least one falsification test.

kani_covered: usize

Obligations covered by at least one Kani harness.

binding_implemented: usize

Number of equations with an implemented binding.

binding_partial: usize

Number of equations with partial binding.

binding_missing: usize

Number of equations with no binding.

by_type: BTreeMap<String, usize>

Per-obligation-type breakdown.

Trait Implementations

impl Clone for ContractCoverage

fn clone(&self) -> ContractCoverage

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ContractCoverage

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

Formats the value using the given formatter.