 |
|
|
|
.. (parent) |
 |
d |
rwxr-xr-x |
8,192 |
.sys
|
 |
- |
rw-r--r-- |
166 |
AALOAD.acl2
|
 |
- |
rw-r--r-- |
20,609 |
AALOAD.lisp
|
 |
- |
rw-r--r-- |
167 |
AASTORE.acl2
|
 |
- |
rw-r--r-- |
21,432 |
AASTORE.lisp
|
 |
- |
rw-r--r-- |
171 |
ACONST_NULL.acl2
|
 |
- |
rw-r--r-- |
9,595 |
ACONST_NULL.lisp
|
 |
- |
rw-r--r-- |
165 |
ALOAD.acl2
|
 |
- |
rw-r--r-- |
13,449 |
ALOAD.lisp
|
 |
- |
rw-r--r-- |
169 |
ANEWARRAY.acl2
|
 |
- |
rw-r--r-- |
13,992 |
ANEWARRAY.lisp
|
 |
- |
rw-r--r-- |
166 |
ASTORE.acl2
|
 |
- |
rw-r--r-- |
19,037 |
ASTORE.lisp
|
 |
- |
rw-r--r-- |
168 |
GETFIELD.acl2
|
 |
- |
rw-r--r-- |
41,899 |
GETFIELD.lisp
|
 |
- |
rw-r--r-- |
164 |
IFEQ.acl2
|
 |
- |
rw-r--r-- |
11,415 |
IFEQ.lisp
|
 |
- |
rw-r--r-- |
188 |
base-REFp-reference-type-s.acl2
|
 |
- |
rw-r--r-- |
2,031 |
base-REFp-reference-type-s.lisp
|
 |
- |
rw-r--r-- |
153 |
base-array-facts.acl2
|
 |
- |
rw-r--r-- |
4,493 |
base-array-facts.lisp
|
 |
- |
rw-r--r-- |
147 |
base-array.acl2
|
 |
- |
rw-r--r-- |
32,375 |
base-array.lisp
|
 |
- |
rw-r--r-- |
169 |
base-bcv-check-monotonic-support.acl2
|
 |
- |
rw-r--r-- |
36,906 |
base-bcv-check-monotonic-support.lisp
|
 |
- |
rw-r--r-- |
161 |
base-bcv-check-monotonic.acl2
|
 |
- |
rw-r--r-- |
24,294 |
base-bcv-check-monotonic.lisp
|
 |
- |
rw-r--r-- |
186 |
base-bcv-djvm-assignable.acl2
|
 |
- |
rw-r--r-- |
18,027 |
base-bcv-djvm-assignable.lisp
|
 |
- |
rw-r--r-- |
159 |
base-bcv-djvm-getfield.acl2
|
 |
- |
rw-r--r-- |
13,249 |
base-bcv-djvm-getfield.lisp
|
 |
- |
rw-r--r-- |
172 |
base-bcv-fact-array-type-assignable.acl2
|
 |
- |
rw-r--r-- |
12,874 |
base-bcv-fact-array-type-assignable.lisp
|
 |
- |
rw-r--r-- |
179 |
base-bcv-fact-isAssignable-len-pushOpstack.acl2
|
 |
- |
rw-r--r-- |
5,035 |
base-bcv-fact-isAssignable-len-pushOpstack.lisp
|
 |
- |
rw-r--r-- |
189 |
base-bcv-fact-isAssignable-prefixclass-not-category2.acl2
|
 |
- |
rw-r--r-- |
440 |
base-bcv-fact-isAssignable-prefixclass-not-category2.lisp
|
 |
- |
rw-r--r-- |
171 |
base-bcv-fact-isMatchingType-array.acl2
|
 |
- |
rw-r--r-- |
1,213 |
base-bcv-fact-isMatchingType-array.lisp
|
 |
- |
rw-r--r-- |
181 |
base-bcv-fact-isMatchingType-canPopCategory1.acl2
|
 |
- |
rw-r--r-- |
4,836 |
base-bcv-fact-isMatchingType-canPopCategory1.lisp
|
 |
- |
rw-r--r-- |
175 |
base-bcv-fact-isMatchingType-consp-stk.acl2
|
 |
- |
rw-r--r-- |
1,694 |
base-bcv-fact-isMatchingType-consp-stk.lisp
|
 |
- |
rw-r--r-- |
178 |
base-bcv-fact-isMatchingType-isAssignable.acl2
|
 |
- |
rw-r--r-- |
1,660 |
base-bcv-fact-isMatchingType-isAssignable.lisp
|
 |
- |
rw-r--r-- |
188 |
base-bcv-fact-isMatchingType-isAssignableTo-support.acl2
|
 |
- |
rw-r--r-- |
76,830 |
base-bcv-fact-isMatchingType-isAssignableTo-support.lisp
|
 |
- |
rw-r--r-- |
180 |
base-bcv-fact-isMatchingType-isAssignableTo.acl2
|
 |
- |
rw-r--r-- |
2,495 |
base-bcv-fact-isMatchingType-isAssignableTo.lisp
|
 |
- |
rw-r--r-- |
180 |
base-bcv-fact-isMatchingType-suitable-value.acl2
|
 |
- |
rw-r--r-- |
21,980 |
base-bcv-fact-isMatchingType-suitable-value.lisp
|
 |
- |
rw-r--r-- |
183 |
base-bcv-fact-isMatchingType-value-initialized.acl2
|
 |
- |
rw-r--r-- |
4,739 |
base-bcv-fact-isMatchingType-value-initialized.lisp
|
 |
- |
rw-r--r-- |
179 |
base-bcv-fact-nth-opstack-specific-env-sig.acl2
|
 |
- |
rw-r--r-- |
2,297 |
base-bcv-fact-nth-opstack-specific-env-sig.lisp
|
 |
- |
rw-r--r-- |
162 |
base-bcv-fact-nth-opstack.acl2
|
 |
- |
rw-r--r-- |
3,182 |
base-bcv-fact-nth-opstack.lisp
|
 |
- |
rw-r--r-- |
165 |
base-bcv-frame-sig-expansion.acl2
|
 |
- |
rw-r--r-- |
29,712 |
base-bcv-frame-sig-expansion.lisp
|
 |
- |
rw-r--r-- |
189 |
base-bcv-isAssignable-facts.acl2
|
 |
- |
rw-r--r-- |
13,920 |
base-bcv-isAssignable-facts.lisp
|
 |
- |
rw-r--r-- |
152 |
base-bcv-locals.acl2
|
 |
- |
rw-r--r-- |
12,687 |
base-bcv-locals.lisp
|
 |
- |
rw-r--r-- |
167 |
base-bcv-modify-local-variable.acl2
|
 |
- |
rw-r--r-- |
7,876 |
base-bcv-modify-local-variable.lisp
|
 |
- |
rw-r--r-- |
171 |
base-bcv-protected-check-monotonic.acl2
|
 |
- |
rw-r--r-- |
3,463 |
base-bcv-protected-check-monotonic.lisp
|
 |
- |
rw-r--r-- |
160 |
base-bcv-step-monotonic.acl2
|
 |
- |
rw-r--r-- |
11,430 |
base-bcv-step-monotonic.lisp
|
 |
- |
rw-r--r-- |
153 |
base-bcv-support.acl2
|
 |
- |
rw-r--r-- |
60,967 |
base-bcv-support.lisp
|
 |
- |
rw-r--r-- |
157 |
base-bcv-update-heap.acl2
|
 |
- |
rw-r--r-- |
349 |
base-bcv-update-heap.lisp
|
 |
- |
rw-r--r-- |
169 |
base-bcv-valid-local-index-facts.acl2
|
 |
- |
rw-r--r-- |
5,339 |
base-bcv-valid-local-index-facts.lisp
|
 |
- |
rw-r--r-- |
145 |
base-bcv.acl2
|
 |
- |
rw-r--r-- |
7,229 |
base-bcv.lisp
|
 |
- |
rw-r--r-- |
2,881 |
base-bind-free.lisp
|
 |
- |
rw-r--r-- |
155 |
base-branch-instrs.acl2
|
 |
- |
rw-r--r-- |
712 |
base-branch-instrs.lisp
|
 |
- |
rw-r--r-- |
191 |
base-build-an-array-instance-creates-consistent-object.acl2
|
 |
- |
rw-r--r-- |
3,472 |
base-build-an-array-instance-creates-consistent-object.lisp
|
 |
- |
rw-r--r-- |
212 |
base-canPop1-consistent-sig-stack-consistent-value.acl2
|
 |
- |
rw-r--r-- |
7,700 |
base-canPop1-consistent-sig-stack-consistent-value.lisp
|
 |
- |
rw-r--r-- |
171 |
base-consistent-object-m6-getfield.acl2
|
 |
- |
rw-r--r-- |
54,244 |
base-consistent-object-m6-getfield.lisp
|
 |
- |
rw-r--r-- |
181 |
base-consistent-state-class-names-are-string.acl2
|
 |
- |
rw-r--r-- |
661 |
base-consistent-state-class-names-are-string.lisp
|
 |
- |
rw-r--r-- |
184 |
base-consistent-state-consistent-object-support.acl2
|
 |
- |
rw-r--r-- |
2,702 |
base-consistent-state-consistent-object-support.lisp
|
 |
- |
rw-r--r-- |
176 |
base-consistent-state-consistent-object.acl2
|
 |
- |
rw-r--r-- |
1,135 |
base-consistent-state-consistent-object.lisp
|
 |
- |
rw-r--r-- |
171 |
base-consistent-state-good-icl-etc.acl2
|
 |
- |
rw-r--r-- |
7,764 |
base-consistent-state-good-icl-etc.lisp
|
 |
- |
rw-r--r-- |
177 |
base-consistent-state-load-class-support.acl2
|
 |
- |
rw-r--r-- |
19,205 |
base-consistent-state-load-class-support.lisp
|
 |
- |
rw-r--r-- |
169 |
base-consistent-state-load-class.acl2
|
 |
- |
rw-r--r-- |
1,909 |
base-consistent-state-load-class.lisp
|
 |
- |
rw-r--r-- |
174 |
base-consistent-state-lookupfield-bcv.acl2
|
 |
- |
rw-r--r-- |
11,105 |
base-consistent-state-lookupfield-bcv.lisp
|
 |
- |
rw-r--r-- |
178 |
base-consistent-state-lookupfield-support.acl2
|
 |
- |
rw-r--r-- |
53,634 |
base-consistent-state-lookupfield-support.lisp
|
 |
- |
rw-r--r-- |
170 |
base-consistent-state-lookupfield.acl2
|
 |
- |
rw-r--r-- |
4,666 |
base-consistent-state-lookupfield.lisp
|
 |
- |
rw-r--r-- |
177 |
base-consistent-state-make-state-general.acl2
|
 |
- |
rw-r--r-- |
17,547 |
base-consistent-state-make-state-general.lisp
|
 |
- |
rw-r--r-- |
169 |
base-consistent-state-make-state.acl2
|
 |
- |
rw-r--r-- |
14,392 |
base-consistent-state-make-state.lisp
|
 |
- |
rw-r--r-- |
183 |
base-consistent-state-modifying-object-support.acl2
|
 |
- |
rw-r--r-- |
15,052 |
base-consistent-state-modifying-object-support.lisp
|
 |
- |
rw-r--r-- |
175 |
base-consistent-state-modifying-object.acl2
|
 |
- |
rw-r--r-- |
3,140 |
base-consistent-state-modifying-object.lisp
|
 |
- |
rw-r--r-- |
163 |
base-consistent-state-more.acl2
|
 |
- |
rw-r--r-- |
14,232 |
base-consistent-state-more.lisp
|
 |
- |
rw-r--r-- |
180 |
base-consistent-state-pushCategory2-support.acl2
|
 |
- |
rw-r--r-- |
26,881 |
base-consistent-state-pushCategory2-support.lisp
|
 |
- |
rw-r--r-- |
172 |
base-consistent-state-pushCategory2.acl2
|
 |
- |
rw-r--r-- |
600 |
base-consistent-state-pushCategory2.lisp
|
 |
- |
rw-r--r-- |
173 |
base-consistent-state-state-set-heap.acl2
|
 |
- |
rw-r--r-- |
1,204 |
base-consistent-state-state-set-heap.lisp
|
 |
- |
rw-r--r-- |
174 |
base-consistent-state-step-definition.acl2
|
 |
- |
rw-r--r-- |
1,917 |
base-consistent-state-step-definition.lisp
|
 |
- |
rw-r--r-- |
174 |
base-consistent-state-step-properties.acl2
|
 |
- |
rw-r--r-- |
8,683 |
base-consistent-state-step-properties.lisp
|
 |
- |
rw-r--r-- |
171 |
base-consistent-state-update-trace.acl2
|
 |
- |
rw-r--r-- |
1,093 |
base-consistent-state-update-trace.lisp
|
 |
- |
rw-r--r-- |
158 |
base-consistent-state.acl2
|
 |
- |
rw-r--r-- |
51,680 |
base-consistent-state.lisp
|
 |
- |
rw-r--r-- |
181 |
base-djvm-functions.acl2
|
 |
- |
rw-r--r-- |
306 |
base-djvm-functions.lisp
|
 |
- |
rw-r--r-- |
147 |
base-extra.acl2
|
 |
- |
rw-r--r-- |
5,562 |
base-extra.lisp
|
 |
- |
rw-r--r-- |
168 |
base-fatal-errorflag-not-earsed.acl2
|
 |
- |
rw-r--r-- |
285 |
base-fatal-errorflag-not-earsed.lisp
|
 |
- |
rw-r--r-- |
171 |
base-frame-sig-after-class-loading.acl2
|
 |
- |
rw-r--r-- |
10,327 |
base-frame-sig-after-class-loading.lisp
|
 |
- |
rw-r--r-- |
169 |
base-frame-sig-expansion-support.acl2
|
 |
- |
rw-r--r-- |
10,489 |
base-frame-sig-expansion-support.lisp
|
 |
- |
rw-r--r-- |
161 |
base-frame-sig-expansion.acl2
|
 |
- |
rw-r--r-- |
64,571 |
base-frame-sig-expansion.lisp
|
 |
- |
rw-r--r-- |
169 |
base-good-java-type-valid-type-s.acl2
|
 |
- |
rw-r--r-- |
2,997 |
base-good-java-type-valid-type-s.lisp
|
 |
- |
rw-r--r-- |
175 |
base-isAssignableTo-properties-support.acl2
|
 |
- |
rw-r--r-- |
7,684 |
base-isAssignableTo-properties-support.lisp
|
 |
- |
rw-r--r-- |
167 |
base-isAssignableTo-properties.acl2
|
 |
- |
rw-r--r-- |
826 |
base-isAssignableTo-properties.lisp
|
 |
- |
rw-r--r-- |
178 |
base-judgement-after-load-class-no-change.acl2
|
 |
- |
rw-r--r-- |
16,029 |
base-judgement-after-load-class-no-change.lisp
|
 |
- |
rw-r--r-- |
183 |
base-load-class-normalize-assignmentcompatible.acl2
|
 |
- |
rw-r--r-- |
5,369 |
base-load-class-normalize-assignmentcompatible.lisp
|
 |
- |
rw-r--r-- |
1,042 |
base-load-class-normalize-class-by-name-support.acl2
|
 |
- |
rw-r--r-- |
6,756 |
base-load-class-normalize-class-by-name-support.lisp
|
 |
- |
rw-r--r-- |
176 |
base-load-class-normalize-class-by-name.acl2
|
 |
- |
rw-r--r-- |
795 |
base-load-class-normalize-class-by-name.lisp
|
 |
- |
rw-r--r-- |
177 |
base-load-class-normalize-deref2-support.acl2
|
 |
- |
rw-r--r-- |
9,596 |
base-load-class-normalize-deref2-support.lisp
|
 |
- |
rw-r--r-- |
169 |
base-load-class-normalize-deref2.acl2
|
 |
- |
rw-r--r-- |
1,472 |
base-load-class-normalize-deref2.lisp
|
 |
- |
rw-r--r-- |
185 |
base-load-class-normalize-isAssignableTo-support.acl2
|
 |
- |
rw-r--r-- |
10,716 |
base-load-class-normalize-isAssignableTo-support.lisp
|
 |
- |
rw-r--r-- |
177 |
base-load-class-normalize-isAssignableTo.acl2
|
 |
- |
rw-r--r-- |
669 |
base-load-class-normalize-isAssignableTo.lisp
|
 |
- |
rw-r--r-- |
170 |
base-load-class-normalize-support.acl2
|
 |
- |
rw-r--r-- |
12,078 |
base-load-class-normalize-support.lisp
|
 |
- |
rw-r--r-- |
173 |
base-load-class-normalize-when-found.acl2
|
 |
- |
rw-r--r-- |
6,362 |
base-load-class-normalize-when-found.lisp
|
 |
- |
rw-r--r-- |
162 |
base-load-class-normalize.acl2
|
 |
- |
rw-r--r-- |
9,864 |
base-load-class-normalize.lisp
|
 |
- |
rw-r--r-- |
174 |
base-loader-preserve-consistent-state.acl2
|
 |
- |
rw-r--r-- |
250,579 |
base-loader-preserve-consistent-state.lisp
|
 |
- |
rw-r--r-- |
148 |
base-locals.acl2
|
 |
- |
rw-r--r-- |
2,904 |
base-locals.lisp
|
 |
- |
rw-r--r-- |
173 |
base-lookupfield-fieldname-normalize.acl2
|
 |
- |
rw-r--r-- |
1,763 |
base-lookupfield-fieldname-normalize.lisp
|
 |
- |
rw-r--r-- |
168 |
base-lookupfield-get-field-type.acl2
|
 |
- |
rw-r--r-- |
3,473 |
base-lookupfield-get-field-type.lisp
|
 |
- |
rw-r--r-- |
170 |
base-m6-getfield-consistent-value.acl2
|
 |
- |
rw-r--r-- |
2,778 |
base-m6-getfield-consistent-value.lisp
|
 |
- |
rw-r--r-- |
158 |
base-method-no-change.acl2
|
 |
- |
rw-r--r-- |
2,250 |
base-method-no-change.lisp
|
 |
- |
rw-r--r-- |
162 |
base-method-ptr-no-change.acl2
|
 |
- |
rw-r--r-- |
1,088 |
base-method-ptr-no-change.lisp
|
 |
- |
rw-r--r-- |
166 |
base-next-state-more-specific.acl2
|
 |
- |
rw-r--r-- |
39,856 |
base-next-state-more-specific.lisp
|
 |
- |
rw-r--r-- |
181 |
base-object-field-always-initialized-support.acl2
|
 |
- |
rw-r--r-- |
13,615 |
base-object-field-always-initialized-support.lisp
|
 |
- |
rw-r--r-- |
173 |
base-object-field-always-initialized.acl2
|
 |
- |
rw-r--r-- |
1,510 |
base-object-field-always-initialized.lisp
|
 |
- |
rw-r--r-- |
198 |
base-reference-type-s-good-java-type.acl2
|
 |
- |
rw-r--r-- |
2,024 |
base-reference-type-s-good-java-type.lisp
|
 |
- |
rw-r--r-- |
153 |
base-skip-proofs.acl2
|
 |
- |
rw-r--r-- |
2,657 |
base-skip-proofs.lisp
|
 |
- |
rw-r--r-- |
154 |
base-skip-proofs2.acl2
|
 |
- |
rw-r--r-- |
540 |
base-skip-proofs2.lisp
|
 |
- |
rw-r--r-- |
176 |
base-state-equiv.acl2
|
 |
- |
rw-r--r-- |
68,468 |
base-state-equiv.lisp
|
 |
- |
rw-r--r-- |
160 |
base-state-set-local-at.acl2
|
 |
- |
rw-r--r-- |
34,761 |
base-state-set-local-at.lisp
|
 |
- |
rw-r--r-- |
170 |
base-type-size-normalize-fix-type.acl2
|
 |
- |
rw-r--r-- |
7,378 |
base-type-size-normalize-fix-type.lisp
|
 |
- |
rw-r--r-- |
154 |
base-update-array.acl2
|
 |
- |
rw-r--r-- |
4,333 |
base-update-array.lisp
|
 |
- |
rw-r--r-- |
153 |
base-update-heap.acl2
|
 |
- |
rw-r--r-- |
8,494 |
base-update-heap.lisp
|
 |
- |
rw-r--r-- |
164 |
base-update-trace-normalize.acl2
|
 |
- |
rw-r--r-- |
877 |
base-update-trace-normalize.lisp
|
 |
- |
rw-r--r-- |
190 |
base-valid-object-type-assignable-to-java-lang-Object.acl2
|
 |
- |
rw-r--r-- |
1,175 |
base-valid-object-type-assignable-to-java-lang-Object.lisp
|
 |
- |
rw-r--r-- |
154 |
base-valid-type-s.acl2
|
 |
- |
rw-r--r-- |
3,612 |
base-valid-type-s.lisp
|
 |
- |
rw-r--r-- |
194 |
base-value-sig-no-change-after-class-table-heap-extension.acl2
|
 |
- |
rw-r--r-- |
15,004 |
base-value-sig-no-change-after-class-table-heap-extension.lisp
|
 |
- |
rw-r--r-- |
141 |
base.acl2
|
 |
- |
rw-r--r-- |
16,941 |
base.lisp
|
 |
- |
rw-r--r-- |
164 |
inst.acl2
|
 |
- |
rw-r--r-- |
328 |
inst.lisp
|