Struct KaniListJson

pub struct KaniListJson {
    pub kani_version: BoxStr,
    pub file_version: BoxStr,
    pub standard_harnesses: KaniListHarnesses,
    pub contract_harnesses: KaniListHarnesses,
    pub contracts: IndexSet<ContractedFunction>,
    pub totals: Totals,
}

The datastructure generated from kani list --json.

ref: https://github.com/model-checking/kani/blob/b64e59de669cd77b625cc8c0b9a94f29117a0ff7/kani-driver/src/list/output.rs#L113

Fields

kani_version: BoxStr

file_version: BoxStr

standard_harnesses: KaniListHarnesses

contract_harnesses: KaniListHarnesses

contracts: IndexSet<ContractedFunction>

totals: Totals

Implementations

impl KaniListJson

pub fn normalize_file_path(&mut self)

Call this immediately after deserialization is done, especially before strip_path_prefix.

pub fn strip_path_prefix<P: AsRef<Path>>(&mut self, path: P)

pub fn strip_path_prefix_raw(&mut self, prefix: &str)

This function is used in tests.

pub fn strip_path_closure_name(&mut self, text: &[&str])

pub fn files(&self) -> Value

pub fn harness_names( &self, filter: impl FnMut(&str, &str) -> bool, ) -> IndexSet<&str>

Trait Implementations

impl Clone for KaniListJson

fn clone(&self) -> KaniListJson

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for KaniListJson

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for KaniListJson

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for KaniListJson

fn eq(&self, other: &KaniListJson) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for KaniListJson

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for KaniListJson

impl StructuralPartialEq for KaniListJson