[][src]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.