Module method_spec 

Provides the MethodSpec type, used for compositional reasoning. Also provides MethodSpecBuilder, which is used internally by the compositional reasoning macros to construct a MethodSpec from a symbolic test.

Note that these types work only when running under crux-mir-comp. Trying to use them under ordinary crux-mir will produce an error.

Structs

MethodSpec

The specification of a function. This can be used when verifying callers of the function to avoid simulating the entire function itself.

MethodSpecBuilder

Helper type used to incrementally construct a MethodSpec for a function.

Functions

clobber_globals

Replace all mutable global data with arbitrary values. This is used at the start of tests to ensure that the property holds in any context.