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 AbstrInput<M> = <<M as FullMachine>::Abstr as abstr::Machine<M>>::Input;
28type RefinInput<M> = <<M as FullMachine>::Refin as refin::Machine<M>>::Input;
29
30type AbstrParam<M> = <<M as FullMachine>::Abstr as abstr::Machine<M>>::Param;
31type RefinParam<M> = <<M as FullMachine>::Refin as refin::Machine<M>>::Param;
32
33type AbstrState<M> = <<M as FullMachine>::Abstr as abstr::Machine<M>>::State;
34type RefinState<M> = <<M as FullMachine>::Refin as refin::Machine<M>>::State;
35
36type AbstrPanicState<M> = abstr::PanicResult<AbstrState<M>>;
37type RefinPanicState<M> = refin::PanicResult<RefinState<M>>;
38
39type WrappedInput<M> = MetaWrap<AbstrInput<M>>;
40type WrappedParam<M> = MetaWrap<AbstrParam<M>>;
41type WrappedState<M> = MetaWrap<AbstrPanicState<M>>;
machine_check_exec/lib.rs

machine_check_exec/
lib.rs
