Crate precept 

Modules

dispatch

fault

ghost

A compile-time-checked layer for writing read-only test properties and ghost state on top of the rest of precept.

macros_stubs

random

Macros

emit_event

expect_always

expect_always_or_unreachable

expect_reachable

expect_sometimes

expect_unreachable

function_name

observe

Runs a read-only observation block, optionally borrowing one or more GhostStates.

setup_complete

sometimes_fault

Structs

GhostState

See the enabled definition for documentation.

Constants

ENABLED

If ENABLED is false, all precept macros and faults are disabled

Functions

init

Initializes the precept library with a static dispatcher reference.

init_boxed

Initializes the precept library with a boxed dispatcher.