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