Module test_generation::summaries

Structs

• Summary
  The Summary of a bytecode instruction contains a list of Preconditions and a list of Effects.

Enums

• Effects

Functions

• instruction_summary
  Return the Summary for a bytecode instruction, instruction

Type Definitions

• FunctionInstantiableEffect
• InstantiableEffect
• NonInstantiableEffect
  A Effect is a function that transforms on AbstractState to another
• Precondition
  A Precondition is a boolean predicate on an AbstractState.