 |
|
|
|
.. (parent) |
 |
d |
rwxr-xr-x |
4,096 |
.sys
|
 |
- |
rw-r--r-- |
622 |
Makefile
|
 |
- |
rw-r--r-- |
140 |
bcv-base.acl2
|
 |
- |
rw-r--r-- |
15,210 |
bcv-base.lisp
|
 |
- |
rw-r--r-- |
165 |
bcv-collect-sig-frame-vector-misc.acl2
|
 |
- |
rw-r--r-- |
4,048 |
bcv-collect-sig-frame-vector-misc.lisp
|
 |
- |
rw-r--r-- |
176 |
bcv-collect-sig-frame-vector-never-aftergoto.acl2
|
 |
- |
rw-r--r-- |
3,021 |
bcv-collect-sig-frame-vector-never-aftergoto.lisp
|
 |
- |
rw-r--r-- |
168 |
bcv-collected-frames-are-good-frames.acl2
|
 |
- |
rw-r--r-- |
12,155 |
bcv-collected-frames-are-good-frames.lisp
|
 |
- |
rw-r--r-- |
173 |
bcv-collected-frames-are-strictly-ordered.acl2
|
 |
- |
rw-r--r-- |
13,664 |
bcv-collected-frames-are-strictly-ordered.lisp
|
 |
- |
rw-r--r-- |
188 |
bcv-functions-basic-verify-guard.acl2
|
 |
- |
rw-r--r-- |
1,360 |
bcv-functions-basic-verify-guard.lisp
|
 |
- |
rw-r--r-- |
175 |
bcv-functions-basic.acl2
|
 |
- |
rw-r--r-- |
2,509 |
bcv-functions-basic.lisp
|
 |
- |
rw-r--r-- |
169 |
bcv-functions.acl2
|
 |
- |
rw-r--r-- |
5,977 |
bcv-functions.lisp
|
 |
- |
rw-r--r-- |
156 |
bcv-good-env-encapsulate.acl2
|
 |
- |
rw-r--r-- |
1,940 |
bcv-good-env-encapsulate.lisp
|
 |
- |
rw-r--r-- |
169 |
bcv-instructionIsTypeSafe-if-verified.acl2
|
 |
- |
rw-r--r-- |
1,825 |
bcv-instructionIsTypeSafe-if-verified.lisp
|
 |
- |
rw-r--r-- |
151 |
bcv-is-suffix-facts.acl2
|
 |
- |
rw-r--r-- |
6,201 |
bcv-is-suffix-facts.lisp
|
 |
- |
rw-r--r-- |
184 |
bcv-isAssignable-transitive.acl2
|
 |
- |
rw-r--r-- |
47,497 |
bcv-isAssignable-transitive.lisp
|
 |
- |
rw-r--r-- |
156 |
bcv-mergedcodeIsTypesafe.acl2
|
 |
- |
rw-r--r-- |
14,983 |
bcv-mergedcodeIsTypesafe.lisp
|
 |
- |
rw-r--r-- |
148 |
bcv-next-inst-is.acl2
|
 |
- |
rw-r--r-- |
4,776 |
bcv-next-inst-is.lisp
|
 |
- |
rw-r--r-- |
171 |
bcv-next-stackframe-equal-suffix-suffix.acl2
|
 |
- |
rw-r--r-- |
15,780 |
bcv-next-stackframe-equal-suffix-suffix.lisp
|
 |
- |
rw-r--r-- |
154 |
bcv-pc-wff-mergedcode1.acl2
|
 |
- |
rw-r--r-- |
1,254 |
bcv-pc-wff-mergedcode1.lisp
|
 |
- |
rw-r--r-- |
172 |
bcv-searchStackFrame-only-suffix-matters.acl2
|
 |
- |
rw-r--r-- |
4,628 |
bcv-searchStackFrame-only-suffix-matters.lisp
|
 |
- |
rw-r--r-- |
169 |
bcv-searchStackFrame-reduce-support-2.acl2
|
 |
- |
rw-r--r-- |
11,281 |
bcv-searchStackFrame-reduce-support-2.lisp
|
 |
- |
rw-r--r-- |
167 |
bcv-searchStackFrame-reduce-support.acl2
|
 |
- |
rw-r--r-- |
26,539 |
bcv-searchStackFrame-reduce-support.lisp
|
 |
- |
rw-r--r-- |
159 |
bcv-searchStackFrame-reduce.acl2
|
 |
- |
rw-r--r-- |
3,766 |
bcv-searchStackFrame-reduce.lisp
|
 |
- |
rw-r--r-- |
172 |
bcv-sig-do-produce-compatible-next-state.acl2
|
 |
- |
rw-r--r-- |
17,056 |
bcv-sig-do-produce-compatible-next-state.lisp
|
 |
- |
rw-r--r-- |
170 |
bcv-succeed-implies-bcv-simple-succeed.acl2
|
 |
- |
rw-r--r-- |
28,621 |
bcv-succeed-implies-bcv-simple-succeed.lisp
|
 |
- |
rw-r--r-- |
144 |
bcv-wff-code.acl2
|
 |
- |
rw-r--r-- |
6,493 |
bcv-wff-code.lisp
|
 |
- |
rw-r--r-- |
889 |
bcv.pkg
|
 |
- |
rw-r--r-- |
179 |
bcv.pkg.lisp
|
 |
- |
rw-r--r-- |
161 |
good-scl-strong-encapsulate.acl2
|
 |
- |
rw-r--r-- |
3,903 |
good-scl-strong-encapsulate.lisp
|
 |
- |
rw-r--r-- |
149 |
typechecker-ext.acl2
|
 |
- |
rw-r--r-- |
5,654 |
typechecker-ext.lisp
|
 |
- |
rw-r--r-- |
59 |
typechecker-simple.acl2
|
 |
- |
rw-r--r-- |
7,791 |
typechecker-simple.lisp
|
 |
- |
rw-r--r-- |
53 |
typechecker.acl2
|
 |
- |
rw-r--r-- |
164,194 |
typechecker.lisp
|