Struct move_model::model::StructEnv

pub struct StructEnv<'env> {
    pub module_env: ModuleEnv<'env>,
    /* private fields */
}

Fields

module_env: ModuleEnv<'env>

Reference to enclosing module.

Implementations

impl<'env> StructEnv<'env>

pub fn get_name(&self) -> Symbol

Returns the name of this struct.

pub fn get_full_name_str(&self) -> String

Gets full name as string.

pub fn get_full_name_with_address(&self) -> String

Gets full name with module address as string.

pub fn get_identifier(&self) -> Option<Identifier>

Returns the VM identifier for this struct

pub fn symbol_pool(&self) -> &SymbolPool

Shortcut for accessing the symbol pool.

pub fn get_loc(&self) -> Loc

Returns the location of this struct.

pub fn get_attributes(&self) -> &[Attribute]

Returns the attributes of this struct.

pub fn get_doc(&self) -> &str

Get documentation associated with this struct.

pub fn get_properties(&self) -> &PropertyBag

Returns properties from pragmas.

pub fn get_id(&self) -> StructId

Gets the id associated with this struct.

pub fn get_qualified_id(&self) -> QualifiedId<StructId>

Gets the qualified id of this struct.

pub fn is_native(&self) -> bool

Determines whether this struct is native.

pub fn is_intrinsic(&self) -> bool

Returns true if this struct has the pragma intrinsic set to true.

pub fn is_well_known(&self, name: &str) -> bool

Returns true if this is the well-known native or intrinsic struct of the given name.

pub fn is_vector(&self) -> bool

Determines whether this struct is the well-known vector type.

pub fn is_ghost_memory(&self) -> bool

Returns true if this struct is ghost memory for a specification variable.

pub fn get_ghost_memory_spec_var(&self) -> Option<QualifiedId<SpecVarId>>

Get the specification variable associated with this struct if this is ghost memory.

pub fn get_abilities(&self) -> AbilitySet

Get the abilities of this struct.

pub fn has_memory(&self) -> bool

Determines whether memory-related operations needs to be declared for this struct.

pub fn get_fields(&'env self) -> impl Iterator<Item = FieldEnv<'env>>

Get an iterator for the fields, ordered by offset.

pub fn get_field_count(&self) -> usize

Return the number of fields in the struct.

pub fn get_field(&'env self, id: FieldId) -> FieldEnv<'env>

Gets a field by its id.

pub fn find_field(&'env self, name: Symbol) -> Option<FieldEnv<'env>>

Find a field by its name.

pub fn get_field_by_offset(&'env self, offset: usize) -> FieldEnv<'env>

Gets a field by its offset.

pub fn is_phantom_parameter(&self, idx: usize) -> bool

Whether the type parameter at position idx is declared as phantom.

pub fn get_type_parameters(&self) -> Vec<TypeParameter>

Returns the type parameters associated with this struct.

pub fn get_named_type_parameters(&self) -> Vec<TypeParameter>

Returns the type parameters associated with this struct, with actual names.

pub fn has_conditions(&self) -> bool

Returns true if this struct has specification conditions.

pub fn get_spec(&'env self) -> &'env Spec

Returns the data invariants associated with this struct.

pub fn is_pragma_true(&self, name: &str, default: impl FnOnce() -> bool) -> bool

Returns the value of a boolean pragma for this struct. This first looks up a pragma in this struct, then the enclosing module, and finally uses the provided default. value

pub fn is_native_or_intrinsic(&self) -> bool

Returns true if this struct is native or marked as intrinsic.

Trait Implementations

impl<'env> Clone for StructEnv<'env>

fn clone(&self) -> StructEnv<'env>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'env> Debug for StructEnv<'env>

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

Formats the value using the given formatter.