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

#[cfg(test)]
mod tests;

mod arith;
mod bitwise;
mod cmp;
mod eq;
mod ext;
mod shift;
mod support;

use crate::{
    bitvector::{BitvectorBound, RBound},
    concr::ConcreteBitvector,
    misc::CBound,
};

#[derive(Clone, Copy, Hash, Serialize, Deserialize)]
pub struct ThreeValuedBitvector<B: BitvectorBound> {
    zeros: ConcreteBitvector<B>,
    ones: ConcreteBitvector<B>,
}

pub type RThreeValuedBitvector = ThreeValuedBitvector<RBound>;
pub type CThreeValuedBitvector<const W: u32> = ThreeValuedBitvector<CBound<W>>;

use serde::{Deserialize, Serialize};

pub struct InvalidZerosOnes;