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

use crate::{bitvector::bound::BitvectorBound, concr::Boolean, forward::TypedEq};

use super::ConcreteBitvector;

impl<B: BitvectorBound> TypedEq for ConcreteBitvector<B> {
    type Output = Boolean;

    fn eq(self, rhs: Self) -> Boolean {
        assert_eq!(self.bound, rhs.bound);
        let result = self.value == rhs.value;
        Boolean::new(result)
    }

    fn ne(self, rhs: Self) -> Boolean {
        assert_eq!(self.bound, rhs.bound);
        let result = self.value != rhs.value;
        Boolean::new(result)
    }
}