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
• simplifier::SpecRewriterPipeline
• spec_translator::SpecTranslator
• spec_translator::TranslatedSpec
• symbol::Symbol
• symbol::SymbolDisplay
• symbol::SymbolPool
• ty::Substitution
• ty::TypeDisplay
• ty::TypeInstantiationDerivation
• ty::TypeUnificationAdapter

Enums

• ast::Attribute
• ast::AttributeValue
• ast::ConditionKind
• ast::ExpData
• ast::Operation
• ast::PropertyValue
• ast::QuantKind
• ast::SpecBlockTarget
• ast::TraceKind
• ast::Value
• exp_rewriter::RewriteTarget
• model::FunctionVisibility
• model::VerificationScope
• simplifier::SimplificationPass
• ty::PrimitiveType
• ty::Type
• ty::TypeDisplayContext
• ty::TypeUnificationError
• ty::Variance

Traits

• exp_generator::ExpGenerator
• exp_rewriter::ExpRewriterFunctions
• model::GetNameString
• simplifier::SpecRewriter

Macros

• emit
• emitln

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

Typedefs

• ast::MemoryLabel
• ast::PropertyBag
• ast::TempIndex
• model::MoveIrLoc
• model::RawIndex

Constants

• model::GHOST_MEMORY_PREFIX
• model::SCRIPT_BYTECODE_FUN_NAME
• model::SCRIPT_MODULE_NAME
• 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
• well_known::EVENT_EMIT_EVENT
• well_known::TABLE_BORROW_MUT
• well_known::TABLE_TABLE
• well_known::VECTOR_BORROW_MUT