MCPcopy Create free account

hub / github.com/asymptotic-code/sui-prover / types & classes

Types & classes307 in github.com/asymptotic-code/sui-prover

⨍ Functions 2,109◇ Types & classes 307
↓ 18 callersClassTypeParameter
crates/move-model/src/model.rs:6149
↓ 11 callersClassModelParseError
Represents error resulting from model parsing.
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:2765
↓ 8 callersClassLabel
crates/move-stackless-bytecode/src/stackless_bytecode.rs:29
↓ 6 callersClassAbilityConstraint
crates/move-model/src/model.rs:6152
↓ 5 callersClassFieldId
crates/move-model/src/model.rs:193
↓ 5 callersClassModuleName
crates/move-model/src/ast.rs:69
↓ 4 callersClassDatatypeId
crates/move-model/src/model.rs:185
↓ 3 callersEnumValue
crates/move-model/src/ast.rs:41
↓ 3 callersClassVariantId
crates/move-model/src/model.rs:189
↓ 2 callersEnumConstant
crates/move-stackless-bytecode/src/stackless_bytecode.rs:97
↓ 2 callersClassFunId
crates/move-model/src/model.rs:197
↓ 2 callersClassLiveVarAnnotation
crates/move-stackless-bytecode/src/livevar_analysis.rs:35
↓ 2 callersClassNamedConstantId
crates/move-model/src/model.rs:181
↓ 2 callersClassSymbol
crates/move-model/src/symbol.rs:18
↓ 1 callersClassAccessPathTrie
crates/move-stackless-bytecode/src/access_path_trie.rs:41
↓ 1 callersClassBlock
crates/move-stackless-bytecode/src/stackless_control_flow_graph.rs:25
↓ 1 callersClassCodeWriterLabel
crates/move-model/src/code_writer.rs:46
↓ 1 callersClassEscapeAnalysisProcessor
crates/move-stackless-bytecode/src/escape_analysis.rs:332
↓ 1 callersClassExp
crates/move-stackless-bytecode/src/ast.rs:302
↓ 1 callersClassModuleId
crates/move-model/src/model.rs:177
↓ 1 callersClassPackedTypesProcessor
crates/move-stackless-bytecode/src/packed_types_analysis.rs:171
↓ 1 callersClassParameter
crates/move-model/src/model.rs:6156
↓ 1 callersClassReachingDefAnnotation
crates/move-stackless-bytecode/src/reaching_def_analysis.rs:38
↓ 1 callersClassUsageProcessor
crates/move-stackless-bytecode/src/usage_analysis.rs:275
EnumAbortAction
crates/move-stackless-bytecode/src/stackless_bytecode.rs:560
ClassAbsAddrDisplay
crates/move-stackless-bytecode/src/access_path.rs:851
ClassAbsStructType
crates/move-stackless-bytecode/src/access_path.rs:48
ClassAbsStructTypeDisplay
crates/move-stackless-bytecode/src/access_path.rs:813
EnumAbsValue
crates/move-stackless-bytecode/src/escape_analysis.rs:34
InterfaceAbstractDomain
A trait to be implemented by domains which support a join.
crates/move-stackless-bytecode/src/dataflow_domains.rs:41
ClassAccessPath
crates/move-stackless-bytecode/src/access_path.rs:103
ClassAccessPathDisplay
crates/move-stackless-bytecode/src/access_path.rs:943
InterfaceAccessPathMap
Trait for a domain that can be viewed as a partial map from access paths to values and values can be deleted using their access paths
crates/move-stackless-bytecode/src/access_path.rs:113
ClassAccessPathTrieDisplay
crates/move-stackless-bytecode/src/access_path_trie.rs:572
EnumAddr
crates/move-stackless-bytecode/src/access_path.rs:57
ClassAddrDisplay
crates/move-stackless-bytecode/src/access_path.rs:837
ClassAddressFormatter
A formatter for address
crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:940
ClassAnalysisState
crates/move-stackless-bytecode/src/clean_and_optimize.rs:69
ClassAnalyzer
crates/move-stackless-bytecode/src/mono_analysis.rs:408
ClassAnnotations
crates/move-stackless-bytecode/src/annotations.rs:17
ClassArgs
crates/sui-prover/src/main.rs:26
ClassAssertInfo
Information about an assertion in a .bpl file, for trace output.
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:164
EnumAssertsMode
crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:93
EnumAssignKind
crates/move-stackless-bytecode/src/stackless_bytecode.rs:72
ClassAttrId
crates/move-stackless-bytecode/src/stackless_bytecode.rs:43
EnumAttribute
crates/move-model/src/ast.rs:35
EnumAttributeValue
crates/move-model/src/ast.rs:29
EnumAutoTraceLevel
crates/move-stackless-bytecode/src/options.rs:10
ClassAxiomFunctionAnalysisProcessor
crates/move-stackless-bytecode/src/axiom_function_analysis.rs:14
EnumBlockContent
crates/move-stackless-bytecode/src/stackless_control_flow_graph.rs:31
ClassBlockState
crates/move-stackless-bytecode/src/dataflow_analysis.rs:20
ClassBoogieError
A boogie error.
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:93
EnumBoogieErrorKind
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:78
EnumBoogieFileMode
crates/move-prover-boogie-backend/src/boogie_backend/options.rs:91
ClassBoogieOptions
crates/move-prover-boogie-backend/src/boogie_backend/options.rs:108
ClassBoogieOutput
Output of a boogie run.
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:68
ClassBoogieTranslator
crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:81
ClassBoogieWrapper
Represents the boogie wrapper.
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:59
ClassBorrowAggregate
crates/move-prover-boogie-backend/src/boogie_backend/options.rs:71
ClassBorrowAnalysis
crates/move-stackless-bytecode/src/borrow_analysis.rs:703
ClassBorrowAnalysisProcessor
Borrow analysis processor.
crates/move-stackless-bytecode/src/borrow_analysis.rs:449
ClassBorrowAnnotation
crates/move-stackless-bytecode/src/borrow_analysis.rs:395
EnumBorrowEdge
crates/move-stackless-bytecode/src/stackless_bytecode.rs:505
ClassBorrowEdgeDisplay
crates/move-stackless-bytecode/src/stackless_bytecode.rs:1593
ClassBorrowInfo
crates/move-stackless-bytecode/src/borrow_analysis.rs:32
ClassBorrowInfoAtCodeOffset
crates/move-stackless-bytecode/src/borrow_analysis.rs:379
EnumBorrowNode
crates/move-stackless-bytecode/src/stackless_bytecode.rs:464
ClassBorrowNodeDisplay
A display object for a borrow node.
crates/move-stackless-bytecode/src/stackless_bytecode.rs:1539
ClassBplAnalysis
Complete analysis of a .bpl file for trace output. Contains parsed procedure information and call graphs, allowing call traces to be computed on-the-f
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:184
ClassBplProcInfo
Parsed information about a Boogie procedure in a .bpl file.
crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:172
ClassBuildConfig
crates/sui-prover/src/prove.rs:128
ClassBvInfo
crates/move-prover-boogie-backend/src/boogie_backend/lib.rs:89
EnumBytecode
crates/move-stackless-bytecode/src/stackless_bytecode.rs:566
ClassBytecodeDisplay
A display object for a bytecode.
crates/move-stackless-bytecode/src/stackless_bytecode.rs:1092
ClassCallInfo
crates/move-stackless-bytecode/src/spec_hierarchy.rs:26
ClassCleanAndOptimizeProcessor
crates/move-stackless-bytecode/src/clean_and_optimize.rs:25
ClassCloudConfig
crates/sui-prover/src/remote_config.rs:9
ClassCodeWriter
A helper to emit code. Supports indentation and maintains source to target location information.
crates/move-model/src/code_writer.rs:41
ClassCodeWriterData
crates/move-model/src/code_writer.rs:18
InterfaceCompositionalAnalysis
Trait that lifts an intraprocedural analysis into a bottom-up, compositional interprocedural analysis. Here, the type `Summary` represents a transform
crates/move-stackless-bytecode/src/compositional_analysis.rs:56
ClassCondition
crates/move-stackless-bytecode/src/ast.rs:200
EnumConditionKind
crates/move-stackless-bytecode/src/ast.rs:38
ClassConditionalMergeInsertionProcessor
crates/move-stackless-bytecode/src/conditional_merge_insertion.rs:590
ClassConstEntry
crates/move-model/src/builder/model_builder.rs:82
ClassCustomNativeOptions
crates/move-prover-boogie-backend/src/boogie_backend/options.rs:48
ClassData
An internal struct to represent annotation data. This carries in addition to the dynamically typed value a function for cloning this value. This works
crates/move-stackless-bytecode/src/annotations.rs:25
InterfaceDataflowAnalysis
crates/move-stackless-bytecode/src/dataflow_analysis.rs:60
EnumDatatypeData
crates/move-model/src/builder/model_builder.rs:57
ClassDatatypeEntry
crates/move-model/src/builder/model_builder.rs:46
ClassDebugInstrumenter
crates/move-stackless-bytecode/src/debug_instrumentation.rs:30
ClassDeterministicAnalysisProcessor
crates/move-stackless-bytecode/src/deterministic_analysis.rs:14
ClassDeterministicInfo
crates/move-stackless-bytecode/src/deterministic_analysis.rs:10
ClassDfQids
crates/move-stackless-bytecode/src/dynamic_field_analysis.rs:262
ClassDomRelation
crates/move-stackless-bytecode/src/graph.rs:140
ClassDotCFGBlock
CFG dot graph generation
crates/move-stackless-bytecode/src/stackless_control_flow_graph.rs:468
ClassDotCFGEdge
A dummy struct to implement fmt required by petgraph::Dot
crates/move-stackless-bytecode/src/stackless_control_flow_graph.rs:503
ClassDynamicFieldAnalysisProcessor
crates/move-stackless-bytecode/src/dynamic_field_analysis.rs:651
ClassDynamicFieldInfo
crates/move-prover-boogie-backend/src/boogie_backend/lib.rs:115
ClassDynamicFieldInfo
crates/move-stackless-bytecode/src/dynamic_field_analysis.rs:28
ClassEliminateImmRefs
crates/move-stackless-bytecode/src/eliminate_imm_refs.rs:41
next →1–100 of 307, ranked by callers