Struct KaniHarness 

pub struct KaniHarness {
    pub id: String,
    pub obligation: String,
    pub property: Option<String>,
    pub bound: Option<u32>,
    pub strategy: Option<KaniStrategy>,
    pub solver: Option<String>,
    pub harness: Option<String>,
    pub actually_verified: Option<bool>,
}

A Kani bounded model checking harness definition.

Corresponds to Phase 6 (Verify) of the pipeline.

Fields

id: String

obligation: String

property: Option<String>

bound: Option<u32>

strategy: Option<KaniStrategy>

solver: Option<String>

harness: Option<String>

actually_verified: Option<bool>

GH-1595: When true, the harness has been verified by a green cargo kani run in CI (e.g. apr-cookbook kani-gate). Lifts the D3 strategy weight to 1.0 for non-exhaustive strategies because the runtime witness supplants the static-readiness signal.

Trait Implementations

impl Clone for KaniHarness

fn clone(&self) -> KaniHarness

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for KaniHarness

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

Formats the value using the given formatter.

impl Default for KaniHarness

fn default() -> KaniHarness

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for KaniHarness

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for KaniHarness

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

where __S: Serializer,

Serialize this value into the given Serde serializer.