File: jvm-exceptions-guard-verification.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 (47 lines) | stat: -rw-r--r-- 1,403 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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
(in-package "JVM")
(include-book "../M6-DJVM-shared/jvm-exceptions")
(include-book "../M6-DJVM-shared/jvm-thread-primitives-guard-verification")
(include-book "../M6-DJVM-shared/jvm-object-type-hierachy-guard-verification")
(include-book "../M6-DJVM-shared/jvm-monitor-primitives-guard-verification")
(include-book "../M6-DJVM-shared/jvm-frame-manipulation-primitives-guard-verification")
(include-book "../M6-DJVM-shared/jvm-linker-guard-verification")
;;; similarly in jvm-thread-primitives-guard-verification.lisp
;; CHEAT!!
(skip-proofs (verify-guards JavaString-to-ACL2-str))
(skip-proofs (verify-guards throw-exception2))
(skip-proofs (verify-guards find-handler))
(skip-proofs (verify-guards getExceptionMessage))
(skip-proofs (verify-guards monitorExit))
(skip-proofs (verify-guards call-stack-depth))
(skip-proofs (verify-guards locked-stage))
(skip-proofs (verify-guards exception-measure))
(skip-proofs (verify-guards invariant-exception-handling-1))
(skip-proofs (verify-guards invariant-exception-handling-2))
(skip-proofs (verify-guards release-lock-invariant))
(skip-proofs (verify-guards release-lock-on-sync-obj))
(skip-proofs (verify-guards throw-exception1))
(skip-proofs (verify-guards throw-exception))
(skip-proofs (verify-guards raise-exception1))
(skip-proofs (verify-guards raise-exception))


;;; Thu Apr  8 21:39:53 2004. Note these operations has a guard