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

#[macro_use]
mod op;

use crate::bitvector::abstr::dual_interval::CDualInterval;
use crate::bitvector::concr::CConcreteBitvector;
use crate::traits::forward::*;

// === SMALL-LENGTH-EXHAUSTIVE TESTS ===

// --- UNARY TESTS ---

// not and neg
uni_op_test!(bit_not);
uni_op_test!(arith_neg);

// --- BINARY TESTS ---

// arithmetic tests
bi_op_test!(add, true);
bi_op_test!(sub, true);
bi_op_test!(mul, false);
divrem_op_test!(udiv, false);
divrem_op_test!(sdiv, false);
divrem_op_test!(urem, false);
divrem_op_test!(srem, false);

// bitwise tests
bi_op_test!(bit_and, true);
bi_op_test!(bit_or, true);
bi_op_test!(bit_xor, true);

// equality and comparison tests
comparison_op_test!(eq, true);
comparison_op_test!(slt, true);
comparison_op_test!(sle, true);
comparison_op_test!(ult, true);
comparison_op_test!(ule, true);

// shift tests
bi_op_test!(logic_shl, false);
bi_op_test!(logic_shr, false);
bi_op_test!(arith_shr, true);

// --- EXTENSION TESTS ---

// extension tests
ext_op_test!(uext, false);
ext_op_test!(sext, false);