bv/correct_test_results at master · termite2/bv · GitHub

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
termToCTerm test
(x{16}++y{16}) --> x{16}+65536*y{16}
256*x{16}[0:7]{16} --> 256*x{16}[0:7]
(x{16}++y{16})[8:23] --> x{16}[8:15]+256*y{16}[0:7]
(x{16}[0:7]++x{16}[8:15]) --> x{16}
(~x{16}[0:7]) --> 255*x{16}[0:7]+255{8}
(~(x{16}++0{16})[8:23]) --> 65535*x{16}[8:15]+65535{16}
(~(0{16}++0{16})[8:23]) --> 65535{16}
(~(65535{16}++x{16})[8:23]) --> 65280*x{16}[0:7]+65280{16}
(~(x{16}++y{16})[8:23]) --> 65535*x{16}[8:15]+65280*y{16}[0:7]+65535{16}
(~((x{16}++y{16})++z{16})[8:39]) --> 4294967295*x{16}[8:15]+4294967040*y{16}+4278190080*z{16}[0:7]+4294967295{32}
((x{16}++y{16})++z{16})[8:39] --> x{16}[8:15]+256*y{16}+16777216*z{16}[0:7]

atomToCAtom test
x{16} == y{16} --> Right x{16} == y{16}
y{16} == x{16} --> Right x{16} == y{16}
0{16} == x{16} --> Right x{16} == 0{16}
0{16} == (~(x{16}++y{16})[8:23]) --> Right x{16}[8:15] == 65280*y{16}[0:7]+65535{16}

existential quantification test
Ex x{16}.x{16} == y{16} = Just (Left True)
Ex x{16}.x{16} != y{16} = Just (Left True)
Ex x{16}.x{16} != y{16} /\ x{16} == z{16} = Just (Right [y{16} != z{16}])
Ex x{16}.x{16}[0:7] == (y{16}+4{16})[0:7] /\ x{16} == (z{16}+8{16}) = Nothing
Ex x{16}.x{16} == (y{16}+4{16}) /\ x{16} == (z{16}+8{16}) = Just (Right [y{16} == z{16}+4{16}])