Crate test_generation

Modules

• abstract_state
• borrow_graph
• bytecode_generator
• config
• control_flow_graph
• error
• summaries
• transitions

Macros

• function_instantiation_for_state
  Determine the proper type instantiation for function call in the current state.
• state_control_flow
  Predicate that is false for every state, unless control operations are allowed.
• state_create_struct
  Wrapper for enclosing the arguments of stack_pack_struct so that only the state needs to be given.
• state_create_struct_from_inst
• state_function_can_acquire_resource
  Wrapper for enclosing the arguments of function_can_acquire_resource so that only the state needs to be given.
• state_local_availability_is
  Wrapper for enclosing the arguments of local_availability_is so that only the state needs to be given.
• state_local_exists
  Wrapper for enclosing the arguments of local_exists so that only the state needs to be given.
• state_local_has_ability
  Wrapper for enclosing the arguments of state_local_has_ability so that only the state needs to be given.
• state_local_place
  Wrapper for enclosing the arguments of local_palce so that only the state needs to be given.
• state_local_set
  Wrapper for enclosing the arguments of local_set so that only the state needs to be given.
• state_local_take
  Wrapper for enclosing the arguments of local_take so that only the state needs to be given.
• state_local_take_borrow
  Wrapper for enclosing the arguments of local_take_borrow so that only the state needs to be given.
• state_memory_safe
  Wrapper for enclosing the arguments of memory_safe so that only the state needs to be given.
• state_never
  Predicate that is false for every state.
• state_register_dereference
  Wrapper for enclosing the arguments of register_dereference so that only the state needs to be given.
• state_stack_bin_op
• state_stack_function_call
  Wrapper for enclosing the arguments of stack_function_call so that only the state needs to be given.
• state_stack_function_inst_call
• state_stack_function_inst_popn
• state_stack_function_popn
  Wrapper for enclosing the arguments of stack_function_popn so that only the state needs to be given.
• state_stack_has
  Wrapper for enclosing the arguments of stack_has so that only the state needs to be given.
• state_stack_has_ability
  Wrapper for enclosing the arguments of stack_kind_is so that only the state needs to be given.
• state_stack_has_integer
  Wrapper for enclosing the arguments of stack_has_integer so that only the state needs to be given.
• state_stack_has_polymorphic_eq
  Wrapper for for enclosing the arguments of stack_has_polymorphic_eq so that only the state needs to be given.
• state_stack_has_reference
  Wrapper for enclosing the arguments of stack_has_reference so that only the state needs to be given.
• state_stack_has_struct
  Wrapper for enclosing the arguments of stack_has_struct so that only the state needs to be given.
• state_stack_has_struct_inst
• state_stack_is_castable
  Determines if the type at the top of the abstract stack is castable to the given type.
• state_stack_local_polymorphic_eq
  Wrapper for enclosing the arguments of stack_local_polymorphic_eq so that only the state needs to be given.
• state_stack_pop
  Wrapper for enclosing the arguments of stack_pop so that only the state needs to be given.
• state_stack_push
  Wrapper for enclosing the arguments of stack_push so that only the state needs to be given.
• state_stack_push_register
  Wrapper for enclosing the arguments of stack_push_register so that only the state needs to be given.
• state_stack_push_register_borrow
  Wrapper for enclosing the arguments of stack_push_register_borrow so that only the state needs to be given.
• state_stack_ref_polymorphic_eq
  Wrapper for enclosing the arguments of stack_ref_polymorphic_eq so that only the state needs to be given.
• state_stack_satisfies_function_inst_signature
• state_stack_satisfies_function_signature
  Wrapper for enclosing the arguments of stack_satisfies_function_signature so that only the state needs to be given.
• state_stack_satisfies_struct_signature
  Wrapper for enclosing the arguments of stack_satisfies_struct_signature so that only the state needs to be given.
• state_stack_struct_borrow_field
  Wrapper for enclosing the arguments of stack_struct_borrow_field so that only the state needs to be given.
• state_stack_struct_borrow_field_inst
• state_stack_struct_has_field
  Wrapper for enclosing the arguments of struct_has_field so that only the state needs to be given.
• state_stack_struct_has_field_inst
• state_stack_struct_inst_popn
  Wrapper for enclosing the arguments of state_stack_struct_inst_popn so that only the state needs to be given.
• state_stack_struct_popn
  Wrapper for enclosing the arguments of stack_struct_popn so that only the state needs to be given.
• state_stack_unpack_struct
  Wrapper for enclosing the arguments of stack_unpack_struct so that only the state needs to be given.
• state_stack_unpack_struct_inst
• state_struct_has_key
  Wrapper for enclosing the arguments of struct_abilities so that only the state needs to be given.
• state_struct_inst_has_key
• struct_instantiation_for_state
  Determine the proper type instantiation for struct in the current state.
• unpack_instantiation_for_state
  Determine the proper type instantiation for struct in the current state.
• with_ty_param
  A wrapper around type instantiation, that allows specifying an “exact” instantiation index, or if the instantiation should be inferred from the current state.

Enums

• Status

Functions

• abilities
• bytecode_generation
• module_frame_generation
• run_generation
  Run generate_bytecode for the range passed in and test each generated module on the bytecode verifier.