machine_check_exec/
lib.rs

1#![doc = include_str!("../README.md")]
2
3mod framework;
4mod model_check;
5mod precision;
6mod space;
7
8use machine_check_common::property::Property;
9use mck::{abstr, concr::FullMachine, misc::MetaWrap, refin};
10
11pub use framework::Framework;
12
13/// Abstraction and refinement strategy.
14pub struct Strategy {
15    /// Whether each input should immediately cover only a single concrete input.
16    pub naive_inputs: bool,
17    /// Whether each step output should decay to fully-unknown by default.
18    pub use_decay: bool,
19}
20
21/// Whether we are verifying the inherent property or a standard property.
22pub enum VerificationType {
23    Inherent,
24    Property(Property),
25}
26
27type AbstrPanicState<M> =
28    abstr::PanicResult<<<M as FullMachine>::Abstr as abstr::Machine<M>>::State>;
29type RefinPanicState<M> =
30    refin::PanicResult<<<M as mck::concr::FullMachine>::Refin as refin::Machine<M>>::State>;
31type AbstrInput<M> = <<M as FullMachine>::Abstr as abstr::Machine<M>>::Input;
32type RefinInput<M> = <<M as FullMachine>::Refin as refin::Machine<M>>::Input;
33type WrappedInput<M> = MetaWrap<AbstrInput<M>>;
34type WrappedState<M> = MetaWrap<AbstrPanicState<M>>;
machine_check_exec/lib.rs

machine_check_exec/
lib.rs
