File: djvm-thread.lisp

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
file content (29 lines) | stat: -rw-r--r-- 1,066 bytes parent folder | download | duplicates (2) 
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
 
(in-package "DJVM")
(include-book "../M6-DJVM-shared/jvm-thread")


;;; Mon Mar 29 20:57:27 2004
;;; The following is used by DJVM so need to be guard verified. 
(acl2::set-verify-guards-eagerness 2)

;; (defun method-stackMap (Method)
;;   (declare (xargs :guard (and (wff-method-decl method)
;;                               (wff-code (method-code method)))))
;;   (code-stackmaps (method-code method)))

;; (defun method-maxStack (Method)
;;   (declare (xargs :guard (and (wff-method-decl method)
;;                               (wff-code (method-code method)))))
;;    (code-max-Stack (method-code method)))

;; (defun method-maxLocals (Method)
;;   (declare (xargs :guard (and (wff-method-decl method)
;;                               (wff-code (method-code method)))))
;;    (code-max-local (method-code method)))

;; (defun method-handlers (Method)
;;   (declare (xargs :guard (and (wff-method-decl method)
;;                               (wff-code (method-code method)))))
;;    (code-handlers (method-code method)))

(acl2::set-verify-guards-eagerness 0)