001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.ast;
004
005 import javafe.ast.Identifier;
006 import javafe.util.Assert;
007
008 import escjava.prover.Atom;
009
010 public class TagConstants extends GeneratedTags
011 //javafe.tc.TagConstants
012 //implements GeneratedTags
013 {
014 //// Tags for new binary operators
015 public static final int IMPLIES = escjava.ast.GeneratedTags.LAST_TAG + 1;
016 public static final int EXPLIES = IMPLIES + 1;
017 public static final int IFF = EXPLIES + 1; // equivalence (equality)
018 public static final int NIFF = IFF + 1; // discrepance (xor)
019 public static final int SUBTYPE = NIFF + 1;
020 public static final int DOTDOT = SUBTYPE + 1;
021
022 //// Tags for pragma punctuation
023 public static final int LEFTARROW = DOTDOT + 1; // <-
024 public static final int RIGHTARROW = LEFTARROW + 1; // ->
025 public static final int OPENPRAGMA = RIGHTARROW + 1; // {|
026 public static final int CLOSEPRAGMA = OPENPRAGMA + 1; // |}
027
028 //// Tags for new literal expressions
029 public static final int SYMBOLLIT = CLOSEPRAGMA + 1;
030
031 //// Tags for new primitive types
032 public static final int ANY = SYMBOLLIT + 1;
033 public static final int TYPECODE = ANY + 1;
034 public static final int BIGINTTYPE = TYPECODE + 1;
035 public static final int REALTYPE = BIGINTTYPE + 1;
036 public static final int LOCKSET = REALTYPE + 1;
037 public static final int OBJECTSET = LOCKSET + 1;
038
039 //// Tags for guarded commands
040 public static final int ASSERTCMD = OBJECTSET + 1;
041 public static final int ASSUMECMD = ASSERTCMD + 1;
042 public static final int CHOOSECMD = ASSUMECMD + 1;
043 public static final int RAISECMD = CHOOSECMD + 1;
044 public static final int SKIPCMD = RAISECMD + 1;
045 public static final int TRYCMD = SKIPCMD + 1;
046
047 //// Tags for special tokens
048 public static final int INFORMALPRED_TOKEN = TRYCMD + 1;
049
050 //// Tags for ESC/Java checks
051 public static final int FIRSTESCCHECKTAG = INFORMALPRED_TOKEN + 1;
052 public static final int CHKARITHMETIC = FIRSTESCCHECKTAG;
053 public static final int CHKARRAYSTORE = CHKARITHMETIC + 1;
054 public static final int CHKASSERT = CHKARRAYSTORE + 1;
055 public static final int CHKCLASSCAST = CHKASSERT + 1;
056 public static final int CHKCODEREACHABILITY = CHKCLASSCAST + 1;
057 public static final int CHKCONSISTENT = CHKCODEREACHABILITY + 1;
058 public static final int CHKCONSTRAINT = CHKCONSISTENT + 1;
059 public static final int CHKCONSTRUCTORLEAK = CHKCONSTRAINT + 1;
060 public static final int CHKDECREASES_BOUND = CHKCONSTRUCTORLEAK + 1;
061 public static final int CHKDECREASES_DECR = CHKDECREASES_BOUND + 1;
062 public static final int CHKDEFINEDNESS = CHKDECREASES_DECR + 1;
063 public static final int CHKEXPRDEFINEDNESS = CHKDEFINEDNESS + 1;
064 public static final int CHKINDEXNEGATIVE = CHKEXPRDEFINEDNESS + 1;
065 public static final int CHKINDEXTOOBIG = CHKINDEXNEGATIVE + 1;
066 public static final int CHKINITIALIZATION = CHKINDEXTOOBIG + 1;
067 public static final int CHKINITIALIZERLEAK = CHKINITIALIZATION + 1;
068 public static final int CHKINITIALLY = CHKINITIALIZERLEAK + 1;
069 public static final int CHKLOCKINGORDER = CHKINITIALLY + 1;
070 public static final int CHKLOOPINVARIANT = CHKLOCKINGORDER + 1;
071 public static final int CHKLOOPOBJECTINVARIANT = CHKLOOPINVARIANT + 1;
072 public static final int CHKMODIFIESEXTENSION = CHKLOOPOBJECTINVARIANT + 1;
073 public static final int CHKMODIFIES = CHKMODIFIESEXTENSION + 1;
074 public static final int CHKNEGATIVEARRAYSIZE = CHKMODIFIES + 1;
075 public static final int CHKNONNULL = CHKNEGATIVEARRAYSIZE + 1;
076 public static final int CHKNONNULLINIT = CHKNONNULL + 1;
077 public static final int CHKNONNULLRESULT = CHKNONNULLINIT + 1;
078 public static final int CHKNULLPOINTER = CHKNONNULLRESULT + 1;
079 public static final int CHKOBJECTINVARIANT = CHKNULLPOINTER + 1;
080 public static final int CHKOWNERNULL = CHKOBJECTINVARIANT + 1;
081 public static final int CHKPOSTCONDITION = CHKOWNERNULL + 1;
082 public static final int CHKPRECONDITION = CHKPOSTCONDITION + 1;
083 public static final int CHKSHARING = CHKPRECONDITION + 1;
084 public static final int CHKSHARINGALLNULL = CHKSHARING + 1;
085 public static final int CHKUNENFORCEBLEOBJECTINVARIANT = CHKSHARINGALLNULL + 1;
086 public static final int CHKUNEXPECTEDEXCEPTION = CHKUNENFORCEBLEOBJECTINVARIANT + 1;
087 public static final int CHKUNEXPECTEDEXCEPTION2 = CHKUNEXPECTEDEXCEPTION + 1;
088 public static final int CHKWRITABLEDEFERRED = CHKUNEXPECTEDEXCEPTION2 + 1;
089 public static final int CHKWRITABLE = CHKWRITABLEDEFERRED + 1;
090 public static final int CHKQUIET = CHKWRITABLE + 1;
091 public static final int CHKASSUME = CHKQUIET + 1;
092 public static final int CHKADDINFO = CHKASSUME + 1;
093 public static final int CHKFREE = CHKADDINFO + 1;
094 public static final int LASTESCCHECKTAG = CHKFREE;
095
096 //// Tags for Nary function symbols that are _not_ ESCJ keywords
097 //
098 // These need to be added both below and in escfunctions in this file,
099 // as well as as switch labels in escjava.ast.EscPrettyPrint and
100 // escjava.translate.VcToString.
101 //
102 public static final int FIRSTFUNCTIONTAG = LASTESCCHECKTAG + 1;
103 public static final int ALLOCLT = FIRSTFUNCTIONTAG;
104 public static final int ALLOCLE = ALLOCLT+1;
105 public static final int ANYEQ = ALLOCLE+1;
106 public static final int ANYNE = ANYEQ+1;
107 public static final int ARRAYLENGTH = ANYNE+1;
108 public static final int ARRAYFRESH = ARRAYLENGTH + 1;
109 public static final int ARRAYMAKE = ARRAYFRESH + 1;
110 public static final int ARRAYSHAPEMORE = ARRAYMAKE + 1;
111 public static final int ARRAYSHAPEONE = ARRAYSHAPEMORE + 1;
112 public static final int ASELEMS = ARRAYSHAPEONE + 1;
113 public static final int ASFIELD = ASELEMS + 1;
114 public static final int ASLOCKSET = ASFIELD + 1;
115 public static final int BOOLAND = ASLOCKSET + 1;
116 public static final int BOOLANDX = BOOLAND + 1;
117 public static final int BOOLEQ = BOOLANDX + 1;
118 public static final int BOOLIMPLIES = BOOLEQ + 1;
119 public static final int BOOLNE = BOOLIMPLIES + 1;
120 public static final int BOOLNOT = BOOLNE + 1;
121 public static final int BOOLOR = BOOLNOT + 1;
122 public static final int CAST = BOOLOR + 1;
123 public static final int CLASSLITERALFUNC = CAST + 1;
124 public static final int CONDITIONAL = CLASSLITERALFUNC + 1;
125 public static final int ECLOSEDTIME = CONDITIONAL + 1;
126 // ELEMSNONNULL -- an ESC keyword
127 // ELEMTYPE -- an ESC keyword
128 public static final int FCLOSEDTIME = ECLOSEDTIME + 1;
129 public static final int FLOATINGADD = FCLOSEDTIME + 1;
130 public static final int FLOATINGDIV = FLOATINGADD + 1;
131 public static final int FLOATINGEQ = FLOATINGDIV + 1;
132 public static final int FLOATINGGE = FLOATINGEQ + 1;
133 public static final int FLOATINGGT = FLOATINGGE + 1;
134 public static final int FLOATINGLE = FLOATINGGT + 1;
135 public static final int FLOATINGLT = FLOATINGLE + 1;
136 public static final int FLOATINGMOD = FLOATINGLT + 1;
137 public static final int FLOATINGMUL = FLOATINGMOD + 1;
138 public static final int FLOATINGNE = FLOATINGMUL + 1;
139 public static final int FLOATINGNEG = FLOATINGNE + 1;
140 public static final int FLOATINGSUB = FLOATINGNEG + 1;
141 public static final int INTEGRALADD = FLOATINGSUB + 1;
142 public static final int INTEGRALAND = INTEGRALADD + 1;
143 public static final int INTEGRALDIV = INTEGRALAND + 1;
144 public static final int INTEGRALEQ = INTEGRALDIV + 1;
145 public static final int INTEGRALGE = INTEGRALEQ + 1;
146 public static final int INTEGRALGT = INTEGRALGE + 1;
147 public static final int INTEGRALLE = INTEGRALGT + 1;
148 public static final int INTEGRALLT = INTEGRALLE + 1;
149 public static final int INTEGRALMOD = INTEGRALLT + 1;
150 public static final int INTEGRALMUL = INTEGRALMOD + 1;
151 public static final int INTEGRALNE = INTEGRALMUL + 1;
152 public static final int INTEGRALNEG = INTEGRALNE + 1;
153 public static final int INTEGRALNOT = INTEGRALNEG + 1;
154 public static final int INTEGRALOR = INTEGRALNOT + 1;
155 public static final int INTSHIFTL = INTEGRALOR + 1;
156 public static final int LONGSHIFTL = INTSHIFTL + 1;
157 public static final int INTSHIFTR = LONGSHIFTL + 1;
158 public static final int LONGSHIFTR = INTSHIFTR + 1;
159 public static final int INTSHIFTRU = LONGSHIFTR + 1;
160 public static final int LONGSHIFTRU = INTSHIFTRU + 1;
161 public static final int INTEGRALSUB = LONGSHIFTRU + 1;
162 public static final int INTEGRALXOR = INTEGRALSUB + 1;
163 public static final int INTERN = INTEGRALXOR + 1;
164 public static final int INTERNED = INTERN + 1;
165 public static final int IS = INTERNED + 1;
166 public static final int ISALLOCATED = IS + 1;
167 public static final int ISNEWARRAY = ISALLOCATED + 1;
168 // MAX -- an ESC keyword
169 public static final int LOCKLE = ISNEWARRAY + 1;
170 public static final int LOCKLT = LOCKLE + 1;
171 public static final int METHODCALL = LOCKLT + 1;
172 public static final int REFEQ = METHODCALL + 1;
173 public static final int REFNE = REFEQ + 1;
174 public static final int SELECT = REFNE + 1;
175 public static final int STORE = SELECT + 1;
176 public static final int STRINGCAT = STORE + 1;
177 public static final int STRINGCATP = STRINGCAT + 1;
178 public static final int TYPEEQ = STRINGCATP + 1;
179 public static final int TYPENE = TYPEEQ + 1;
180 public static final int TYPELE = TYPENE + 1; // a.k.a. "<:"
181 // TYPEOF -- an ESC keyword
182 public static final int UNSET = TYPELE + 1;
183 public static final int VALLOCTIME = UNSET + 1;
184 public static final int LASTFUNCTIONTAG = VALLOCTIME;
185
186 // Constants used in deciding how to translate CHKs
187 public static final int CHK_AS_ASSUME = LASTFUNCTIONTAG + 1;
188 public static final int CHK_AS_ASSERT = CHK_AS_ASSUME + 1;
189 public static final int CHK_AS_SKIP = CHK_AS_ASSERT + 1;
190
191 // FIXME - these should be merged into one order so they are easy to find
192 // Also keywords are looked up by a linear search - that could be improved
193 // upon greatly
194 //// JML keywords
195 public static final int FIRSTJMLKEYWORDTAG = CHK_AS_SKIP + 1;
196
197 public static final int ASSUME = FIRSTJMLKEYWORDTAG;
198 public static final int AXIOM = ASSUME + 1;
199 public static final int CODE_CONTRACT = AXIOM + 1;
200 public static final int DECREASES = CODE_CONTRACT + 1;
201 public static final int DTTFSA = DECREASES + 1;
202 public static final int ENSURES = DTTFSA + 1;
203 public static final int ELEMSNONNULL = ENSURES + 1; // Function
204 public static final int ELEMTYPE = ELEMSNONNULL + 1; // Function
205 public static final int EXISTS = ELEMTYPE + 1;
206 public static final int EXSURES = EXISTS + 1;
207 public static final int FRESH = EXSURES + 1; // Non-GCE function
208 public static final int FORALL = FRESH + 1;
209 public static final int FUNCTION = FORALL + 1;
210 public static final int GHOST = FUNCTION + 1;
211 public static final int HELPER = GHOST + 1;
212 public static final int IMMUTABLE = HELPER + 1;
213 public static final int IN = IMMUTABLE + 1;
214 public static final int IN_REDUNDANTLY = IN + 1;
215 public static final int INTO = IN_REDUNDANTLY + 1;
216 public static final int INVARIANT = INTO + 1;
217 public static final int LBLPOS = INVARIANT + 1;
218 public static final int LBLNEG = LBLPOS + 1;
219 public static final int LOOP_INVARIANT = LBLNEG + 1;
220 public static final int LOOP_PREDICATE = LOOP_INVARIANT + 1;
221 public static final int LS = LOOP_PREDICATE + 1;
222 public static final int MAPS = LS + 1;
223 public static final int MAPS_REDUNDANTLY = MAPS + 1;
224 public static final int MAX = MAPS_REDUNDANTLY + 1; // Function
225 public static final int MODIFIES = MAX + 1;
226 public static final int MONITORED = MODIFIES + 1;
227 public static final int MONITORED_BY = MONITORED + 1;
228 public static final int MONITORS_FOR = MONITORED_BY + 1;
229 public static final int NON_NULL = MONITORS_FOR + 1;
230 public static final int NOWARN = NON_NULL + 1;
231 public static final int PRE = NOWARN + 1;
232 public static final int READABLE = PRE + 1;
233 public static final int READABLE_IF = READABLE + 1;
234 public static final int RES = READABLE_IF + 1;
235 public static final int REQUIRES = RES + 1;
236 public static final int SET = REQUIRES + 1;
237 public static final int SPEC_PUBLIC = SET + 1;
238 public static final int STILL_DEFERRED = SPEC_PUBLIC + 1;
239 public static final int TYPE = STILL_DEFERRED + 1; // "type"
240 public static final int TYPETYPE = TYPE + 1; // "TYPE"; name for TYPECODE
241 public static final int TYPEOF = TYPETYPE + 1; // Function
242 public static final int UNINITIALIZED = TYPEOF + 1;
243 public static final int UNREACHABLE = UNINITIALIZED + 1;
244 public static final int WRITABLE_DEFERRED = UNREACHABLE + 1;
245 public static final int WRITABLE_IF = WRITABLE_DEFERRED+ 1;
246 public static final int WRITABLE = WRITABLE_IF + 1;
247 public static final int SKOLEM_CONSTANT = WRITABLE + 1;
248
249 public static final int BIGINT = SKOLEM_CONSTANT + 1;
250 public static final int WACK_DURATION = BIGINT + 1;
251 // \elemtype -- an ESC keyword
252 public static final int EVERYTHING = WACK_DURATION + 1;
253 // \exists -- an ESC keyword
254 public static final int FIELDS_OF = EVERYTHING + 1;
255 // \forall -- an ESC keyword
256 // \fresh -- an ESC keyword
257 public static final int INVARIANT_FOR = FIELDS_OF + 1;
258 public static final int IS_INITIALIZED = INVARIANT_FOR + 1;
259 // \lblneg -- an ESC keyword
260 // \lblpos -- an ESC keyword
261 // \lockset -- an ESC keyword
262 // \max -- an ESC keyword
263 public static final int MAXQUANT = IS_INITIALIZED + 1;
264 public static final int MIN = MAXQUANT + 1;
265 // \nonnullelements -- an ESC keyword
266 public static final int NOTHING = MIN + 1;
267 public static final int NOT_MODIFIED = NOTHING + 1;
268 public static final int NOT_SPECIFIED = NOT_MODIFIED + 1;
269 public static final int WACK_NOWARN = NOT_SPECIFIED + 1;
270 public static final int NOWARN_OP = WACK_NOWARN + 1;
271 public static final int NUM_OF = NOWARN_OP + 1;
272 // \old -- an ESC keyword
273 public static final int OTHER = NUM_OF + 1;
274 public static final int PRIVATE_DATA = OTHER + 1;
275 public static final int PRODUCT = PRIVATE_DATA + 1;
276 public static final int REACH = PRODUCT + 1;
277 public static final int REAL = REACH + 1;
278 // \result -- an ESC keyword
279 public static final int SPACE = REAL + 1;
280 public static final int SUCH_THAT = SPACE + 1;
281 public static final int SUM = SUCH_THAT + 1;
282 // \type -- an ESC keyword
283 // \typeof -- an ESC keyword
284 // \TYPE -- an ESC keyword
285 public static final int WARN = SUM + 1;
286 public static final int WARN_OP = WARN + 1;
287 public static final int WACK_WORKING_SPACE = WARN_OP + 1;
288
289 public static final int ABRUPT_BEHAVIOR = WACK_WORKING_SPACE + 1;
290 public static final int ACCESSIBLE_REDUNDANTLY = ABRUPT_BEHAVIOR + 1;
291 public static final int ACCESSIBLE = ACCESSIBLE_REDUNDANTLY + 1;
292 public static final int ALSO = ACCESSIBLE + 1;
293 public static final int ALSO_REFINE = ALSO + 1; // Internal use only
294 public static final int ASSERT_REDUNDANTLY = ALSO_REFINE + 1;
295 public static final int ASSIGNABLE_REDUNDANTLY = ASSERT_REDUNDANTLY + 1;
296 public static final int ASSIGNABLE = ASSIGNABLE_REDUNDANTLY + 1;
297 public static final int ASSUME_REDUNDANTLY = ASSIGNABLE + 1;
298 // assume -- an ESC keyword
299 // axiom -- an ESC keyword
300 public static final int BEHAVIOR = ASSUME_REDUNDANTLY + 1;
301 public static final int BREAKS_REDUNDANTLY = BEHAVIOR + 1;
302 public static final int BREAKS = BREAKS_REDUNDANTLY + 1;
303 public static final int CALLABLE_REDUNDANTLY = BREAKS + 1;
304 public static final int CALLABLE = CALLABLE_REDUNDANTLY + 1;
305 public static final int CHOOSE_IF = CALLABLE + 1;
306 public static final int CHOOSE = CHOOSE_IF + 1;
307 public static final int CONSTRAINT_REDUNDANTLY = CHOOSE + 1;
308 public static final int CONSTRAINT = CONSTRAINT_REDUNDANTLY + 1;
309 public static final int CONSTRUCTOR = CONSTRAINT + 1;
310 public static final int CONTINUES_REDUNDANTLY = CONSTRUCTOR + 1;
311 public static final int CONTINUES = CONTINUES_REDUNDANTLY + 1; // @review
312 public static final int DECREASES_REDUNDANTLY = CONTINUES + 1;
313 // decreases -- an ESC keyword
314 public static final int DECREASING_REDUNDANTLY = DECREASES_REDUNDANTLY + 1;
315 public static final int DECREASING = DECREASING_REDUNDANTLY + 1;
316 public static final int DEPENDS_REDUNDANTLY = DECREASING + 1;
317 public static final int DEPENDS = DEPENDS_REDUNDANTLY + 1;
318 public static final int DIVERGES_REDUNDANTLY = DEPENDS + 1;
319 public static final int DIVERGES = DIVERGES_REDUNDANTLY + 1;
320 public static final int DURATION_REDUNDANTLY = DIVERGES + 1;
321 public static final int DURATION = DURATION_REDUNDANTLY + 1;
322 public static final int END = DURATION + 1; // Internal use only
323 public static final int ENSURES_REDUNDANTLY = END + 1;
324 // ensures -- an ESC keyword
325 public static final int EXAMPLE = ENSURES_REDUNDANTLY + 1;
326 public static final int EXCEPTIONAL_BEHAVIOR = EXAMPLE + 1;
327 public static final int EXCEPTIONAL_EXAMPLE = EXCEPTIONAL_BEHAVIOR + 1;
328 public static final int EXSURES_REDUNDANTLY = EXCEPTIONAL_EXAMPLE + 1;
329 public static final int FIELDKW = EXSURES_REDUNDANTLY + 1;
330 // exsures -- an ESC keyword
331 public static final int NO_WACK_FORALL = FIELDKW + 1;
332 public static final int FOR_EXAMPLE = NO_WACK_FORALL + 1;
333 // ghost -- an ESC keyword
334 public static final int IMPLIES_THAT = FOR_EXAMPLE + 1;
335 // helper -- an ESC keyword
336 public static final int HENCE_BY_REDUNDANTLY = IMPLIES_THAT + 1;
337 public static final int HENCE_BY = HENCE_BY_REDUNDANTLY + 1;
338 public static final int INITIALIZER = HENCE_BY + 1;
339 public static final int INITIALLY = INITIALIZER + 1;
340 public static final int INSTANCE = INITIALLY + 1;
341 public static final int INVARIANT_REDUNDANTLY = INSTANCE + 1;
342 // invariant -- an ESC keyword
343 public static final int LOOP_INVARIANT_REDUNDANTLY = INVARIANT_REDUNDANTLY + 1;
344 // loop_invariant -- an ESC keyword
345 public static final int MAINTAINING_REDUNDANTLY = LOOP_INVARIANT_REDUNDANTLY + 1;
346 public static final int MAINTAINING = MAINTAINING_REDUNDANTLY + 1;
347 public static final int MEASURED_BY_REDUNDANTLY = MAINTAINING + 1;
348 public static final int MEASURED_BY = MEASURED_BY_REDUNDANTLY + 1;
349 public static final int METHOD = MEASURED_BY + 1;
350 public static final int MODEL = METHOD + 1;
351 public static final int MODEL_PROGRAM = MODEL + 1;
352 public static final int MODIFIABLE_REDUNDANTLY = MODEL_PROGRAM + 1;
353 public static final int MODIFIABLE = MODIFIABLE_REDUNDANTLY + 1;
354 public static final int MODIFIES_REDUNDANTLY = MODIFIABLE + 1;
355 // modifies -- an ESC keyword
356 // monitored_by -- an ESC keyword
357 // monitored -- an ESC keyword
358 public static final int NESTEDMODIFIERPRAGMA = MODIFIES_REDUNDANTLY + 1;
359 // non_null -- an ESC keyword
360 public static final int NORMAL_BEHAVIOR = NESTEDMODIFIERPRAGMA + 1;
361 public static final int NORMAL_EXAMPLE = NORMAL_BEHAVIOR + 1;
362 // nowarn -- an ESC keyword
363 public static final int OLD = NORMAL_EXAMPLE + 1;
364 public static final int MODELPROGRAM_OR = OLD + 1;
365 public static final int PARSEDSPECS = MODELPROGRAM_OR + 1;
366 public static final int POSTCONDITION_REDUNDANTLY = PARSEDSPECS + 1;
367 public static final int POSTCONDITION = POSTCONDITION_REDUNDANTLY + 1;
368 public static final int PRECONDITION_REDUNDANTLY = POSTCONDITION + 1;
369 public static final int PRECONDITION = PRECONDITION_REDUNDANTLY + 1;
370 public static final int PURE = PRECONDITION + 1;
371 // readable_if -- an ESC keyword
372 public static final int REFINE = PURE + 1;
373 public static final int REPRESENTS_REDUNDANTLY = REFINE + 1;
374 public static final int REPRESENTS = REPRESENTS_REDUNDANTLY + 1;
375 public static final int REQUIRES_REDUNDANTLY = REPRESENTS + 1;
376 // requires -- an ESC keyword
377 public static final int RETURNS_REDUNDANTLY = REQUIRES_REDUNDANTLY + 1;
378 public static final int RETURNS = RETURNS_REDUNDANTLY + 1;
379 // set -- an ESC keyword
380 public static final int SIGNALS_REDUNDANTLY = RETURNS + 1;
381 public static final int SIGNALS = SIGNALS_REDUNDANTLY + 1;
382 public static final int SIGNALS_ONLY = SIGNALS + 1;
383 public static final int SPEC_PROTECTED = SIGNALS_ONLY + 1;
384 // spec_public -- an ESC keyword
385 public static final int STATIC_INITIALIZER = SPEC_PROTECTED + 1;
386 public static final int SUBCLASSING_CONTRACT = STATIC_INITIALIZER + 1;
387 // uninitialized -- an ESC keyword
388 // unreachable -- an ESC keyword
389 public static final int WEAKLY = SUBCLASSING_CONTRACT + 1;
390 public static final int WHEN_REDUNDANTLY = WEAKLY + 1;
391 public static final int WHEN = WHEN_REDUNDANTLY + 1;
392 public static final int WORKING_SPACE_REDUNDANTLY = WHEN + 1;
393 public static final int WORKING_SPACE = WORKING_SPACE_REDUNDANTLY + 1;
394
395 public static final int LASTJMLKEYWORDTAG = WORKING_SPACE;
396
397 //// Tags for ESCJ keywords
398 // These are keywords that are not in JML (either obsolete or
399 // extensions), or are tokens for internal use only
400 // Be sure to keep the esckeywords[] array in synch
401 public static final int FIRSTESCKEYWORDTAG = LASTJMLKEYWORDTAG + 1;
402 public static final int ALSO_ENSURES = FIRSTESCKEYWORDTAG;
403 public static final int ALSO_EXSURES = ALSO_ENSURES + 1;
404 public static final int ALSO_MODIFIES = ALSO_EXSURES + 1;
405 public static final int ALSO_REQUIRES = ALSO_MODIFIES + 1;
406
407 // Include the Universe type annotation keywords (cjbooms)
408 //alx: dw
409 public static final int PEER = ALSO_REQUIRES + 1;
410 public static final int READONLY = PEER + 1;
411 public static final int REP = READONLY + 1;
412 /*
413 public static final int PEER = ALSO_REQUIRES + 1;
414 public static final int READONLY = PEER + 1;
415 public static final int REP = READONLY + 1;
416 */
417 //alx-end
418
419 // Chalin-Kiniry experimental keywords for nullness, purity, and whatnot
420 public static final int NULLABLE = REP + 1;
421 public static final int NULLABLE_BY_DEFAULT = NULLABLE + 1;
422 public static final int NON_NULL_BY_DEFAULT = NULLABLE_BY_DEFAULT + 1;
423 public static final int OBS_PURE = NON_NULL_BY_DEFAULT + 1;
424
425 // Chalin's spec and code modifiers for different math semantics
426 public static final int WACK_JAVA_MATH = OBS_PURE + 1;
427 public static final int WACK_SAFE_MATH = WACK_JAVA_MATH + 1;
428 public static final int WACK_BIGINT_MATH = WACK_SAFE_MATH + 1;
429 public static final int CODE_JAVA_MATH = WACK_BIGINT_MATH + 1;
430 public static final int CODE_SAFE_MATH = CODE_JAVA_MATH + 1;
431 public static final int CODE_BIGINT_MATH = CODE_SAFE_MATH + 1;
432 public static final int SPEC_JAVA_MATH = CODE_BIGINT_MATH + 1;
433 public static final int SPEC_SAFE_MATH = SPEC_JAVA_MATH + 1;
434 public static final int SPEC_BIGINT_MATH = SPEC_SAFE_MATH + 1;
435
436 public static final int LASTESCKEYWORDTAG = SPEC_BIGINT_MATH;
437
438 public static final int LAST_TAG = LASTESCKEYWORDTAG;
439
440 public static final /*@non_null*/ Identifier ExsuresIdnName =
441 Identifier.intern("Optional..Exsures..Id..Name");
442
443 //// Helper functions
444
445 public static /*@non_null*/ String toVcString(int tag) {
446 switch(tag) {
447 case TYPECODE:
448 return "TYPECODE"; // displayed to user as "TYPE"
449 default:
450 break;
451 }
452
453 String s = toString(tag);
454 //@ assume s.length() > 0;
455 if (s.charAt(0) == '\\') {
456 s = s.substring(1);
457 }
458 if (s.equals("lockset")) {
459 s = "LS";
460 } else if (s.equals("result")) {
461 s = "RES";
462 }
463 return s;
464 }
465
466 // Documented in parent.
467
468 public static /*@non_null*/ String toString(int tag) {
469 switch(tag) {
470 // new literal expression (not true keyword)
471 case SYMBOLLIT:
472 return "*SYMBOLLIT*";
473 // guarded commands (not true keywords)
474 case ASSERTCMD:
475 return "*ASSERTCMD*";
476 case ASSUMECMD:
477 return "*ASSUMECMD*";
478 case CHOOSECMD:
479 return "*CHOOSECMD*";
480 case RAISECMD:
481 return "*RAISECMD*";
482 case SKIPCMD:
483 return "*SKIPCMD*";
484 case TRYCMD:
485 return "*TRYCMD*";
486 // informal predicates (not true keyword)
487 case INFORMALPRED_TOKEN:
488 return "*INFORMAL_PREDICATE*";
489 // special symbols
490 case IMPLIES:
491 return "==>";
492 case EXPLIES:
493 return "<==";
494 case IFF:
495 return "<==>";
496 case NIFF:
497 return "<=!=>";
498 case SUBTYPE:
499 return "<:";
500 case DOTDOT:
501 return "..";
502 case LEFTARROW:
503 return "<-";
504 case RIGHTARROW:
505 return "->";
506 case OPENPRAGMA:
507 return "{|";
508 case CLOSEPRAGMA:
509 return "|}";
510 case ANY:
511 return "ANY";
512 case TYPECODE:
513 //return "TYPECODE"; // displayed to user as "TYPE"
514 return "TYPE";
515 case LOCKSET:
516 return "LOCKSET";
517 case OBJECTSET:
518 return "OBJECTSET";
519 case CHK_AS_ASSUME:
520 return "CHK_AS_ASSUME";
521 case CHK_AS_ASSERT:
522 return "CHK_AS_ASSERT";
523 case CHK_AS_SKIP:
524 return "CHK_AS_SKIP";
525 default:
526 if (FIRSTESCKEYWORDTAG <= tag && tag <= LASTESCKEYWORDTAG)
527 return esckeywords[tag - FIRSTESCKEYWORDTAG].toString();
528 else if (FIRSTESCCHECKTAG <= tag && tag <= LASTESCCHECKTAG)
529 return escchecks[tag - FIRSTESCCHECKTAG];
530 else if (FIRSTFUNCTIONTAG <= tag && tag <= LASTFUNCTIONTAG)
531 return escfunctions[tag - FIRSTFUNCTIONTAG];
532 else if (FIRSTJMLKEYWORDTAG <= tag && tag <= LASTJMLKEYWORDTAG)
533 return jmlkeywords[tag - FIRSTJMLKEYWORDTAG].toString();
534 else if (tag == TagConstants.MODIFIESGROUPPRAGMA)
535 return "modifies";
536 else if (tag <= GeneratedTags.LAST_TAG)
537 return GeneratedTags.toString(tag);
538 else {
539 return "Unknown ESC tag <" + tag
540 + " (+" + (tag - javafe.tc.TagConstants.LAST_TAG) + ") >";
541 }
542 }
543 }
544
545 /**
546 * @param keyword the keyword to lookup.
547 * @return the index of the {@link TagConstants} attribute
548 * corresponding to the keyword encoded as an {@link Identifier}
549 * in the parameter 'keyword'. A {@link #NULL} is returned if
550 * the identifier in question is not an ESC/Java or JML keyword
551 * known to {@link TagConstants}.
552 */
553 public static int fromIdentifier(Identifier keyword) {
554 for(int i = 0; i < jmlkeywords.length; i++)
555 if (keyword == jmlkeywords[i]) return i + FIRSTJMLKEYWORDTAG;
556 for(int i = 0; i < esckeywords.length; i++)
557 if (keyword == esckeywords[i]) return i + FIRSTESCKEYWORDTAG;
558 return NULL;
559 }
560
561 public static boolean isKeywordTag(int tag) {
562 return (FIRSTJMLKEYWORDTAG <= tag && tag <= LASTJMLKEYWORDTAG)
563 || (FIRSTESCKEYWORDTAG <= tag && tag <= LASTESCKEYWORDTAG)
564 || tag == TagConstants.NULLLIT;
565 }
566
567 public static int checkFromString(/*@non_null*/ String s) {
568 for (int i = FIRSTESCCHECKTAG; i <= LASTESCCHECKTAG; i++) {
569 if (s.equals(escchecks[i - FIRSTESCCHECKTAG]))
570 return i;
571 }
572 //@ unreachable;
573 Assert.fail("unrecognized check string: \"" + s + "\"");
574 return -1;
575 }
576
577 /**
578 * @return a "redundant-fied" version of the passed tag if it can
579 * be made redundant; otherwise, return the parameter unchanged.
580 */
581 public static int makeRedundant(int tag) {
582 int Result = tag;
583 switch (tag) {
584 case TagConstants.REQUIRES:
585 Result = TagConstants.REQUIRES_REDUNDANTLY; break;
586 case TagConstants.ENSURES:
587 Result = TagConstants.ENSURES_REDUNDANTLY; break;
588 case TagConstants.PRECONDITION:
589 Result = TagConstants.PRECONDITION_REDUNDANTLY; break;
590 case TagConstants.DIVERGES:
591 Result = TagConstants.DIVERGES_REDUNDANTLY; break;
592 case TagConstants.WHEN:
593 Result = TagConstants.WHEN_REDUNDANTLY; break;
594 case TagConstants.POSTCONDITION:
595 Result = TagConstants.POSTCONDITION_REDUNDANTLY; break;
596 case TagConstants.EXSURES:
597 Result = TagConstants.EXSURES_REDUNDANTLY; break;
598 case TagConstants.SIGNALS:
599 Result = TagConstants.SIGNALS_REDUNDANTLY; break;
600 case TagConstants.MODIFIABLE:
601 Result = TagConstants.MODIFIABLE_REDUNDANTLY; break;
602 case TagConstants.ASSIGNABLE:
603 Result = TagConstants.ASSIGNABLE_REDUNDANTLY; break;
604 case TagConstants.MODIFIES:
605 Result = TagConstants.MODIFIES_REDUNDANTLY; break;
606 case TagConstants.MEASURED_BY:
607 Result = TagConstants.MEASURED_BY_REDUNDANTLY; break;
608 case TagConstants.ASSERT:
609 Result = TagConstants.ASSERT_REDUNDANTLY; break;
610 case TagConstants.ASSUME:
611 Result = TagConstants.ASSUME_REDUNDANTLY; break;
612 case TagConstants.LOOP_INVARIANT:
613 Result = TagConstants.LOOP_INVARIANT_REDUNDANTLY; break;
614 case TagConstants.MAINTAINING:
615 Result = TagConstants.MAINTAINING_REDUNDANTLY; break;
616 case TagConstants.DECREASES:
617 Result = TagConstants.DECREASES_REDUNDANTLY; break;
618 case TagConstants.INVARIANT:
619 Result = TagConstants.INVARIANT_REDUNDANTLY; break;
620 case TagConstants.REPRESENTS:
621 Result = TagConstants.REPRESENTS_REDUNDANTLY; break;
622 case TagConstants.CONSTRAINT:
623 Result = TagConstants.CONSTRAINT_REDUNDANTLY; break;
624 case TagConstants.DECREASING:
625 Result = TagConstants.DECREASING_REDUNDANTLY; break;
626 case TagConstants.DURATION:
627 Result = TagConstants.DURATION_REDUNDANTLY; break;
628 case TagConstants.WORKING_SPACE:
629 Result = TagConstants.WORKING_SPACE_REDUNDANTLY; break;
630 case TagConstants.IN:
631 Result = TagConstants.IN_REDUNDANTLY; break;
632 case TagConstants.MAPS:
633 Result = TagConstants.MAPS_REDUNDANTLY; break;
634 case TagConstants.HENCE_BY:
635 Result = TagConstants.HENCE_BY_REDUNDANTLY; break;
636 }
637 return Result;
638 }
639
640 /**
641 * @return an "unredundant-fied" version of the passed tag if it
642 * is redundant; otherwise, return the parameter unchanged.
643 */
644 public static int unRedundant(int tag) {
645 int Result = tag;
646 switch (tag) {
647 case TagConstants.REQUIRES_REDUNDANTLY:
648 Result = TagConstants.REQUIRES; break;
649 case TagConstants.ENSURES_REDUNDANTLY:
650 Result = TagConstants.ENSURES; break;
651 case TagConstants.PRECONDITION_REDUNDANTLY:
652 Result = TagConstants.PRECONDITION; break;
653 case TagConstants.DIVERGES_REDUNDANTLY:
654 Result = TagConstants.DIVERGES; break;
655 case TagConstants.WHEN_REDUNDANTLY:
656 Result = TagConstants.WHEN; break;
657 case TagConstants.POSTCONDITION_REDUNDANTLY:
658 Result = TagConstants.POSTCONDITION; break;
659 case TagConstants.EXSURES_REDUNDANTLY:
660 Result = TagConstants.EXSURES; break;
661 case TagConstants.SIGNALS_REDUNDANTLY:
662 Result = TagConstants.SIGNALS; break;
663 case TagConstants.MODIFIABLE_REDUNDANTLY:
664 Result = TagConstants.MODIFIABLE; break;
665 case TagConstants.ASSIGNABLE_REDUNDANTLY:
666 Result = TagConstants.ASSIGNABLE; break;
667 case TagConstants.MODIFIES_REDUNDANTLY:
668 Result = TagConstants.MODIFIES; break;
669 case TagConstants.MEASURED_BY_REDUNDANTLY:
670 Result = TagConstants.MEASURED_BY; break;
671 case TagConstants.ASSERT_REDUNDANTLY:
672 Result = TagConstants.ASSERT; break;
673 case TagConstants.ASSUME_REDUNDANTLY:
674 Result = TagConstants.ASSUME; break;
675 case TagConstants.LOOP_INVARIANT_REDUNDANTLY:
676 Result = TagConstants.LOOP_INVARIANT; break;
677 case TagConstants.MAINTAINING_REDUNDANTLY:
678 Result = TagConstants.MAINTAINING; break;
679 case TagConstants.DECREASES_REDUNDANTLY:
680 Result = TagConstants.DECREASES; break;
681 case TagConstants.INVARIANT_REDUNDANTLY:
682 Result = TagConstants.INVARIANT; break;
683 case TagConstants.REPRESENTS_REDUNDANTLY:
684 Result = TagConstants.REPRESENTS; break;
685 case TagConstants.CONSTRAINT_REDUNDANTLY:
686 Result = TagConstants.CONSTRAINT; break;
687 case TagConstants.DECREASING_REDUNDANTLY:
688 Result = TagConstants.DECREASING; break;
689 case TagConstants.DURATION_REDUNDANTLY:
690 Result = TagConstants.DURATION; break;
691 case TagConstants.WORKING_SPACE_REDUNDANTLY:
692 Result = TagConstants.WORKING_SPACE; break;
693 case TagConstants.IN_REDUNDANTLY:
694 Result = TagConstants.IN; break;
695 case TagConstants.MAPS_REDUNDANTLY:
696 Result = TagConstants.MAPS; break;
697 case TagConstants.HENCE_BY_REDUNDANTLY:
698 Result = TagConstants.HENCE_BY; break;
699 }
700 return Result;
701 }
702
703 public static boolean isRedundant(int tag) {
704 return (tag == TagConstants.REQUIRES_REDUNDANTLY
705 || tag == TagConstants.ASSERT_REDUNDANTLY
706 || tag == TagConstants.ASSIGNABLE_REDUNDANTLY
707 || tag == TagConstants.ASSUME_REDUNDANTLY
708 || tag == TagConstants.CONSTRAINT_REDUNDANTLY
709 || tag == TagConstants.DECREASES_REDUNDANTLY
710 || tag == TagConstants.DECREASING_REDUNDANTLY
711 || tag == TagConstants.DIVERGES_REDUNDANTLY
712 || tag == TagConstants.DURATION_REDUNDANTLY
713 || tag == TagConstants.ENSURES_REDUNDANTLY
714 || tag == TagConstants.EXSURES_REDUNDANTLY
715 || tag == TagConstants.HENCE_BY_REDUNDANTLY
716 || tag == TagConstants.INVARIANT_REDUNDANTLY
717 || tag == TagConstants.IN_REDUNDANTLY
718 || tag == TagConstants.LOOP_INVARIANT_REDUNDANTLY
719 || tag == TagConstants.MAINTAINING_REDUNDANTLY
720 || tag == TagConstants.MAPS_REDUNDANTLY
721 || tag == TagConstants.MEASURED_BY_REDUNDANTLY
722 || tag == TagConstants.MODIFIABLE_REDUNDANTLY
723 || tag == TagConstants.MODIFIES_REDUNDANTLY
724 || tag == TagConstants.POSTCONDITION_REDUNDANTLY
725 || tag == TagConstants.PRECONDITION_REDUNDANTLY
726 || tag == TagConstants.REPRESENTS_REDUNDANTLY
727 || tag == TagConstants.SIGNALS_REDUNDANTLY
728 || tag == TagConstants.WHEN_REDUNDANTLY
729 || tag == TagConstants.WORKING_SPACE_REDUNDANTLY
730 );
731 }
732
733 public final static /*@non_null*/ String[] escchecks = {
734 "ZeroDiv",
735 "ArrayStore",
736 "Assert",
737 "Cast",
738 "Reachable",
739 "Inconsistent",
740 "Constraint",
741 "CLeak",
742 "DecreasesBound",
743 "Decreases",
744 "Unreadable",
745 "Undefined",
746 "IndexNegative",
747 "IndexTooBig",
748 "Uninit",
749 "ILeak",
750 "Initially",
751 "Deadlock",
752 "LoopInv",
753 "LoopObjInv",
754 "ModExt",
755 "Modifies",
756 "NegSize",
757 "NonNull",
758 "NonNullInit",
759 "NonNullResult",
760 "Null",
761 "Invariant",
762 "OwnerNull",
763 "Post",
764 "Pre",
765 "Race",
766 "RaceAllNull",
767 "Unenforcable",
768 "Exception",
769 "SpecificationException",
770 "Deferred",
771 "Writable",
772 "vc.Quiet", // printed in debugging output only
773 "Assume", // internal use only
774 "AdditionalInfo", // internal use only
775 "Free" // printed in debugging output only
776 };
777
778 private static /*@non_null*/ String[] escfunctions = {
779 "allocLT",
780 "allocLE",
781 "anyEQ",
782 "anyNE",
783 "arrayLength",
784 "arrayFresh",
785 "arrayMake",
786 "arrayShapeMore",
787 "arrayShapeOne",
788 "asElems",
789 "asField",
790 "asLockSet",
791 "boolAnd",
792 "boolAndX",
793 "boolEq",
794 "boolImplies",
795 "boolNE",
796 "boolNot",
797 "boolOr",
798 "cast",
799 "classLiteral",
800 "termConditional",
801 "eClosedTime",
802 "fClosedTime",
803 "floatingAdd",
804 "floatingDiv",
805 "floatingEQ",
806 "floatingGE",
807 "floatingGT",
808 "floatingLE",
809 "floatingLT",
810 "floatingMod",
811 "floatingMul",
812 "floatingNE",
813 "floatingNeg",
814 "floatingSub",
815 "integralAdd",
816 "integralAnd",
817 "integralDiv",
818 "integralEQ",
819 "integralGE",
820 "integralGT",
821 "integralLE",
822 "integralLT",
823 "integralMod",
824 "integralMul",
825 "integralNE",
826 "integralNeg",
827 "integralNot",
828 "integralOr",
829 "intShiftL",
830 "longShiftL",
831 "intShiftAR",
832 "longShiftAR",
833 "intShiftUR",
834 "longShiftUR",
835 "integralSub",
836 "integralXor",
837 "|intern:|", // maps int to String for Strings interned by ESC/Java
838 "|interned:|", // maps String to boolean to say whether a String is interned, per Java semantics
839 "is",
840 "isAllocated",
841 "isNewArray",
842 "lockLE",
843 "lockLT",
844 "methodCall",
845 "refEQ",
846 "refNE",
847 "select",
848 "store",
849 "stringCat",
850 "stringCatP",
851 "typeEQ",
852 "typeNE",
853 "typeLE",
854 "unset",
855 "vAllocTime"
856 };
857
858 static public final String STRINGCATINFIX = "java.lang.String._infixConcat_";
859 // Must match method name in String.spec
860
861 private static /*@non_null*/ Identifier[] jmlkeywords = {
862 Identifier.intern("assume"),
863 Identifier.intern("axiom"),
864 Identifier.intern("code_contract"),
865 Identifier.intern("decreases"),
866 Identifier.intern("\\dttfsa"),
867 Identifier.intern("ensures"),
868 Identifier.intern("\\nonnullelements"),
869 Identifier.intern("\\elemtype"),
870 Identifier.intern("\\exists"),
871 Identifier.intern("exsures"),
872 Identifier.intern("\\fresh"),
873 Identifier.intern("\\forall"),
874 Identifier.intern("function"),
875 Identifier.intern("ghost"),
876 Identifier.intern("helper"),
877 Identifier.intern("immutable"),
878 Identifier.intern("in"),
879 Identifier.intern("in_redundantly"),
880 Identifier.intern("\\into"),
881 Identifier.intern("invariant"),
882 Identifier.intern("\\lblpos"),
883 Identifier.intern("\\lblneg"),
884 Identifier.intern("loop_invariant"),
885 Identifier.intern("loop_predicate"),
886 Identifier.intern("\\lockset"),
887 Identifier.intern("maps"),
888 Identifier.intern("maps_redundantly"),
889 Identifier.intern("\\max"),
890 Identifier.intern("modifies"),
891 Identifier.intern("monitored"),
892 Identifier.intern("monitored_by"),
893 Identifier.intern("monitors_for"),
894 Identifier.intern("non_null"),
895 Identifier.intern("nowarn"),
896 Identifier.intern("\\old"), // TagConstants.PRE
897 Identifier.intern("readable"),
898 Identifier.intern("readable_if"),
899 Identifier.intern("\\result"),
900 Identifier.intern("requires"),
901 Identifier.intern("set"),
902 Identifier.intern("spec_public"),
903 Identifier.intern("still_deferred"),
904 Identifier.intern("\\type"), // TYPE
905 Identifier.intern("\\TYPE"), // TYPETYPE
906 Identifier.intern("\\typeof"),
907 Identifier.intern("uninitialized"),
908 Identifier.intern("unreachable"),
909 Identifier.intern("writable_deferred"),
910 Identifier.intern("writable_if"),
911 Identifier.intern("writable"),
912 Identifier.intern("skolem_constant"),
913 Identifier.intern("\\bigint"),
914 Identifier.intern("\\duration"),
915 Identifier.intern("\\everything"),
916 Identifier.intern("\\fields_of"),
917 Identifier.intern("\\invariant_for"),
918 Identifier.intern("\\is_initialized"),
919 Identifier.intern("\\max"),
920 Identifier.intern("\\min"),
921 Identifier.intern("\\nothing"),
922 Identifier.intern("\\not_modified"),
923 Identifier.intern("\\not_specified"),
924 Identifier.intern("\\nowarn"),
925 Identifier.intern("\\nowarn_op"),
926 Identifier.intern("\\num_of"),
927 Identifier.intern("\\other"),
928 Identifier.intern("\\private_data"),
929 Identifier.intern("\\product"),
930 Identifier.intern("\\reach"),
931 Identifier.intern("\\real"),
932 Identifier.intern("\\space"),
933 Identifier.intern("\\such_that"),
934 Identifier.intern("\\sum"),
935 Identifier.intern("\\warn"),
936 Identifier.intern("\\warn_op"),
937 Identifier.intern("\\working_space"),
938 Identifier.intern("abrupt_behavior"),
939 Identifier.intern("accessible_redundantly"),
940 Identifier.intern("accessible"),
941 Identifier.intern("also"),
942 Identifier.intern("---also_refine---"), // internal use only
943 Identifier.intern("assert_redundantly"),
944 Identifier.intern("assignable_redundantly"),
945 Identifier.intern("assignable"),
946 Identifier.intern("assume_redundantly"),
947 Identifier.intern("behavior"),
948 Identifier.intern("breaks_redundantly"),
949 Identifier.intern("breaks"),
950 Identifier.intern("callable_redundantly"),
951 Identifier.intern("callable"),
952 Identifier.intern("choose_if"),
953 Identifier.intern("choose"),
954 Identifier.intern("constraint_redundantly"),
955 Identifier.intern("constraint"),
956 Identifier.intern("constructor"),
957 Identifier.intern("continues_redundantly"),
958 Identifier.intern("continues"),
959 Identifier.intern("decreases_redundantly"),
960 Identifier.intern("decreasing_redundantly"),
961 Identifier.intern("decreasing"),
962 Identifier.intern("depends_redundantly"),
963 Identifier.intern("depends"),
964 Identifier.intern("diverges_redundantly"),
965 Identifier.intern("diverges"),
966 Identifier.intern("duration_redundantly"),
967 Identifier.intern("duration"),
968 Identifier.intern("---end---"), // Internal use only
969 Identifier.intern("ensures_redundantly"),
970 Identifier.intern("example"),
971 Identifier.intern("exceptional_behavior"),
972 Identifier.intern("exceptional_example"),
973 Identifier.intern("exsures_redundantly"),
974 Identifier.intern("field"),
975 Identifier.intern("forall"),
976 Identifier.intern("for_example"),
977 Identifier.intern("implies_that"),
978 Identifier.intern("hence_by_redundantly"),
979 Identifier.intern("hence_by"),
980 Identifier.intern("initializer"),
981 Identifier.intern("initially"),
982 Identifier.intern("instance"),
983 Identifier.intern("invariant_redundantly"),
984 Identifier.intern("loop_invariant_redundantly"),
985 Identifier.intern("maintaining_redundantly"),
986 Identifier.intern("maintaining"),
987 Identifier.intern("measured_by_redundantly"),
988 Identifier.intern("measured_by"),
989 Identifier.intern("method"),
990 Identifier.intern("model"),
991 Identifier.intern("model_program"),
992 Identifier.intern("modifiable_redundantly"),
993 Identifier.intern("modifiable"),
994 Identifier.intern("modifies_redundantly"),
995 Identifier.intern("--- nested specs ---"),
996 Identifier.intern("normal_behavior"),
997 Identifier.intern("normal_example"),
998 Identifier.intern("old"),
999 Identifier.intern("or"),
1000 Identifier.intern("--- parsed specs ---"),
1001 Identifier.intern("post_redundantly"),
1002 Identifier.intern("post"),
1003 Identifier.intern("pre_redundantly"),
1004 Identifier.intern("pre"), // PRE not PRE (which is \old )
1005 Identifier.intern("pure"),
1006 Identifier.intern("refine"),
1007 Identifier.intern("represents_redundantly"),
1008 Identifier.intern("represents"),
1009 Identifier.intern("requires_redundantly"),
1010 Identifier.intern("returns_redundantly"),
1011 Identifier.intern("returns"),
1012 Identifier.intern("signals_redundantly"),
1013 Identifier.intern("signals"),
1014 Identifier.intern("signals_only"),
1015 Identifier.intern("spec_protected"),
1016 Identifier.intern("static_initializer"),
1017 Identifier.intern("subclassing_contract"),
1018 Identifier.intern("weakly"),
1019 Identifier.intern("when_redundantly"),
1020 Identifier.intern("when"),
1021 Identifier.intern("working_space_redundantly"),
1022 Identifier.intern("working_space")
1023 };
1024
1025 private static /*@non_null*/ Identifier[] esckeywords = {
1026 Identifier.intern("also_ensures"),
1027 Identifier.intern("also_exsures"),
1028 Identifier.intern("also_modifies"),
1029 Identifier.intern("also_requires"),
1030
1031 // Universe type annotations (cjbooms)
1032 Identifier.intern("\\peer"),
1033 Identifier.intern("\\readonly"),
1034 Identifier.intern("\\rep"),
1035
1036 // Chalin-Kiniry experimental keywords for nullness, purity, and whatnot
1037 Identifier.intern("nullable"),
1038 Identifier.intern("nullable_by_default"),
1039 Identifier.intern("non_null_by_default"),
1040 Identifier.intern("obs_pure"),
1041
1042 // Chalin's spec and code modifiers for different math semantics
1043 Identifier.intern("\\java_math"),
1044 Identifier.intern("\\safe_math"),
1045 Identifier.intern("\\bigint_math"),
1046 Identifier.intern("code_java_math"),
1047 Identifier.intern("code_safe_math"),
1048 Identifier.intern("code_bigint_math"),
1049 Identifier.intern("spec_java_math"),
1050 Identifier.intern("spec_safe_math"),
1051 Identifier.intern("spec_bigint_math")
1052 };
1053
1054 public static void main(/*@ non_null @*/ String[] args) {
1055 for(int i = FIRST_TAG; i <= LAST_TAG; i++ )
1056 System.out.println(i + " " + toString(i));
1057 }
1058
1059 // This initialization code is simply a quick check that the arrays
1060 // are consistent in length.
1061
1062 static private void comp(int i, int j, /*@non_null*/ String s) {
1063 if (i != j)
1064 System.out.println("Mismatched length ("
1065 + i + " vs. " + j + ") in " + s);
1066 }
1067
1068 static {
1069 comp(esckeywords.length, LASTESCKEYWORDTAG - FIRSTESCKEYWORDTAG + 1,
1070 "esckeywords");
1071 comp(jmlkeywords.length, LASTJMLKEYWORDTAG - FIRSTJMLKEYWORDTAG + 1,
1072 "jmlkeywords");
1073 comp(escfunctions.length, LASTFUNCTIONTAG - FIRSTFUNCTIONTAG + 1,
1074 "escfunctions");
1075 comp(escchecks.length, LASTESCCHECKTAG - FIRSTESCCHECKTAG + 1,
1076 "escchecks");
1077 }
1078 }