Crate crucible 

Re-exports

pub use self::symbolic::Symbolic;

Modules

bitvector

cryptol

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.

sym_bytes

symbolic

Macros

crucible_assert

Assert that a condition holds. During symbolic testing, crux-mir will search for an assignment to the symbolic variables that violates an assertion.

crucible_assert_unreachable

Assert that the current code is unreachable. This is similar to the standard unreachable!() macro, but uses crucible_assert! internally.

crucible_assume

Assume that a condition holds. crux-mir will not consider assignments to the symbolic variables that violate an assumption.

crucible_assume_unreachable

Assume that the current code is unreachable. This is similar to crucible_assume!(false), but also returns !, so it can be used in positions where a return value is expected.

cryptol

Structs

TypedAllocator

Functions

concretize

Given a symbolic value, choose an arbitrary instance that satisfies the current path condition. This function operates recursively: a call to concretize(&(x, y)) (where x and y are symbolic integers) will produce a concrete result like &(1, 2).

crucible_i8Deprecated

crucible_i16Deprecated

crucible_i32Deprecated

crucible_i64Deprecated

crucible_u8Deprecated

crucible_u16Deprecated

crucible_u32Deprecated

crucible_u64Deprecated

dump_rv

Print a Crucible RegValue to stderr. Most TypeReprs used by crucible-mir are supported, but not all; if T uses an unsupported TypeRepr, this may print [unsupported] or throw an error.

dump_what4

Print a what4 expression to stderr. T must have a primitive/base type for its Crucible representation.

override_

Install g as an override for f.

print_str

Print a string during symbolic execution. The string must be concrete.