Expand description
§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§
Structs§
- Exec
Result - Execution result of machine-check.
- Exec
Stats - Execution statistics.
- NodeId
- Node identifier. Either a root node or an actual system state.
- StateId
- State identifier. Represents an actual system state.
Enums§
- Exec
Error - Execution error that occured during machine-check execution.
- Known
Param Valuation - Param
Valuation - Signedness
- Signedness of a bit-vector type.
- Three
Valued - An extension of a Boolean to three-valued logic.