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

use std::cmp::Ordering;

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

use super::ConcreteBitvector;

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

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

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

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

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

impl<B: BitvectorBound> ConcreteBitvector<B> {
    pub fn unsigned_cmp(&self, rhs: &Self) -> Ordering {
        assert_eq!(self.bound, rhs.bound);
        self.to_u64().cmp(&rhs.to_u64())
    }
    pub fn signed_cmp(&self, rhs: &Self) -> Ordering {
        assert_eq!(self.bound, rhs.bound);
        self.to_i64().cmp(&rhs.to_i64())
    }
}