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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
(DJVM::CONSISTENT-STATE-BCV-ON-TRACK-IMPLIES-BCV-GOOD-SCL-STRONG)
(DJVM::CONSISTENT-STATE-BCV-ON-TRACK-IMPLIES-GOOD-ICL)
(DJVM::CONSISTENT-STATE-BCV-ON-TRACK-IMPLIES-ICL-SCL-COMPATIBLE
(54 1 (:DEFINITION BCV::SCL-JVM2BCV))
(50 1 (:DEFINITION BCV::MAKE-CLASS-DEF))
(30 1 (:DEFINITION BCV::MERGESTACKMAPANDCODE))
(29 23 (:REWRITE DEFAULT-CDR))
(27 9 (:DEFINITION NTH))
(22 22 (:REWRITE DJVM::CONSISTENT-VALUE-X-TAG-IMLPLIES-NOT-CONSP))
(13 11 (:REWRITE DEFAULT-CAR))
(11 2 (:DEFINITION BCV::ACCESSFLAGS-S))
(9 1 (:DEFINITION BCV::MAKESTACKMAP))
(8 1 (:REWRITE JVM::TRUE-LISTP-LEN-1-IS-LIST-CAR))
(6 1 (:DEFINITION BCV::METHODS-S))
(6 1 (:DEFINITION BCV::INTERFACES-S))
(6 1 (:DEFINITION BCV::FIELDS-S))
(6 1 (:DEFINITION BCV::CONSTANTPOOL-S))
(5 5 (:TYPE-PRESCRIPTION TRUE-LISTP))
(5 1 (:DEFINITION TRUE-LISTP))
(5 1 (:DEFINITION MEM))
(5 1 (:DEFINITION JVM::CLASS-BY-NAME))
(4 1 (:DEFINITION BCV::SUPER-S))
(4 1 (:DEFINITION BCV::CLASSNAME-S))
(3 1 (:DEFINITION BCV::MAPOFFSET))
(3 1 (:DEFINITION BCV::INSTROFFSET))
(2 2 (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP))
(2 2 (:REWRITE MEM-SUBSET))
(2 1 (:REWRITE DEFAULT-<-2))
(2 1 (:REWRITE DEFAULT-<-1))
)
(DJVM::SIG-FRAME-MORE-GENERAL-NOT-NULL-NOT-NULL-SPECIFIC)
(DJVM::INSTRUCTIONISTYPESAFE-AND-IS-INST-AALOAD-CHECK-AALOAD
(528 528 (:TYPE-PRESCRIPTION BCV::PUSHOPERANDSTACK))
(66 66 (:TYPE-PRESCRIPTION BCV::TRANSLATE-TYPE))
(11 11 (:TYPE-PRESCRIPTION BCV::INSTRUCTIONHASEQUIVALENTTYPERULE))
(2 1 (:REWRITE DEFAULT-CAR))
(1 1 (:REWRITE DJVM::SIG-CHECK-AALOAD-ON-MORE-GENERAL-IMPLIES-MORE-SPECIFIC))
(1 1 (:REWRITE DJVM::CONSISTENT-VALUE-X-TAG-IMLPLIES-NOT-CONSP))
)
(DJVM::ON-TRACK-WITH-BCV-IMPLIES-STEP-AALOAD
(240 240 (:TYPE-PRESCRIPTION JVM::LOADER-INV))
(160 80 (:TYPE-PRESCRIPTION JVM::LOADER-INV-IMPLIES-WFF-STATE))
(160 80 (:TYPE-PRESCRIPTION JVM::LOADER-INV-IMPLIES-WFF-INSTANCE-CLASS-TABLE))
(160 80 (:TYPE-PRESCRIPTION JVM::LOADER-INV-IMPLIES-WFF-CLASS-TABLE))
(46 1 (:DEFINITION BCV::STACK-MAP-WRAP))
(40 1 (:DEFINITION BCV::MAKESTACKMAP))
(39 1 (:REWRITE JVM::TRUE-LISTP-LEN-1-IS-LIST-CAR))
(24 4 (:REWRITE DJVM::NOT-VALUE-OF-V-IMPLIES-NOT-NULLP))
(20 4 (:REWRITE DJVM::NULLP-IMPLIED-BY))
(20 4 (:REWRITE DJVM::CHECK-NULL-NOT-EQUAL-VALUE-OF-MINUS-1))
(20 4 (:DEFINITION LEN))
(16 2 (:REWRITE DJVM::CHECK-NULL-IMPLIES-VALUE-BEING-NEGATIVE-1))
(16 2 (:LINEAR DJVM::CONSP-IMPLIES-LEN))
(13 13 (:TYPE-PRESCRIPTION LEN))
(12 4 (:REWRITE DJVM::NOT-NULLP-TAG-REF-NOT-EQUAL-MINUS-1))
(8 8 (:TYPE-PRESCRIPTION DJVM::WFF-REFP))
(8 4 (:REWRITE DEFAULT-+-2))
(8 2 (:REWRITE DJVM::WFF-REFP-IMPLIES-TAG-OF-EQUAL-REF))
(8 2 (:REWRITE DJVM::WFF-REFP-IMPLIES-TAG-OF-BEING-REF))
(8 1 (:LINEAR DJVM::CONSP-LEN-NO-LESS-THAN-0))
(5 5 (:REWRITE DEFAULT-CDR))
(4 4 (:TYPE-PRESCRIPTION DJVM::CHECK-NULL))
(4 4 (:REWRITE DEL-SET-LEN))
(4 4 (:REWRITE DEFAULT-+-1))
(4 4 (:REWRITE DJVM::CONSISTENT-VALUE-X-AND-TAG-REF-IMPLIES-WFF-REFP-B))
(4 1 (:DEFINITION JVM::RAISE-EXCEPTION))
(3 2 (:REWRITE DEFAULT-CAR))
(2 2 (:TYPE-PRESCRIPTION DJVM::STACK-MAPS-WITNESS))
(2 2 (:REWRITE DJVM::CONSISTENT-VALUE-X-TAG-IMLPLIES-NOT-CONSP))
(2 2 (:REWRITE DJVM::CONSISTENT-STATE-STRONG-IMPLIED-BY-B))
(2 2 (:LINEAR SUBSET-NODUP-SET-SIZE))
(1 1 (:TYPE-PRESCRIPTION JVM::NO-FATAL-ERROR?))
(1 1 (:REWRITE JVM::NO-FATAL-ERROR?-NO-FATAL-ERROR?))
(1 1 (:DEFINITION JVM::ALERTUSER))
)
|
