Struct move_model::model::ModuleData
source · pub struct ModuleData {Show 14 fields
pub name: ModuleName,
pub id: ModuleId,
pub module: CompiledModule,
pub named_constants: BTreeMap<NamedConstantId, NamedConstantData>,
pub struct_data: BTreeMap<StructId, StructData>,
pub struct_idx_to_id: BTreeMap<StructDefinitionIndex, StructId>,
pub function_data: BTreeMap<FunId, FunctionData>,
pub function_idx_to_id: BTreeMap<FunctionDefinitionIndex, FunId>,
pub spec_vars: BTreeMap<SpecVarId, SpecVarDecl>,
pub spec_funs: BTreeMap<SpecFunId, SpecFunDecl>,
pub module_spec: Spec,
pub source_map: SourceMap,
pub loc: Loc,
pub spec_block_infos: Vec<SpecBlockInfo>,
/* private fields */
}
Expand description
Module Environment
Represents data for a module.
Fields§
§name: ModuleName
Module name.
id: ModuleId
Id of this module in the global env.
module: CompiledModule
Module byte code.
named_constants: BTreeMap<NamedConstantId, NamedConstantData>
Named constant data
struct_data: BTreeMap<StructId, StructData>
Struct data.
struct_idx_to_id: BTreeMap<StructDefinitionIndex, StructId>
Mapping from struct definition index to id in above map.
function_data: BTreeMap<FunId, FunctionData>
Function data.
function_idx_to_id: BTreeMap<FunctionDefinitionIndex, FunId>
Mapping from function definition index to id in above map.
spec_vars: BTreeMap<SpecVarId, SpecVarDecl>
Specification variables, in SpecVarId order.
spec_funs: BTreeMap<SpecFunId, SpecFunDecl>
Specification functions, in SpecFunId order.
module_spec: Spec
Module level specification.
source_map: SourceMap
Module source location information.
loc: Loc
The location of this module.
spec_block_infos: Vec<SpecBlockInfo>
A list of spec block infos, for documentation generation.