package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17

Folder: small

d .. (parent)
d d rwxr-xr-x 4,096 .sys
- - rw-r--r-- 346 HALT.lisp
- - rw-r--r-- 46 IFEQ.acl2
- - rw-r--r-- 5,604 IFEQ.lisp
- - rw-r--r-- 48 INVOKE.acl2
- - rw-r--r-- 2,556 INVOKE.lisp
- - rw-r--r-- 2,436 POP.lisp
- - rw-r--r-- 46 PUSH.acl2
- - rw-r--r-- 2,449 PUSH.lisp
- - rw-r--r-- 48 RETURN.acl2
- - rw-r--r-- 2,386 RETURN.lisp
- - rw-r--r-- 108 bcv-check-pre-implies-bcv-simple-check-pre-if-all-method-verified.acl2
- - rw-r--r-- 790 bcv-check-pre-implies-bcv-simple-check-pre-if-all-method-verified.lisp
- - rw-r--r-- 82 bcv-find-correct-witness-all-next-state.acl2
- - rw-r--r-- 32,091 bcv-find-correct-witness-all-next-state.lisp
- - rw-r--r-- 81 bcv-find-correct-witness-bcv-check-pre.acl2
- - rw-r--r-- 7,096 bcv-find-correct-witness-bcv-check-pre.lisp
- - rw-r--r-- 81 bcv-find-correct-witness-sig-vector-1.acl2
- - rw-r--r-- 8,563 bcv-find-correct-witness-sig-vector-1.lisp
- - rw-r--r-- 78 bcv-find-correct-witness-sig-vector.acl2
- - rw-r--r-- 12,845 bcv-find-correct-witness-sig-vector.lisp
- - rw-r--r-- 67 bcv-find-correct-witness.acl2
- - rw-r--r-- 7,736 bcv-find-correct-witness.lisp
- - rw-r--r-- 3,767 bcv-if-pc-small-then-not-bound-in-witness.lisp
- - rw-r--r-- 6,895 bcv-if-verified-then-pc-ordered.lisp
- - rw-r--r-- 58 bcv-is-effective.acl2
- - rw-r--r-- 16,927 bcv-is-effective.lisp
- - rw-r--r-- 2,027 bcv-make-inst.lisp
- - rw-r--r-- 61 bcv-method-properties.acl2
- - rw-r--r-- 13,378 bcv-method-properties.lisp
- - rw-r--r-- 21,936 bcv-model.lisp
- - rw-r--r-- 8,080 bcv-partial-signature-vector-full-signature-vector.lisp
- - rw-r--r-- 78 bcv-simple-check-implies-djvm-check.acl2
- - rw-r--r-- 4,269 bcv-simple-check-implies-djvm-check.lisp
- - rw-r--r-- 66 bcv-simple-check-monotonic.acl2
- - rw-r--r-- 279 bcv-simple-check-monotonic.lisp
- - rw-r--r-- 92 bcv-simple-execute-produce-compatible-next-states.acl2
- - rw-r--r-- 26,554 bcv-simple-execute-produce-compatible-next-states.lisp
- - rw-r--r-- 93 bcv-simple-method-implies-bcv-simple-check-step-pre.acl2
- - rw-r--r-- 1,402 bcv-simple-method-implies-bcv-simple-check-step-pre.lisp
- - rw-r--r-- 5,519 bcv-simple-method-properties.lisp
- - rw-r--r-- 9,719 bcv-simple-model.lisp
- - rw-r--r-- 80 bcv-succeed-implies-bcv-simple-succeed.acl2
- - rw-r--r-- 26,319 bcv-succeed-implies-bcv-simple-succeed.lisp
- - rw-r--r-- 7,787 bcv-verified-implies-method-name-method-table-fixed.lisp
- - rw-r--r-- 70 consistent-state-properties.acl2
- - rw-r--r-- 27,170 consistent-state-properties.lisp
- - rw-r--r-- 63 consistent-state-step.acl2
- - rw-r--r-- 3,204 consistent-state-step.lisp
- - rw-r--r-- 5,850 consistent-state.lisp
- - rw-r--r-- 399 djvm-HALT.lisp
- - rw-r--r-- 28,441 djvm-IFEQ.lisp
- - rw-r--r-- 41,753 djvm-INVOKE.lisp
- - rw-r--r-- 17,409 djvm-POP.lisp
- - rw-r--r-- 17,615 djvm-PUSH.lisp
- - rw-r--r-- 13,967 djvm-RETURN.lisp
- - rw-r--r-- 84 djvm-check-succeed-implies-jvm-equiv-state.acl2
- - rw-r--r-- 7,337 djvm-check-succeed-implies-jvm-equiv-state.lisp
- - rw-r--r-- 54 djvm-is-safe.acl2
- - rw-r--r-- 5,942 djvm-is-safe.lisp
- - rw-r--r-- 7,087 djvm-model.lisp
- - rw-r--r-- 3,730 generic.lisp
- - rw-r--r-- 6,284 jvm-model.lisp
- - rw-r--r-- 2,392 state-equiv-def.lisp