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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
|
; Java Library
;
; Copyright (C) 2022 Kestrel Institute (http://www.kestrel.edu)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (coglio@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "std/portcullis" :dir :system)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defpkg "JAVA" (append (set-difference-eq *std-pkg-symbols*
'(package-name
pointers
values))
'(*nil*
*pkg-witness-name*
*primitive-formals-and-guards*
*stobjs-out-invalid*
add-const-to-untranslate-preprocess
add-suffix
all-ffn-symbs
all-fnnames
all-fnnames-lst
all-fnnames1
all-free/bound-vars
all-vars-open
all-vars-open-lst
alpha/digit-chars
alpha/digit/dash-charlist-p
alpha/digit/uscore/dollar-charlist-p
alpha/uscore/dollar-char-p
arity+
bad-atom<=
body
bool
char-downcase
char-upcase
chars=>nats
check-if-call
check-lambda-call
check-list-call
check-mv-let-call
check-unary-lambda-call
conjoin
cons-listp
cons-pos-alistp
define-sk
defmacro+
defthm-commutative
deftutorial
defxdoc+
doublets-to-alist
dumb-occur-var-open
dumb-occur-var-open-lst
ensure-doublet-list$
ensure-function-name-list$
ensure-list-functions$
ensure-list-has-no-duplicates$
ensure-string-or-nil$
ensure-term-ground$
ensure-value-is-boolean$
ensure-value-is-function-name$
ensure-value-is-in-list$
ensure-value-is-string$
ensure-value-is-untranslated-term$
er-soft+
explode
fargn
fargs
fcons-term
fcons-term*
ffn-symb
ffn-symb-p
flambda-applicationp
flambdap
flatten
fmt-hard-right-margin
fmt-soft-right-margin
formals
formals+
fquotep
function-namep
function-name-listp
implicate
implode
impossible
index-of
integers-from-to
irecursivep
keyword-listp
known-packages+
lambda-body
lambda-formals
logext
loghead
logic-fns-with-raw-code
logicp
lower-case-p
make-lambda
make-mv-let-call
maybe-natp
maybe-string
maybe-stringp
msg-listp
mvify
nat
nats=>string
no-stobjs-p
number-of-results+
organize-symbols-by-name
organize-symbols-by-pkg
packn
packn-pos
partition-rest-and-keyword-args
patbind-fun
patbind-run-unless
patbind-run-when
pos
pos-listp
primitivep
printable-charlist-p
program-fns-with-raw-code
pseudo-fn-args-p
pseudo-fn-p
pseudo-lambda
pseudo-lambda->body
pseudo-lambda->formals
pseudo-lambda-p
pseudo-lambdap
pseudo-term-call
pseudo-term-call->args
pseudo-term-call->fn
pseudo-term-case
pseudo-term-count
pseudo-term-equiv
pseudo-term-fix
pseudo-term-fncall
pseudo-term-fncall->args
pseudo-term-fncall->fn
pseudo-term-kind
pseudo-term-lambda
pseudo-term-lambda->args
pseudo-term-lambda->body
pseudo-term-lambda->formals
pseudo-term-list-count
pseudo-term-null
pseudo-term-quote
pseudo-term-quote->val
pseudo-term-var
pseudo-term-var->name
pseudo-termfn-listp
pseudo-termfnp
pseudo-var-p
pure-raw-p
quote-listp
rawp
remove-assocs-eq
remove-dead-if-branches
remove-mbe-exec
remove-mbe-logic
remove-progn
remove-trivial-vars
remove-unused-vars
sbyte8
sbyte8p
sbyte8-listp
sbyte16
sbyte16p
sbyte16-listp
sbyte32
sbyte32p
sbyte32-listp
sbyte64
sbyte64p
sbyte64-listp
sort-symbol-listp
str-fix
string-downcase
string-string-alistp
string-symbollist-alistp
string-upcase
subcor-var
string=>nats
symbol-list
symbol-name-lst
symbol-pos-alistp
symbol-string-alistp
symbol-symbol-alistp
symbol-symbollist-alistp
symbol-package-name-lst
table-alist+
tail-recursive-p
term-possible-numbers-of-results
trans-eval
tuplep
typed-tuplep
ubody
ubody+
ubyte8
ubyte16
ubyte16p
ubyte16-listp
ubyte8=>hexchars
ubyte8s=>hexstring
uguard
unnormalized-body
unquote-term
unquote-term-list
unsigned-byte-listp
upper-case-p
variablep
std::defret-mutual
std::tuple
set::list-in
str::chars-in-charset-p
str::nat-to-dec-string
str::string-list
str::string-list-fix)))
|
