Functions — github.com/asymptotic-code/sui-prover

hub / github.com/asymptotic-code/sui-prover / functions

Functions2,109 in github.com/asymptotic-code/sui-prover

⨍ Functions 2,109◇ Types & classes 307

↓ 8 callersMethodsymbol

(self)

crates/move-model/src/model.rs:240

↓ 8 callersMethodto_loc

Shortcut for translating a Move AST location into ours.

crates/move-model/src/builder/model_builder.rs:102

↓ 8 callersMethodto_module_name

Converts a storage module id into an AST module name.

crates/move-model/src/model.rs:1308

↓ 8 callersMethoduid_qid

(&self)

crates/move-model/src/model.rs:2751

↓ 7 callersFunctionaddr_to_big_uint

Converts an address identifier to a number representing the address.

crates/move-model/src/lib.rs:441

↓ 7 callersMethodanalyze_function

( &self, initial_state: Self::State, instrs: &[Bytecode], cfg: &StacklessContr

crates/move-stackless-bytecode/src/dataflow_analysis.rs:61

↓ 7 callersFunctionboogie_num_type_string_capital

(num: &str, bv_flag: bool)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:509

↓ 7 callersFunctionboogie_struct_name

Return boogie name of given structure.

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:46

↓ 7 callersFunctioncheck_errors

( env: &GlobalEnv, options: &Options, error_writer: &mut W, msg: &'static str, )

crates/move-prover-boogie-backend/src/generator.rs:749

↓ 7 callersMethodextract_map

(&self)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:2309

↓ 7 callersMethodget_abilities

Get the abilities of this enum.

crates/move-model/src/model.rs:5402

↓ 7 callersFunctionget_env_info

Get the information computed by this analysis for the global environment

crates/move-stackless-bytecode/src/dynamic_field_analysis.rs:179

↓ 7 callersMethodget_name_str

(&self)

crates/move-model/src/model.rs:6241

↓ 7 callersMethodget_parameters

Return an iterator over this function's parameters

crates/move-stackless-bytecode/src/function_target.rs:212

↓ 7 callersMethodget_variants

Get an iterator for the variants, ordered by tag.

crates/move-model/src/model.rs:5418

↓ 7 callersMethodglobal_env

Get the global environment

crates/move-stackless-bytecode/src/exp_generator.rs:37

↓ 7 callersMethodis_uninterpreted

Checks if a function is marked as uninterpreted by all verified specs.

crates/move-stackless-bytecode/src/function_target_pipeline.rs:511

↓ 7 callersMethodspecialize

Specializes the type, substituting all variables bound in this substitution.

crates/move-model/src/ty.rs:556

↓ 7 callersMethodto_type

(&self)

crates/move-model/src/model.rs:373

↓ 6 callersFunctionadd_move_lang_diagnostics

(env: &mut GlobalEnv, diags: Diagnostics)

crates/move-model/src/lib.rs:360

↓ 6 callersMethodadd_type

(&mut self, ty: &Type)

crates/move-stackless-bytecode/src/mono_analysis.rs:748

↓ 6 callersMethodat_start

Delivers a location pointing to the start of this one.

crates/move-model/src/model.rs:118

↓ 6 callersFunctionboogie_make_vec_from_strings

Creates a vector from the given list of arguments.

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:390

↓ 6 callersFunctionboogie_num_literal

Generate number literals that may comes with a bv suffix in the boogie code

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:496

↓ 6 callersFunctionboogie_num_type_base

(ty: &Type)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:514

↓ 6 callersFunctionboogie_num_type_string

(num: &str, bv_flag: bool)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:504

↓ 6 callersMethodconsolidate

(&mut self)

crates/move-stackless-bytecode/src/borrow_analysis.rs:222

↓ 6 callersMethodemit_havoc

(&mut self, temp: TempIndex, havoc_kind: HavocKind)

crates/move-stackless-bytecode/src/function_data_builder.rs:326

↓ 6 callersMethoderror

Reports a type checking error.

crates/move-model/src/builder/model_builder.rs:107

↓ 6 callersMethodextract_list_ctor_prefix

Extract the arguments of a list of the form `(<ctor> element...)`.

crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:2328

↓ 6 callersMethodfield_bv_flag

Return whether a field involves bitwise operations

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:1426

↓ 6 callersMethodfile_idx_to_id

Maps an index which was obtained by `file_id_to_idx` back to a FileId.

crates/move-model/src/model.rs:792

↓ 6 callersMethodget_called_functions

Get the functions that this one calls

crates/move-model/src/model.rs:6685

↓ 6 callersMethodget_inv_by_datatype

(&self, id: &QualifiedId<DatatypeId>)

crates/move-stackless-bytecode/src/function_target_pipeline.rs:374

↓ 6 callersMethodget_ret_map

(&self)

crates/move-stackless-bytecode/src/number_operation.rs:122

↓ 6 callersMethodget_return_type

Returns return type at given index.

crates/move-model/src/model.rs:6531

↓ 6 callersMethodget_type_parameters

Returns the type parameters associated with this enum.

crates/move-model/src/model.rs:5502

↓ 6 callersMethodinto_function

Gets a FunctionEnv by id.

crates/move-model/src/model.rs:4898

↓ 6 callersMethodis_asserts_style

(&self)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:280

↓ 6 callersMethodis_number

Returns true if this is any number type.

crates/move-model/src/ty.rs:175

↓ 6 callersMethodmut_vars

(&self)

crates/move-stackless-bytecode/src/spec_global_variable_analysis.rs:33

↓ 6 callersMethodnew_label

Creates a new branching label for bytecode.

crates/move-stackless-bytecode/src/function_data_builder.rs:140

↓ 6 callersMethodpush_todo_fun

(&mut self, id: QualifiedId<FunId>, actuals: Vec<Type>)

crates/move-stackless-bytecode/src/mono_analysis.rs:699

↓ 6 callersMethodregister_annotation_formatter

Register a formatter. Each function target processor which introduces new annotations should register a formatter in order to get is value printed whe

crates/move-stackless-bytecode/src/function_target.rs:553

↓ 6 callersMethodrequires_qid

(&self)

crates/move-model/src/model.rs:2358

↓ 6 callersMethodset_next_debug_comment

Sets the debug comment which should be associated with the next instruction emitted with `self.emit_with(|id| ..)`.

crates/move-stackless-bytecode/src/function_data_builder.rs:193

↓ 6 callersMethodshould_be_used_as_func

(&self, qid: &QualifiedId<FunId>)

crates/move-model/src/model.rs:4307

↓ 6 callersMethodshould_use_opaque_as_function

(&self, write: bool)

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:3004

↓ 6 callersMethodto_loc

Shortcut for translating a Move AST location into ours.

crates/move-model/src/builder/exp_translator.rs:134

↓ 6 callersMethodtranslate_seq

Translates a sequence of items separated by `sep`.

crates/move-prover-boogie-backend/src/boogie_backend/spec_translator.rs:120

↓ 5 callersMethodaccessible

(&self)

crates/move-stackless-bytecode/src/verification_analysis.rs:37

↓ 5 callersMethodadd

( &mut self, loc: Loc, attributes: Vec<Attribute>, toplevel_attributes: expans

crates/move-model/src/model.rs:916

↓ 5 callersMethodaddress

Return the abstract address associated with `self`

crates/move-stackless-bytecode/src/access_path.rs:348

↓ 5 callersMethodanalyze_and_add_type_params

Analyzes the sequence of type parameters as they are provided via the source AST and enters them into the environment. Returns a vector for representi

crates/move-model/src/builder/exp_translator.rs:413

↓ 5 callersMethodblocks

(&self)

crates/move-stackless-bytecode/src/stackless_control_flow_graph.rs:424

↓ 5 callersFunctionboogie_bv_type

Return boogie type for a local with given signature token. TODO(tengzhang): combine with boogie_type later

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:453

↓ 5 callersFunctionboogie_field_sel

Return field selector for given field.

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:76

↓ 5 callersFunctionboogie_temp

(env: &GlobalEnv, ty: &Type, instance: usize, bv_flag: bool)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:487

↓ 5 callersFunctionboogie_well_formed_expr_bv

Create boogie well-formed boolean expression TODO(tengzhang): combine with boogie_well_formed_expr

crates/move-prover-boogie-backend/src/boogie_backend/boogie_helpers.rs:652

↓ 5 callersMethodcall_args

(&self)

crates/move-stackless-bytecode/src/ast.rs:374

↓ 5 callersMethodclone

(&self)

crates/move-stackless-bytecode/src/function_target.rs:42

↓ 5 callersMethoddests

(&self)

crates/move-stackless-bytecode/src/stackless_bytecode.rs:701

↓ 5 callersMethoddynamic_field_names_values

( &self, ty: &Type, )

crates/move-stackless-bytecode/src/dynamic_field_analysis.rs:99

↓ 5 callersMethodemit_let

Emits a let: this creates a new temporary and emits an assumption that this temporary is equal to the given expression. This can be used to abbreviate

crates/move-stackless-bytecode/src/function_data_builder.rs:206

↓ 5 callersMethodextract_type

(&self, args: &str)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:1767

↓ 5 callersMethodfind_enum

Gets an EnumEnv in this module by name.

crates/move-model/src/model.rs:5037

↓ 5 callersMethodget_all_fields

(&'env self)

crates/move-model/src/model.rs:5429

↓ 5 callersMethodget_all_inst

(&self, inst: &[Type])

crates/move-stackless-bytecode/src/usage_analysis.rs:89

↓ 5 callersMethodget_def_idx

Gets the definition index of this function.

crates/move-model/src/model.rs:6263

↓ 5 callersMethodget_default_operation_for_type

Determine the default NumOperation for a given type Returns Arithmetic for number types, Bottom for non-number types

crates/move-stackless-bytecode/src/number_operation.rs:104

↓ 5 callersMethodget_node_instantiation

Gets the type parameter instantiation associated with the given node.

crates/move-model/src/model.rs:1412

↓ 5 callersMethodget_return_count

Returns the number of return values of this function.

crates/move-model/src/model.rs:6536

↓ 5 callersMethodget_source_path

Returns the path to source file of this module.

crates/move-model/src/model.rs:4732

↓ 5 callersMethodget_struct_qid

Gets a struct by qualified id.

crates/move-model/src/model.rs:1275

↓ 5 callersMethodget_target_variants

Gets all available variants for function.

crates/move-stackless-bytecode/src/function_target_pipeline.rs:732

↓ 5 callersMethodget_type_parameter_count

Returns the number of type parameters associated with this function, this includes both the defined type parameters and the ghost type parameters. NO

crates/move-stackless-bytecode/src/function_target.rs:187

↓ 5 callersMethodget_variant

Gets a variant by its id.

crates/move-model/src/model.rs:5454

↓ 5 callersMethodglobal_qid

(&self)

crates/move-model/src/model.rs:2397

↓ 5 callersMethodis_imm_ref

(&self, idx: TempIndex)

crates/move-stackless-bytecode/src/eliminate_imm_refs.rs:72

↓ 5 callersMethodis_script_module

Returns true if this is a module representing a script.

crates/move-model/src/model.rs:4720

↓ 5 callersMethodis_statically_known

Return `true` if `self` consists only of statically known constants

crates/move-stackless-bytecode/src/access_path.rs:210

↓ 5 callersMethodis_system_spec

(&self, qid: &QualifiedId<FunId>)

crates/move-stackless-bytecode/src/package_targets.rs:787

↓ 5 callersMethodis_target

Returns true of this module is target of compilation. A non-target module is a dependency only but not explicitly requested to process.

crates/move-model/src/model.rs:4726

↓ 5 callersMethodis_verified

(&self)

crates/move-stackless-bytecode/src/spec_instrumentation.rs:281

↓ 5 callersMethodis_verified

(&self)

crates/move-stackless-bytecode/src/function_target_pipeline.rs:88

↓ 5 callersMethodjoin

(&mut self, other: &Self)

crates/move-stackless-bytecode/src/borrow_analysis.rs:364

↓ 5 callersMethodmake_trace_entry

(&self, var_name: String, value: PrettyDoc)

crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs:1354

↓ 5 callersMethodoffsets

(&self)

crates/move-stackless-bytecode/src/access_path.rs:605

↓ 5 callersMethodset

Sets annotation of type T.

crates/move-stackless-bytecode/src/annotations.rs:87

↓ 5 callersMethodsuccessors

(&self, block_id: BlockId)

crates/move-stackless-bytecode/src/stackless_control_flow_graph.rs:416

↓ 5 callersMethodtarget_specs

(&self)

crates/move-stackless-bytecode/src/package_targets.rs:1026

↓ 5 callersMethodtype_inv_qid

(&self)

crates/move-model/src/model.rs:2393

↓ 5 callersMethodunify

Unify two types, returning the unified type. This currently implements the following notion of type compatibility: - 1) References are dropped (i.e.

crates/move-model/src/ty.rs:594

↓ 5 callersMethodunion

union two DynamicFieldTypeInfo

crates/move-stackless-bytecode/src/dynamic_field_analysis.rs:112

↓ 5 callersMethodvisit

(&self, visitor: &mut F)

crates/move-model/src/ty.rs:509

↓ 4 callersMethodabort_check_functions

(&self)

crates/move-stackless-bytecode/src/package_targets.rs:1034

↓ 4 callersMethodadd_local

(&mut self, ty: Type)

crates/move-stackless-bytecode/src/function_data_builder.rs:51

↓ 4 callersMethodadd_option_type

(&mut self, inner_ty: &Type)

crates/move-stackless-bytecode/src/mono_analysis.rs:806

↓ 4 callersMethodadd_target

Adds a new function target. The target will be initialized from the Move byte code.

crates/move-stackless-bytecode/src/function_target_pipeline.rs:560

↓ 4 callersMethodadd_type

(&self, ty: &Type)

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs:1395

← previous next →201–300 of 2,109, ranked by callers