List of all items
Structs
- access_path::AbsAddrDisplay
- access_path::AbsStructType
- access_path::AbsStructTypeDisplay
- access_path::AccessPath
- access_path::AccessPathDisplay
- access_path::AddrDisplay
- access_path::GlobalKey
- access_path::GlobalKeyDisplay
- access_path::OffsetDisplay
- access_path::RootDisplay
- access_path_trie::AccessPathTrie
- access_path_trie::AccessPathTrieDisplay
- access_path_trie::TrieNode
- annotations::Annotations
- borrow_analysis::BorrowAnalysisProcessor
- borrow_analysis::BorrowAnnotation
- borrow_analysis::BorrowInfo
- borrow_analysis::BorrowInfoAtCodeOffset
- clean_and_optimize::CleanAndOptimizeProcessor
- compositional_analysis::SummaryCache
- data_invariant_instrumentation::DataInvariantInstrumentationProcessor
- dataflow_analysis::BlockState
- dataflow_domains::MapDomain
- dataflow_domains::SetDomain
- debug_instrumentation::DebugInstrumenter
- eliminate_imm_refs::EliminateImmRefs
- eliminate_imm_refs::EliminateImmRefsProcessor
- function_data_builder::FunctionDataBuilder
- function_data_builder::FunctionDataBuilderOptions
- function_target::FunctionData
- function_target::FunctionTarget
- function_target_pipeline::FunctionTargetPipeline
- function_target_pipeline::FunctionTargetsHolder
- function_target_pipeline::ProcessorResultDisplay
- global_invariant_analysis::GlobalInvariantAnalysisProcessor
- global_invariant_analysis::PerBytecodeRelevance
- global_invariant_analysis::PerFunctionRelevance
- global_invariant_instrumentation::GlobalInvariantInstrumentationProcessor
- global_invariant_instrumentation_v2::GlobalInvariantInstrumentationProcessorV2
- graph::Graph
- graph::NaturalLoop
- inconsistency_check::InconsistencyCheckInstrumenter
- livevar_analysis::LiveVarAnalysisProcessor
- livevar_analysis::LiveVarAnnotation
- livevar_analysis::LiveVarInfoAtCodeOffset
- loop_analysis::FatLoop
- loop_analysis::LoopAnalysisProcessor
- loop_analysis::LoopAnnotation
- memory_instrumentation::MemoryInstrumentationProcessor
- mono_analysis::MonoAnalysisProcessor
- mono_analysis::MonoInfo
- mut_ref_instrumentation::FunctionEnv
- mut_ref_instrumentation::Loc
- mut_ref_instrumentation::MutRefInstrumenter
- mutation_tester::MutationManager
- mutation_tester::MutationTester
- options::ProverOptions
- packed_types_analysis::PackedTypesProcessor
- reaching_def_analysis::ReachingDefAnnotation
- reaching_def_analysis::ReachingDefProcessor
- read_write_set_analysis::ReadWriteSetProcessor
- read_write_set_analysis::ReadWriteSetState
- read_write_set_analysis::ReadWriteSetStateDisplay
- read_write_set_analysis::SpecializedReadWriteSetState
- spec_instrumentation::SpecInstrumentationProcessor
- stackless_bytecode::AbortAction
- stackless_bytecode::AttrId
- stackless_bytecode::BorrowEdgeDisplay
- stackless_bytecode::BorrowNodeDisplay
- stackless_bytecode::BytecodeDisplay
- stackless_bytecode::Label
- stackless_bytecode::OperationDisplay
- stackless_bytecode::SpecBlockId
- stackless_bytecode_generator::StacklessBytecodeGenerator
- stackless_control_flow_graph::StacklessControlFlowGraph
- usage_analysis::MemoryUsage
- usage_analysis::UsageProcessor
- usage_analysis::UsageState
- verification_analysis::InvariantAnalysisData
- verification_analysis::InvariantRelevance
- verification_analysis::VerificationAnalysisProcessor
- verification_analysis::VerificationInfo
- verification_analysis_v2::InvariantAnalysisData
- verification_analysis_v2::VerificationAnalysisProcessorV2
- verification_analysis_v2::VerificationInfoV2
Enums
- access_path::Addr
- access_path::Offset
- access_path::Root
- dataflow_domains::JoinResult
- function_target_pipeline::FunctionVariant
- function_target_pipeline::VerificationFlavor
- mut_ref_instrumentation::Type
- options::AutoTraceLevel
- reaching_def_analysis::Def
- stackless_bytecode::AssignKind
- stackless_bytecode::BorrowEdge
- stackless_bytecode::BorrowNode
- stackless_bytecode::Bytecode
- stackless_bytecode::Constant
- stackless_bytecode::HavocKind
- stackless_bytecode::Operation
- stackless_bytecode::PropKind
- stackless_control_flow_graph::BlockContent
Traits
- access_path::AccessPathMap
- access_path::FootprintDomain
- compositional_analysis::CompositionalAnalysis
- dataflow_analysis::DataflowAnalysis
- dataflow_analysis::TransferFunctions
- dataflow_domains::AbstractDomain
- function_target_pipeline::FunctionTargetProcessor
Functions
- borrow_analysis::format_borrow_annotation
- global_invariant_analysis::get_info
- livevar_analysis::format_livevar_annotation
- mono_analysis::get_info
- packed_types_analysis::get_packed_types
- pipeline_factory::default_pipeline
- pipeline_factory::default_pipeline_with_options
- pipeline_factory::experimental_pipeline
- print_targets_for_test
- reaching_def_analysis::format_reaching_def_annotation
- read_write_set_analysis::format_read_write_set_annotation
- read_write_set_analysis::get_read_write_set
- stackless_control_flow_graph::generate_cfg_in_dot_format
- usage_analysis::get_memory_usage
- verification_analysis::get_info
- verification_analysis::is_invariant_checking_delegated
- verification_analysis::is_invariant_checking_disabled
- verification_analysis::is_invariant_suspendable
- verification_analysis_v2::debug_print_inv_set
- verification_analysis_v2::get_info