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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
|
; The following comment line tells the build system that if *acl2-exports*
; changes, then every book that uses this file should be recertified:
; (depends-on "build/acl2-exports.certdep" :dir :system)
(defpkg "LABEL" '(nil t))
(defpkg "JVM" '(nil t))
(DEFPKG "M5"
(set-difference-equal
(union-eq '(JVM::SCHEDULED
JVM::UNSCHEDULED
JVM::REF
JVM::LOCKED
JVM::S_LOCKED
JVM::UNLOCKED
JVM::AALOAD
JVM::AASTORE
JVM::ACONST_NULL
JVM::ALOAD
JVM::ALOAD_0
JVM::ALOAD_1
JVM::ALOAD_2
JVM::ALOAD_3
JVM::ANEWARRAY
JVM::ARETURN
JVM::ARRAYLENGTH
JVM::ASTORE
JVM::ASTORE_0
JVM::ASTORE_1
JVM::ASTORE_2
JVM::ASTORE_3
JVM::BALOAD
JVM::BASTORE
JVM::BIPUSH
JVM::CALOAD
JVM::CASTORE
JVM::DUP
JVM::DUP_X1
JVM::DUP_X2
JVM::DUP2
JVM::DUP2_X1
JVM::DUP2_X2
JVM::GETFIELD
JVM::GETSTATIC
JVM::GOTO
JVM::GOTO_W
JVM::I2B
JVM::I2C
JVM::I2L
JVM::I2S
JVM::IADD
JVM::IALOAD
JVM::IAND
JVM::IASTORE
JVM::ICONST_M1
JVM::ICONST_0
JVM::ICONST_1
JVM::ICONST_2
JVM::ICONST_3
JVM::ICONST_4
JVM::ICONST_5
JVM::IDIV
JVM::IF_ACMPEQ
JVM::IF_ACMPNE
JVM::IF_ICMPEQ
JVM::IF_ICMPGE
JVM::IF_ICMPGT
JVM::IF_ICMPLE
JVM::IF_ICMPLT
JVM::IF_ICMPNE
JVM::IFEQ
JVM::IFGE
JVM::IFGT
JVM::IFLE
JVM::IFLT
JVM::IFNE
JVM::IFNONNULL
JVM::IFNULL
JVM::IINC
JVM::ILOAD
JVM::ILOAD_0
JVM::ILOAD_1
JVM::ILOAD_2
JVM::ILOAD_3
JVM::IMUL
JVM::INEG
JVM::INSTANCEOF
JVM::INVOKESPECIAL
JVM::INVOKESTATIC
JVM::INVOKEVIRTUAL
JVM::IOR
JVM::IREM
JVM::IRETURN
JVM::ISHL
JVM::ISHR
JVM::ISTORE
JVM::ISTORE_0
JVM::ISTORE_1
JVM::ISTORE_2
JVM::ISTORE_3
JVM::ISUB
JVM::IUSHR
JVM::IXOR
JVM::JSR
JVM::JSR_W
JVM::L2I
JVM::LADD
JVM::LALOAD
JVM::LAND
JVM::LASTORE
JVM::LCMP
JVM::LCONST_0
JVM::LCONST_1
JVM::LDC
JVM::LDC_W
JVM::LDC2_W
JVM::LDIV
JVM::LLOAD
JVM::LLOAD_0
JVM::LLOAD_1
JVM::LLOAD_2
JVM::LLOAD_3
JVM::LMUL
JVM::LNEG
JVM::LOR
JVM::LREM
JVM::LRETURN
JVM::LSHL
JVM::LSHR
JVM::LSTORE
JVM::LSTORE_0
JVM::LSTORE_1
JVM::LSTORE_2
JVM::LSTORE_3
JVM::LSUB
JVM::LUSHR
JVM::LXOR
JVM::MONITORENTER
JVM::MONITOREXIT
JVM::MULTIANEWARRAY
JVM::NEW
JVM::NEWARRAY
JVM::NOP
JVM::POP
JVM::POP2
JVM::PUTFIELD
JVM::PUTSTATIC
JVM::RET
JVM::RETURN
JVM::SALOAD
JVM::SASTORE
JVM::SIPUSH
JVM::SWAP
ASSOC-EQUAL LEN NTH ZP SYNTAXP
QUOTEP FIX NFIX E0-ORDINALP E0-ORD-<)
(union-eq *acl2-exports*
*common-lisp-symbols-from-main-lisp-package*))
'(PC PROGRAM PUSH POP RETURN REVERSE STEP ++)))
(certify-book "m5" ? t)
|
