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

use crate::{
    abstr::{
        combination::DomainCombination, combined::RCombinedBitvector,
        three_valued::RThreeValuedBitvector,
    },
    bitvector::refin::combined::RCombinedMark,
    misc::RBound,
    traits::misc::Meta,
};

impl<D: DomainCombination<RBound, Left = RThreeValuedBitvector>> Meta<RCombinedBitvector<D>>
    for RCombinedMark<D>
{
    fn proto_first(&self) -> RCombinedBitvector<D> {
        RCombinedBitvector::from_left(self.0.proto_first())
    }

    fn proto_increment(&self, proto: &mut RCombinedBitvector<D>) -> bool {
        let mut three_valued = *proto.left();

        let result = self.0.proto_increment(&mut three_valued);
        *proto = RCombinedBitvector::from_left(three_valued);
        result
    }
}