List of all items
Structs
- ast::Condition
- ast::Exp
- ast::ExpDisplay
- ast::GlobalInvariant
- ast::LocalVarDecl
- ast::ModuleName
- ast::ModuleNameDisplay
- ast::OperationDisplay
- ast::QualifiedSymbol
- ast::QualifiedSymbolDisplay
- ast::Spec
- ast::SpecBlockInfo
- ast::SpecFunDecl
- ast::SpecVarDecl
- code_writer::CodeWriter
- code_writer::CodeWriterLabel
- exp_rewriter::ExpRewriter
- model::AbilityConstraint
- model::AbilitySet
- model::EnvDisplay
- model::ExpInfo
- model::FieldData
- model::FieldEnv
- model::FieldId
- model::FunId
- model::FunctionData
- model::FunctionEnv
- model::GlobalEnv
- model::GlobalId
- model::Loc
- model::LocDisplay
- model::ModuleData
- model::ModuleEnv
- model::ModuleId
- model::NamedConstantData
- model::NamedConstantEnv
- model::NamedConstantId
- model::NodeId
- model::Parameter
- model::QualifiedId
- model::QualifiedInstId
- model::SchemaId
- model::SpecFunId
- model::SpecVarId
- model::StructData
- model::StructEnv
- model::StructId
- model::TypeParameter
- options::ModelBuilderOptions
- spec_translator::SpecTranslator
- spec_translator::TranslatedSpec
- symbol::Symbol
- symbol::SymbolDisplay
- symbol::SymbolPool
- ty::Substitution
- ty::TypeDisplay
- ty::TypeInstantiationDerivation
- ty::TypeUnificationAdapter
Enums
- ast::ConditionKind
- ast::ExpData
- ast::Operation
- ast::PropertyValue
- ast::QuantKind
- ast::SpecBlockTarget
- ast::Value
- exp_rewriter::RewriteTarget
- model::FunctionVisibility
- model::VerificationScope
- ty::PrimitiveType
- ty::Type
- ty::TypeDisplayContext
- ty::TypeUnificationError
- ty::Variance
Traits
Macros
Functions
- addr_to_big_uint
- big_uint_to_addr
- parse_addresses_from_options
- pragmas::is_pragma_valid_for_block
- pragmas::is_property_valid_for_condition
- run_bytecode_model_builder
- run_model_builder
- run_model_builder_with_options
- run_model_builder_with_options_and_compilation_flags
Type Definitions
Constants
- model::SCRIPT_BYTECODE_FUN_NAME
- model::SCRIPT_MODULE_NAME
- native::EVENT_EMIT_EVENT
- native::VECTOR_BORROW_MUT
- pragmas::ABORTS_IF_IS_PARTIAL_PRAGMA
- pragmas::ABORTS_IF_IS_STRICT_PRAGMA
- pragmas::ADDITION_OVERFLOW_UNCHECKED_PRAGMA
- pragmas::ALWAYS_ABORTS_TEST_PRAGMA
- pragmas::ASSUME_NO_ABORT_FROM_HERE_PRAGMA
- pragmas::CONDITION_ABORT_ASSERT_PROP
- pragmas::CONDITION_ABORT_ASSUME_PROP
- pragmas::CONDITION_ABSTRACT_PROP
- pragmas::CONDITION_CHECK_ABORT_CODES_PROP
- pragmas::CONDITION_CONCRETE_PROP
- pragmas::CONDITION_DEACTIVATED_PROP
- pragmas::CONDITION_EXPORT_PROP
- pragmas::CONDITION_GLOBAL_PROP
- pragmas::CONDITION_INJECTED_PROP
- pragmas::CONDITION_ISOLATED_PROP
- pragmas::CONDITION_SUSPENDABLE_PROP
- pragmas::DELEGATE_INVARIANTS_TO_CALLER_PRAGMA
- pragmas::DISABLE_INVARIANTS_IN_BODY_PRAGMA
- pragmas::EMITS_IS_PARTIAL_PRAGMA
- pragmas::EMITS_IS_STRICT_PRAGMA
- pragmas::EXPORT_ENSURES_PRAGMA
- pragmas::FRIEND_PRAGMA
- pragmas::INTRINSIC_PRAGMA
- pragmas::OPAQUE_PRAGMA
- pragmas::REQUIRES_IF_ABORTS_PRAGMA
- pragmas::SEED_PRAGMA
- pragmas::TIMEOUT_PRAGMA
- pragmas::VERIFY_DURATION_ESTIMATE_PRAGMA
- pragmas::VERIFY_PRAGMA
- ty::BOOL_TYPE
- ty::NUM_TYPE