|
41561
|
1 |
/*********************************************************/
|
|
|
2 |
/*Proof Rule Declarations*/
|
|
|
3 |
/*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
|
|
|
4 |
/*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
|
|
|
5 |
/*********************************************************/
|
|
|
6 |
|
|
|
7 |
|
|
|
8 |
/*DATE : 29-NOV-2010 14:30:19.87*/
|
|
|
9 |
|
|
|
10 |
/*procedure RMD.Round*/
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
rule_family round_rules:
|
|
|
14 |
X requires [X:any] &
|
|
|
15 |
X <= Y requires [X:ire, Y:ire] &
|
|
|
16 |
X >= Y requires [X:ire, Y:ire].
|
|
|
17 |
|
|
|
18 |
round_rules(1): integer__size >= 0 may_be_deduced.
|
|
|
19 |
round_rules(2): integer__first may_be_replaced_by -2147483648.
|
|
|
20 |
round_rules(3): integer__last may_be_replaced_by 2147483647.
|
|
|
21 |
round_rules(4): integer__base__first may_be_replaced_by -2147483648.
|
|
|
22 |
round_rules(5): integer__base__last may_be_replaced_by 2147483647.
|
|
|
23 |
round_rules(6): interfaces__unsigned_32__size >= 0 may_be_deduced.
|
|
|
24 |
round_rules(7): interfaces__unsigned_32__first may_be_replaced_by 0.
|
|
|
25 |
round_rules(8): interfaces__unsigned_32__last may_be_replaced_by 4294967295.
|
|
|
26 |
round_rules(9): interfaces__unsigned_32__base__first may_be_replaced_by 0.
|
|
|
27 |
round_rules(10): interfaces__unsigned_32__base__last may_be_replaced_by 4294967295.
|
|
|
28 |
round_rules(11): interfaces__unsigned_32__modulus may_be_replaced_by 4294967296.
|
|
|
29 |
round_rules(12): wordops__word__size >= 0 may_be_deduced.
|
|
|
30 |
round_rules(13): wordops__word__first may_be_replaced_by 0.
|
|
|
31 |
round_rules(14): wordops__word__last may_be_replaced_by 4294967295.
|
|
|
32 |
round_rules(15): wordops__word__base__first may_be_replaced_by 0.
|
|
|
33 |
round_rules(16): wordops__word__base__last may_be_replaced_by 4294967295.
|
|
|
34 |
round_rules(17): wordops__word__modulus may_be_replaced_by 4294967296.
|
|
|
35 |
round_rules(18): wordops__rotate_amount__size >= 0 may_be_deduced.
|
|
|
36 |
round_rules(19): wordops__rotate_amount__first may_be_replaced_by 0.
|
|
|
37 |
round_rules(20): wordops__rotate_amount__last may_be_replaced_by 15.
|
|
|
38 |
round_rules(21): wordops__rotate_amount__base__first may_be_replaced_by -2147483648.
|
|
|
39 |
round_rules(22): wordops__rotate_amount__base__last may_be_replaced_by 2147483647.
|
|
|
40 |
round_rules(23): word__size >= 0 may_be_deduced.
|
|
|
41 |
round_rules(24): word__first may_be_replaced_by 0.
|
|
|
42 |
round_rules(25): word__last may_be_replaced_by 4294967295.
|
|
|
43 |
round_rules(26): word__base__first may_be_replaced_by 0.
|
|
|
44 |
round_rules(27): word__base__last may_be_replaced_by 4294967295.
|
|
|
45 |
round_rules(28): word__modulus may_be_replaced_by 4294967296.
|
|
|
46 |
round_rules(29): chain__size >= 0 may_be_deduced.
|
|
|
47 |
round_rules(30): A = B may_be_deduced_from
|
|
|
48 |
[goal(checktype(A,chain)),
|
|
|
49 |
goal(checktype(B,chain)),
|
|
|
50 |
fld_h0(A) = fld_h0(B),
|
|
|
51 |
fld_h1(A) = fld_h1(B),
|
|
|
52 |
fld_h2(A) = fld_h2(B),
|
|
|
53 |
fld_h3(A) = fld_h3(B),
|
|
|
54 |
fld_h4(A) = fld_h4(B)].
|
|
|
55 |
round_rules(31): block_index__size >= 0 may_be_deduced.
|
|
|
56 |
round_rules(32): block_index__first may_be_replaced_by 0.
|
|
|
57 |
round_rules(33): block_index__last may_be_replaced_by 15.
|
|
|
58 |
round_rules(34): block_index__base__first <= block_index__base__last may_be_deduced.
|
|
|
59 |
round_rules(35): block_index__base__first <= block_index__first may_be_deduced.
|
|
|
60 |
round_rules(36): block_index__base__last >= block_index__last may_be_deduced.
|
|
|
61 |
round_rules(37): round_index__size >= 0 may_be_deduced.
|
|
|
62 |
round_rules(38): round_index__first may_be_replaced_by 0.
|
|
|
63 |
round_rules(39): round_index__last may_be_replaced_by 79.
|
|
|
64 |
round_rules(40): round_index__base__first <= round_index__base__last may_be_deduced.
|
|
|
65 |
round_rules(41): round_index__base__first <= round_index__first may_be_deduced.
|
|
|
66 |
round_rules(42): round_index__base__last >= round_index__last may_be_deduced.
|
|
|
67 |
round_rules(43): chain_pair__size >= 0 may_be_deduced.
|
|
|
68 |
round_rules(44): A = B may_be_deduced_from
|
|
|
69 |
[goal(checktype(A,chain_pair)),
|
|
|
70 |
goal(checktype(B,chain_pair)),
|
|
|
71 |
fld_left(A) = fld_left(B),
|
|
|
72 |
fld_right(A) = fld_right(B)].
|
|
|
73 |
round_rules(45): rotate_amount__size >= 0 may_be_deduced.
|
|
|
74 |
round_rules(46): rotate_amount__first may_be_replaced_by 0.
|
|
|
75 |
round_rules(47): rotate_amount__last may_be_replaced_by 15.
|
|
|
76 |
round_rules(48): rotate_amount__base__first may_be_replaced_by -2147483648.
|
|
|
77 |
round_rules(49): rotate_amount__base__last may_be_replaced_by 2147483647.
|