mck 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69

#![doc = include_str!("../README.md")]

mod array;
mod bitvector;
mod boolean;
mod panic;
mod traits;
mod value;

pub use value::{KnownParamValuation, ParamValuation, ThreeValued};

#[doc(hidden)]
pub mod concr {
    pub use super::array::concr::*;
    pub use super::bitvector::concr::*;
    pub use super::boolean::concr::*;
    pub use super::panic::concr::*;
    pub use super::traits::concr::*;

    pub type Bitvector<const W: u32> = super::bitvector::concr::CConcreteBitvector<W>;
}

#[doc(hidden)]
pub mod abstr {
    pub use super::array::abstr::*;
    pub use super::bitvector::abstr::*;
    pub use super::boolean::abstr::*;
    pub use super::panic::abstr::*;
    pub use super::traits::abstr::*;
    pub use super::value::abstr::*;
}

#[doc(hidden)]
pub mod refin {
    pub use super::array::refin::*;
    pub use super::bitvector::refin::*;
    pub use super::boolean::refin::*;
    pub use super::value::refin::*;
}

#[doc(hidden)]
pub mod forward {

    pub use super::traits::forward::*;

    pub type Bitvector<const W: u32> = super::abstr::CBitvector<W>;
    pub type Array<const I: u32, const E: u32> = super::abstr::CArray<I, E>;
    pub type Boolean = super::abstr::Boolean;

    pub use super::panic::abstr::*;
    pub use super::traits::abstr::*;
}

#[doc(hidden)]
pub mod backward {
    pub use super::array::refin::*;
    pub use super::bitvector::refin::*;
    pub use super::boolean::refin::*;
    pub use super::traits::backward::*;
}

#[doc(hidden)]
pub mod misc {
    pub use super::array::light::*;
    pub use super::bitvector::{BitvectorBound, CBound, RBound};
    pub use super::panic::message::*;
    pub use super::traits::misc::*;
    pub use super::value::Interpretation;
}