Crate machine_check_common

Utility common-type crate for machine-check

This crate contains types used for communication between the formal verification tool machine-check and its utility crates or programs that call its utility crates such as machine-check-exec. Note that directly using the utility crates should be avoided unless writing an artefact that is concerned with the internal behaviour of a specific version of machine-check.

Usage and Compatibility

This crate is a utility crate for machine-check and should not be used on its own. No compatibility guarantees are made.

License

Licensed under either of Apache License, Version 2.0 or MIT license at your option. Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in this crate by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Modules

check

Common structures concerning model-checking.

property

Computation Tree Logic properties.

Structs

ExecResult

Execution result of machine-check.

ExecStats

Execution statistics.

NodeId

Node identifier. Either a root node or an actual system state.

StateId

State identifier. Represents an actual system state.

Enums

ExecError

Execution error that occured during machine-check execution.

Signedness

Signedness of a bit-vector type.

ThreeValued

An extension of a Boolean to three-valued logic.

Constants

PANIC_MSG_DIV_BY_ZERO

Message that signifies a panic due to a division by zero.

PANIC_MSG_REM_BY_ZERO

Message that signifies a panic due to a division by zero when computing the remainder.

PANIC_NUM_DIV_BY_ZERO

Number of the message that signifies a panic due to a division by zero.

PANIC_NUM_FIRST_CUSTOM

Number of the first custom message that signifies a panic.

PANIC_NUM_NO_PANIC

Number of the message that signifies no panic.

PANIC_NUM_REM_BY_ZERO

Number of the message that signifies a panic due to a division by zero when computing the remainder.