Struct VShapeDef 

pub struct VShapeDef {
    pub layout: VLayout,
    pub def: VDef,
}

A bounded shape definition for Kani verification.

Unlike facet_core::Shape which uses static references and can be recursive, these shapes are bounded and can implement kani::Arbitrary.

Shape definitions live in a DynShapeStore and are referenced by handle.

Fields

layout: VLayout

Layout of this type.

def: VDef

Type-specific information.

Implementations

impl VShapeDef

pub const fn scalar(layout: VLayout) -> Self

Create a scalar shape with the given layout.

pub fn struct_with_fields( store: &VShapeStore, fields: &[(usize, VShapeHandle)], ) -> Self

Create a struct shape with the given fields.

The field_shapes parameter provides the shape handle for each field. Use store.get_def(handle).layout to get layouts for size calculation.

Trait Implementations

impl Clone for VShapeDef

fn clone(&self) -> VShapeDef

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for VShapeDef

impl Debug for VShapeDef

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

Formats the value using the given formatter.

impl Eq for VShapeDef

impl PartialEq for VShapeDef

fn eq(&self, other: &VShapeDef) -> 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 StructuralPartialEq for VShapeDef