escjava.ast
Class TagConstants
java.lang.Object
javafe.ast.GeneratedTags
javafe.ast.OperatorTags
javafe.ast.TagConstants
javafe.parser.TagConstants
javafe.tc.TagConstants
escjava.ast.GeneratedTags
escjava.ast.TagConstants
- public class TagConstants
- extends GeneratedTags
Fields inherited from class escjava.ast.GeneratedTags |
ARRAYRANGEREFEXPR, CALL, CONDITION, DEFPRED, DEFPREDAPPLEXPR, DEFPREDLETEXPR, DYNINSTCMD, EVERYTHINGEXPR, GETSCMD, GHOSTDECLPRAGMA, GUARDEXPR, IDENTIFIERMODIFIERPRAGMA, IMPORTPRAGMA, LABELEXPR, LOCKSETEXPR, LOOPCMD, MODELCONSTRUCTORDECLPRAGMA, MODELDECLPRAGMA, MODELMETHODDECLPRAGMA, MODELTYPEPRAGMA, MODIFIESGROUPPRAGMA, NOTHINGEXPR, NOTMODIFIEDEXPR, NOTSPECIFIEDEXPR, NOWARNPRAGMA, REACHMODIFIERPRAGMA, REFINEPRAGMA, RESEXPR, RESTOREFROMCMD, SEQCMD, SETCOMPEXPR, SETSTMTPRAGMA, SKOLEMCONSTANTPRAGMA, SPEC, STILLDEFERREDDECLPRAGMA, SUBGETSCMD, SUBSTEXPR, SUBSUBGETSCMD, TYPEEXPR, VARINCMD, WILDREFEXPR |
Fields inherited from class javafe.parser.TagConstants |
ABSTRACT, ASSERT, BOOLEAN, BREAK, BYTE, C_COMMENT, CASE, CATCH, CHAR, CLASS, COLON, COMMA, CONST, CONTINUE, DEFAULT, DO, DOUBLE, ELSE, EOF, EOL_COMMENT, EXTENDS, FALSE, FIELD, FINAL, FINALLY, FIRST_KEYWORD, FLOAT, FOR, GOTO, IF, IMPLEMENTS, IMPORT, INSTANCEOF, INT, INTERFACE, LAST_KEYWORD, LBRACE, LEXICALPRAGMA, LONG, LPAREN, LSQBRACKET, MAX_INT_PLUS_ONE, MAX_LONG_PLUS_ONE, MODIFIERPRAGMA, NATIVE, NEW, NULL, PACKAGE, POSTMODIFIERPRAGMA, PRIVATE, PROTECTED, PUBLIC, QUESTIONMARK, RBRACE, RETURN, RPAREN, RSQBRACKET, SEMICOLON, SHORT, STATIC, STMTPRAGMA, STRICT, SUPER, SWITCH, SYNCHRONIZED, THIS, THROW, THROWS, TRANSIENT, TRUE, TRY, TYPEDECLELEMPRAGMA, TYPEMODIFIERPRAGMA, UNKNOWN_KEYWORD, VOID, VOLATILE, WHILE |
Fields inherited from class javafe.ast.TagConstants |
BOOLEANLIT, BOOLEANTYPE, BYTELIT, BYTETYPE, CHARLIT, CHARTYPE, DOUBLELIT, DOUBLETYPE, ERRORTYPE, FLOATLIT, FLOATTYPE, IDENT, INTLIT, INTTYPE, LONGLIT, LONGTYPE, NULLLIT, NULLTYPE, SHORTLIT, SHORTTYPE, STRINGLIT, VOIDTYPE |
Fields inherited from class javafe.ast.OperatorTags |
ADD, AND, ASGADD, ASGBITAND, ASGBITOR, ASGBITXOR, ASGDIV, ASGLSHIFT, ASGMUL, ASGREM, ASGRSHIFT, ASGSUB, ASGURSHIFT, ASSIGN, BITAND, BITNOT, BITOR, BITXOR, DEC, DIV, EQ, FIRST_TAG, GE, GT, INC, LE, LSHIFT, LT, MOD, NE, NOT, OR, POSTFIXDEC, POSTFIXINC, RSHIFT, STAR, SUB, UNARYADD, UNARYSUB, URSHIFT |
Fields inherited from class javafe.ast.GeneratedTags |
AMBIGUOUSMETHODINVOCATION, AMBIGUOUSVARIABLEACCESS, ARRAYINIT, ARRAYREFEXPR, ARRAYTYPE, ASSERTSTMT, BLOCKSTMT, BREAKSTMT, CASTEXPR, CATCHCLAUSE, CLASSDECL, CLASSDECLSTMT, CLASSLITERAL, COMPILATIONUNIT, COMPOUNDNAME, CONDEXPR, CONSTRUCTORDECL, CONSTRUCTORINVOCATION, CONTINUESTMT, DOSTMT, EVALSTMT, EXPROBJECTDESIGNATOR, FIELDACCESS, FIELDDECL, FORMALPARADECL, FORSTMT, IFSTMT, INITBLOCK, INSTANCEOFEXPR, INTERFACEDECL, LABELSTMT, LOCALVARDECL, METHODDECL, METHODINVOCATION, NEWARRAYEXPR, NEWINSTANCEEXPR, ONDEMANDIMPORTDECL, PARENEXPR, RETURNSTMT, SIMPLENAME, SINGLETYPEIMPORTDECL, SKIPSTMT, SUPEROBJECTDESIGNATOR, SWITCHLABEL, SWITCHSTMT, SYNCHRONIZESTMT, THISEXPR, THROWSTMT, TRYCATCHSTMT, TRYFINALLYSTMT, TYPENAME, TYPEOBJECTDESIGNATOR, VARDECLSTMT, VARIABLEACCESS, WHILESTMT |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
IMPLIES
public static final int IMPLIES
- See Also:
- Constant Field Values
EXPLIES
public static final int EXPLIES
- See Also:
- Constant Field Values
IFF
public static final int IFF
- See Also:
- Constant Field Values
NIFF
public static final int NIFF
- See Also:
- Constant Field Values
SUBTYPE
public static final int SUBTYPE
- See Also:
- Constant Field Values
DOTDOT
public static final int DOTDOT
- See Also:
- Constant Field Values
LEFTARROW
public static final int LEFTARROW
- See Also:
- Constant Field Values
RIGHTARROW
public static final int RIGHTARROW
- See Also:
- Constant Field Values
OPENPRAGMA
public static final int OPENPRAGMA
- See Also:
- Constant Field Values
CLOSEPRAGMA
public static final int CLOSEPRAGMA
- See Also:
- Constant Field Values
SYMBOLLIT
public static final int SYMBOLLIT
- See Also:
- Constant Field Values
ANY
public static final int ANY
- See Also:
- Constant Field Values
TYPECODE
public static final int TYPECODE
- See Also:
- Constant Field Values
BIGINTTYPE
public static final int BIGINTTYPE
- See Also:
- Constant Field Values
REALTYPE
public static final int REALTYPE
- See Also:
- Constant Field Values
LOCKSET
public static final int LOCKSET
- See Also:
- Constant Field Values
OBJECTSET
public static final int OBJECTSET
- See Also:
- Constant Field Values
ASSERTCMD
public static final int ASSERTCMD
- See Also:
- Constant Field Values
ASSUMECMD
public static final int ASSUMECMD
- See Also:
- Constant Field Values
CHOOSECMD
public static final int CHOOSECMD
- See Also:
- Constant Field Values
RAISECMD
public static final int RAISECMD
- See Also:
- Constant Field Values
SKIPCMD
public static final int SKIPCMD
- See Also:
- Constant Field Values
TRYCMD
public static final int TRYCMD
- See Also:
- Constant Field Values
INFORMALPRED_TOKEN
public static final int INFORMALPRED_TOKEN
- See Also:
- Constant Field Values
FIRSTESCCHECKTAG
public static final int FIRSTESCCHECKTAG
- See Also:
- Constant Field Values
CHKARITHMETIC
public static final int CHKARITHMETIC
- See Also:
- Constant Field Values
CHKARRAYSTORE
public static final int CHKARRAYSTORE
- See Also:
- Constant Field Values
CHKASSERT
public static final int CHKASSERT
- See Also:
- Constant Field Values
CHKCLASSCAST
public static final int CHKCLASSCAST
- See Also:
- Constant Field Values
CHKCODEREACHABILITY
public static final int CHKCODEREACHABILITY
- See Also:
- Constant Field Values
CHKCONSISTENT
public static final int CHKCONSISTENT
- See Also:
- Constant Field Values
CHKCONSTRAINT
public static final int CHKCONSTRAINT
- See Also:
- Constant Field Values
CHKCONSTRUCTORLEAK
public static final int CHKCONSTRUCTORLEAK
- See Also:
- Constant Field Values
CHKDECREASES_BOUND
public static final int CHKDECREASES_BOUND
- See Also:
- Constant Field Values
CHKDECREASES_DECR
public static final int CHKDECREASES_DECR
- See Also:
- Constant Field Values
CHKDEFINEDNESS
public static final int CHKDEFINEDNESS
- See Also:
- Constant Field Values
CHKINDEXNEGATIVE
public static final int CHKINDEXNEGATIVE
- See Also:
- Constant Field Values
CHKINDEXTOOBIG
public static final int CHKINDEXTOOBIG
- See Also:
- Constant Field Values
CHKINITIALIZATION
public static final int CHKINITIALIZATION
- See Also:
- Constant Field Values
CHKINITIALIZERLEAK
public static final int CHKINITIALIZERLEAK
- See Also:
- Constant Field Values
CHKINITIALLY
public static final int CHKINITIALLY
- See Also:
- Constant Field Values
CHKLOCKINGORDER
public static final int CHKLOCKINGORDER
- See Also:
- Constant Field Values
CHKLOOPINVARIANT
public static final int CHKLOOPINVARIANT
- See Also:
- Constant Field Values
CHKLOOPOBJECTINVARIANT
public static final int CHKLOOPOBJECTINVARIANT
- See Also:
- Constant Field Values
CHKMODIFIESEXTENSION
public static final int CHKMODIFIESEXTENSION
- See Also:
- Constant Field Values
CHKMODIFIES
public static final int CHKMODIFIES
- See Also:
- Constant Field Values
CHKNEGATIVEARRAYSIZE
public static final int CHKNEGATIVEARRAYSIZE
- See Also:
- Constant Field Values
CHKNONNULL
public static final int CHKNONNULL
- See Also:
- Constant Field Values
CHKNONNULLINIT
public static final int CHKNONNULLINIT
- See Also:
- Constant Field Values
CHKNONNULLRESULT
public static final int CHKNONNULLRESULT
- See Also:
- Constant Field Values
CHKNULLPOINTER
public static final int CHKNULLPOINTER
- See Also:
- Constant Field Values
CHKOBJECTINVARIANT
public static final int CHKOBJECTINVARIANT
- See Also:
- Constant Field Values
CHKOWNERNULL
public static final int CHKOWNERNULL
- See Also:
- Constant Field Values
CHKPOSTCONDITION
public static final int CHKPOSTCONDITION
- See Also:
- Constant Field Values
CHKPRECONDITION
public static final int CHKPRECONDITION
- See Also:
- Constant Field Values
CHKSHARING
public static final int CHKSHARING
- See Also:
- Constant Field Values
CHKSHARINGALLNULL
public static final int CHKSHARINGALLNULL
- See Also:
- Constant Field Values
CHKUNENFORCEBLEOBJECTINVARIANT
public static final int CHKUNENFORCEBLEOBJECTINVARIANT
- See Also:
- Constant Field Values
CHKUNEXPECTEDEXCEPTION
public static final int CHKUNEXPECTEDEXCEPTION
- See Also:
- Constant Field Values
CHKUNEXPECTEDEXCEPTION2
public static final int CHKUNEXPECTEDEXCEPTION2
- See Also:
- Constant Field Values
CHKWRITABLEDEFERRED
public static final int CHKWRITABLEDEFERRED
- See Also:
- Constant Field Values
CHKWRITABLE
public static final int CHKWRITABLE
- See Also:
- Constant Field Values
CHKQUIET
public static final int CHKQUIET
- See Also:
- Constant Field Values
CHKASSUME
public static final int CHKASSUME
- See Also:
- Constant Field Values
CHKADDINFO
public static final int CHKADDINFO
- See Also:
- Constant Field Values
CHKFREE
public static final int CHKFREE
- See Also:
- Constant Field Values
LASTESCCHECKTAG
public static final int LASTESCCHECKTAG
- See Also:
- Constant Field Values
FIRSTFUNCTIONTAG
public static final int FIRSTFUNCTIONTAG
- See Also:
- Constant Field Values
ALLOCLT
public static final int ALLOCLT
- See Also:
- Constant Field Values
ALLOCLE
public static final int ALLOCLE
- See Also:
- Constant Field Values
ANYEQ
public static final int ANYEQ
- See Also:
- Constant Field Values
ANYNE
public static final int ANYNE
- See Also:
- Constant Field Values
ARRAYLENGTH
public static final int ARRAYLENGTH
- See Also:
- Constant Field Values
ARRAYFRESH
public static final int ARRAYFRESH
- See Also:
- Constant Field Values
ARRAYMAKE
public static final int ARRAYMAKE
- See Also:
- Constant Field Values
ARRAYSHAPEMORE
public static final int ARRAYSHAPEMORE
- See Also:
- Constant Field Values
ARRAYSHAPEONE
public static final int ARRAYSHAPEONE
- See Also:
- Constant Field Values
ASELEMS
public static final int ASELEMS
- See Also:
- Constant Field Values
ASFIELD
public static final int ASFIELD
- See Also:
- Constant Field Values
ASLOCKSET
public static final int ASLOCKSET
- See Also:
- Constant Field Values
BOOLAND
public static final int BOOLAND
- See Also:
- Constant Field Values
BOOLANDX
public static final int BOOLANDX
- See Also:
- Constant Field Values
BOOLEQ
public static final int BOOLEQ
- See Also:
- Constant Field Values
BOOLIMPLIES
public static final int BOOLIMPLIES
- See Also:
- Constant Field Values
BOOLNE
public static final int BOOLNE
- See Also:
- Constant Field Values
BOOLNOT
public static final int BOOLNOT
- See Also:
- Constant Field Values
BOOLOR
public static final int BOOLOR
- See Also:
- Constant Field Values
CAST
public static final int CAST
- See Also:
- Constant Field Values
CLASSLITERALFUNC
public static final int CLASSLITERALFUNC
- See Also:
- Constant Field Values
CONDITIONAL
public static final int CONDITIONAL
- See Also:
- Constant Field Values
ECLOSEDTIME
public static final int ECLOSEDTIME
- See Also:
- Constant Field Values
FCLOSEDTIME
public static final int FCLOSEDTIME
- See Also:
- Constant Field Values
FLOATINGADD
public static final int FLOATINGADD
- See Also:
- Constant Field Values
FLOATINGDIV
public static final int FLOATINGDIV
- See Also:
- Constant Field Values
FLOATINGEQ
public static final int FLOATINGEQ
- See Also:
- Constant Field Values
FLOATINGGE
public static final int FLOATINGGE
- See Also:
- Constant Field Values
FLOATINGGT
public static final int FLOATINGGT
- See Also:
- Constant Field Values
FLOATINGLE
public static final int FLOATINGLE
- See Also:
- Constant Field Values
FLOATINGLT
public static final int FLOATINGLT
- See Also:
- Constant Field Values
FLOATINGMOD
public static final int FLOATINGMOD
- See Also:
- Constant Field Values
FLOATINGMUL
public static final int FLOATINGMUL
- See Also:
- Constant Field Values
FLOATINGNE
public static final int FLOATINGNE
- See Also:
- Constant Field Values
FLOATINGNEG
public static final int FLOATINGNEG
- See Also:
- Constant Field Values
FLOATINGSUB
public static final int FLOATINGSUB
- See Also:
- Constant Field Values
INTEGRALADD
public static final int INTEGRALADD
- See Also:
- Constant Field Values
INTEGRALAND
public static final int INTEGRALAND
- See Also:
- Constant Field Values
INTEGRALDIV
public static final int INTEGRALDIV
- See Also:
- Constant Field Values
INTEGRALEQ
public static final int INTEGRALEQ
- See Also:
- Constant Field Values
INTEGRALGE
public static final int INTEGRALGE
- See Also:
- Constant Field Values
INTEGRALGT
public static final int INTEGRALGT
- See Also:
- Constant Field Values
INTEGRALLE
public static final int INTEGRALLE
- See Also:
- Constant Field Values
INTEGRALLT
public static final int INTEGRALLT
- See Also:
- Constant Field Values
INTEGRALMOD
public static final int INTEGRALMOD
- See Also:
- Constant Field Values
INTEGRALMUL
public static final int INTEGRALMUL
- See Also:
- Constant Field Values
INTEGRALNE
public static final int INTEGRALNE
- See Also:
- Constant Field Values
INTEGRALNEG
public static final int INTEGRALNEG
- See Also:
- Constant Field Values
INTEGRALNOT
public static final int INTEGRALNOT
- See Also:
- Constant Field Values
INTEGRALOR
public static final int INTEGRALOR
- See Also:
- Constant Field Values
INTSHIFTL
public static final int INTSHIFTL
- See Also:
- Constant Field Values
LONGSHIFTL
public static final int LONGSHIFTL
- See Also:
- Constant Field Values
INTSHIFTR
public static final int INTSHIFTR
- See Also:
- Constant Field Values
LONGSHIFTR
public static final int LONGSHIFTR
- See Also:
- Constant Field Values
INTSHIFTRU
public static final int INTSHIFTRU
- See Also:
- Constant Field Values
LONGSHIFTRU
public static final int LONGSHIFTRU
- See Also:
- Constant Field Values
INTEGRALSUB
public static final int INTEGRALSUB
- See Also:
- Constant Field Values
INTEGRALXOR
public static final int INTEGRALXOR
- See Also:
- Constant Field Values
INTERN
public static final int INTERN
- See Also:
- Constant Field Values
INTERNED
public static final int INTERNED
- See Also:
- Constant Field Values
IS
public static final int IS
- See Also:
- Constant Field Values
ISALLOCATED
public static final int ISALLOCATED
- See Also:
- Constant Field Values
ISNEWARRAY
public static final int ISNEWARRAY
- See Also:
- Constant Field Values
LOCKLE
public static final int LOCKLE
- See Also:
- Constant Field Values
LOCKLT
public static final int LOCKLT
- See Also:
- Constant Field Values
METHODCALL
public static final int METHODCALL
- See Also:
- Constant Field Values
REFEQ
public static final int REFEQ
- See Also:
- Constant Field Values
REFNE
public static final int REFNE
- See Also:
- Constant Field Values
SELECT
public static final int SELECT
- See Also:
- Constant Field Values
STORE
public static final int STORE
- See Also:
- Constant Field Values
STRINGCAT
public static final int STRINGCAT
- See Also:
- Constant Field Values
STRINGCATP
public static final int STRINGCATP
- See Also:
- Constant Field Values
TYPEEQ
public static final int TYPEEQ
- See Also:
- Constant Field Values
TYPENE
public static final int TYPENE
- See Also:
- Constant Field Values
TYPELE
public static final int TYPELE
- See Also:
- Constant Field Values
UNSET
public static final int UNSET
- See Also:
- Constant Field Values
VALLOCTIME
public static final int VALLOCTIME
- See Also:
- Constant Field Values
LASTFUNCTIONTAG
public static final int LASTFUNCTIONTAG
- See Also:
- Constant Field Values
CHK_AS_ASSUME
public static final int CHK_AS_ASSUME
- See Also:
- Constant Field Values
CHK_AS_ASSERT
public static final int CHK_AS_ASSERT
- See Also:
- Constant Field Values
CHK_AS_SKIP
public static final int CHK_AS_SKIP
- See Also:
- Constant Field Values
FIRSTJMLKEYWORDTAG
public static final int FIRSTJMLKEYWORDTAG
- See Also:
- Constant Field Values
ASSUME
public static final int ASSUME
- See Also:
- Constant Field Values
AXIOM
public static final int AXIOM
- See Also:
- Constant Field Values
CODE_CONTRACT
public static final int CODE_CONTRACT
- See Also:
- Constant Field Values
DECREASES
public static final int DECREASES
- See Also:
- Constant Field Values
DTTFSA
public static final int DTTFSA
- See Also:
- Constant Field Values
ENSURES
public static final int ENSURES
- See Also:
- Constant Field Values
ELEMSNONNULL
public static final int ELEMSNONNULL
- See Also:
- Constant Field Values
ELEMTYPE
public static final int ELEMTYPE
- See Also:
- Constant Field Values
EXISTS
public static final int EXISTS
- See Also:
- Constant Field Values
EXSURES
public static final int EXSURES
- See Also:
- Constant Field Values
FRESH
public static final int FRESH
- See Also:
- Constant Field Values
FORALL
public static final int FORALL
- See Also:
- Constant Field Values
FUNCTION
public static final int FUNCTION
- See Also:
- Constant Field Values
GHOST
public static final int GHOST
- See Also:
- Constant Field Values
HELPER
public static final int HELPER
- See Also:
- Constant Field Values
IMMUTABLE
public static final int IMMUTABLE
- See Also:
- Constant Field Values
IN
public static final int IN
- See Also:
- Constant Field Values
IN_REDUNDANTLY
public static final int IN_REDUNDANTLY
- See Also:
- Constant Field Values
INTO
public static final int INTO
- See Also:
- Constant Field Values
INVARIANT
public static final int INVARIANT
- See Also:
- Constant Field Values
LBLPOS
public static final int LBLPOS
- See Also:
- Constant Field Values
LBLNEG
public static final int LBLNEG
- See Also:
- Constant Field Values
LOOP_INVARIANT
public static final int LOOP_INVARIANT
- See Also:
- Constant Field Values
LOOP_PREDICATE
public static final int LOOP_PREDICATE
- See Also:
- Constant Field Values
LS
public static final int LS
- See Also:
- Constant Field Values
MAPS
public static final int MAPS
- See Also:
- Constant Field Values
MAPS_REDUNDANTLY
public static final int MAPS_REDUNDANTLY
- See Also:
- Constant Field Values
MAX
public static final int MAX
- See Also:
- Constant Field Values
MODIFIES
public static final int MODIFIES
- See Also:
- Constant Field Values
MONITORED
public static final int MONITORED
- See Also:
- Constant Field Values
MONITORED_BY
public static final int MONITORED_BY
- See Also:
- Constant Field Values
MONITORS_FOR
public static final int MONITORS_FOR
- See Also:
- Constant Field Values
NON_NULL
public static final int NON_NULL
- See Also:
- Constant Field Values
NOWARN
public static final int NOWARN
- See Also:
- Constant Field Values
PRE
public static final int PRE
- See Also:
- Constant Field Values
READABLE
public static final int READABLE
- See Also:
- Constant Field Values
READABLE_IF
public static final int READABLE_IF
- See Also:
- Constant Field Values
RES
public static final int RES
- See Also:
- Constant Field Values
REQUIRES
public static final int REQUIRES
- See Also:
- Constant Field Values
SET
public static final int SET
- See Also:
- Constant Field Values
SPEC_PUBLIC
public static final int SPEC_PUBLIC
- See Also:
- Constant Field Values
STILL_DEFERRED
public static final int STILL_DEFERRED
- See Also:
- Constant Field Values
TYPE
public static final int TYPE
- See Also:
- Constant Field Values
TYPETYPE
public static final int TYPETYPE
- See Also:
- Constant Field Values
TYPEOF
public static final int TYPEOF
- See Also:
- Constant Field Values
UNINITIALIZED
public static final int UNINITIALIZED
- See Also:
- Constant Field Values
UNREACHABLE
public static final int UNREACHABLE
- See Also:
- Constant Field Values
WRITABLE_DEFERRED
public static final int WRITABLE_DEFERRED
- See Also:
- Constant Field Values
WRITABLE_IF
public static final int WRITABLE_IF
- See Also:
- Constant Field Values
WRITABLE
public static final int WRITABLE
- See Also:
- Constant Field Values
SKOLEM_CONSTANT
public static final int SKOLEM_CONSTANT
- See Also:
- Constant Field Values
BIGINT
public static final int BIGINT
- See Also:
- Constant Field Values
WACK_DURATION
public static final int WACK_DURATION
- See Also:
- Constant Field Values
EVERYTHING
public static final int EVERYTHING
- See Also:
- Constant Field Values
FIELDS_OF
public static final int FIELDS_OF
- See Also:
- Constant Field Values
INVARIANT_FOR
public static final int INVARIANT_FOR
- See Also:
- Constant Field Values
IS_INITIALIZED
public static final int IS_INITIALIZED
- See Also:
- Constant Field Values
MAXQUANT
public static final int MAXQUANT
- See Also:
- Constant Field Values
MIN
public static final int MIN
- See Also:
- Constant Field Values
NOTHING
public static final int NOTHING
- See Also:
- Constant Field Values
NOT_MODIFIED
public static final int NOT_MODIFIED
- See Also:
- Constant Field Values
NOT_SPECIFIED
public static final int NOT_SPECIFIED
- See Also:
- Constant Field Values
WACK_NOWARN
public static final int WACK_NOWARN
- See Also:
- Constant Field Values
NOWARN_OP
public static final int NOWARN_OP
- See Also:
- Constant Field Values
NUM_OF
public static final int NUM_OF
- See Also:
- Constant Field Values
OTHER
public static final int OTHER
- See Also:
- Constant Field Values
PRIVATE_DATA
public static final int PRIVATE_DATA
- See Also:
- Constant Field Values
PRODUCT
public static final int PRODUCT
- See Also:
- Constant Field Values
REACH
public static final int REACH
- See Also:
- Constant Field Values
REAL
public static final int REAL
- See Also:
- Constant Field Values
SPACE
public static final int SPACE
- See Also:
- Constant Field Values
SUCH_THAT
public static final int SUCH_THAT
- See Also:
- Constant Field Values
SUM
public static final int SUM
- See Also:
- Constant Field Values
WARN
public static final int WARN
- See Also:
- Constant Field Values
WARN_OP
public static final int WARN_OP
- See Also:
- Constant Field Values
WACK_WORKING_SPACE
public static final int WACK_WORKING_SPACE
- See Also:
- Constant Field Values
ABRUPT_BEHAVIOR
public static final int ABRUPT_BEHAVIOR
- See Also:
- Constant Field Values
ACCESSIBLE_REDUNDANTLY
public static final int ACCESSIBLE_REDUNDANTLY
- See Also:
- Constant Field Values
ACCESSIBLE
public static final int ACCESSIBLE
- See Also:
- Constant Field Values
ALSO
public static final int ALSO
- See Also:
- Constant Field Values
ALSO_REFINE
public static final int ALSO_REFINE
- See Also:
- Constant Field Values
ASSERT_REDUNDANTLY
public static final int ASSERT_REDUNDANTLY
- See Also:
- Constant Field Values
ASSIGNABLE_REDUNDANTLY
public static final int ASSIGNABLE_REDUNDANTLY
- See Also:
- Constant Field Values
ASSIGNABLE
public static final int ASSIGNABLE
- See Also:
- Constant Field Values
ASSUME_REDUNDANTLY
public static final int ASSUME_REDUNDANTLY
- See Also:
- Constant Field Values
BEHAVIOR
public static final int BEHAVIOR
- See Also:
- Constant Field Values
BREAKS_REDUNDANTLY
public static final int BREAKS_REDUNDANTLY
- See Also:
- Constant Field Values
BREAKS
public static final int BREAKS
- See Also:
- Constant Field Values
CALLABLE_REDUNDANTLY
public static final int CALLABLE_REDUNDANTLY
- See Also:
- Constant Field Values
CALLABLE
public static final int CALLABLE
- See Also:
- Constant Field Values
CHOOSE_IF
public static final int CHOOSE_IF
- See Also:
- Constant Field Values
CHOOSE
public static final int CHOOSE
- See Also:
- Constant Field Values
CONSTRAINT_REDUNDANTLY
public static final int CONSTRAINT_REDUNDANTLY
- See Also:
- Constant Field Values
CONSTRAINT
public static final int CONSTRAINT
- See Also:
- Constant Field Values
CONSTRUCTOR
public static final int CONSTRUCTOR
- See Also:
- Constant Field Values
CONTINUES_REDUNDANTLY
public static final int CONTINUES_REDUNDANTLY
- See Also:
- Constant Field Values
CONTINUES
public static final int CONTINUES
- See Also:
- Constant Field Values
DECREASES_REDUNDANTLY
public static final int DECREASES_REDUNDANTLY
- See Also:
- Constant Field Values
DECREASING_REDUNDANTLY
public static final int DECREASING_REDUNDANTLY
- See Also:
- Constant Field Values
DECREASING
public static final int DECREASING
- See Also:
- Constant Field Values
DEPENDS_REDUNDANTLY
public static final int DEPENDS_REDUNDANTLY
- See Also:
- Constant Field Values
DEPENDS
public static final int DEPENDS
- See Also:
- Constant Field Values
DIVERGES_REDUNDANTLY
public static final int DIVERGES_REDUNDANTLY
- See Also:
- Constant Field Values
DIVERGES
public static final int DIVERGES
- See Also:
- Constant Field Values
DURATION_REDUNDANTLY
public static final int DURATION_REDUNDANTLY
- See Also:
- Constant Field Values
DURATION
public static final int DURATION
- See Also:
- Constant Field Values
END
public static final int END
- See Also:
- Constant Field Values
ENSURES_REDUNDANTLY
public static final int ENSURES_REDUNDANTLY
- See Also:
- Constant Field Values
EXAMPLE
public static final int EXAMPLE
- See Also:
- Constant Field Values
EXCEPTIONAL_BEHAVIOR
public static final int EXCEPTIONAL_BEHAVIOR
- See Also:
- Constant Field Values
EXCEPTIONAL_EXAMPLE
public static final int EXCEPTIONAL_EXAMPLE
- See Also:
- Constant Field Values
EXSURES_REDUNDANTLY
public static final int EXSURES_REDUNDANTLY
- See Also:
- Constant Field Values
FIELDKW
public static final int FIELDKW
- See Also:
- Constant Field Values
NO_WACK_FORALL
public static final int NO_WACK_FORALL
- See Also:
- Constant Field Values
FOR_EXAMPLE
public static final int FOR_EXAMPLE
- See Also:
- Constant Field Values
IMPLIES_THAT
public static final int IMPLIES_THAT
- See Also:
- Constant Field Values
HENCE_BY_REDUNDANTLY
public static final int HENCE_BY_REDUNDANTLY
- See Also:
- Constant Field Values
HENCE_BY
public static final int HENCE_BY
- See Also:
- Constant Field Values
INITIALIZER
public static final int INITIALIZER
- See Also:
- Constant Field Values
INITIALLY
public static final int INITIALLY
- See Also:
- Constant Field Values
INSTANCE
public static final int INSTANCE
- See Also:
- Constant Field Values
INVARIANT_REDUNDANTLY
public static final int INVARIANT_REDUNDANTLY
- See Also:
- Constant Field Values
LOOP_INVARIANT_REDUNDANTLY
public static final int LOOP_INVARIANT_REDUNDANTLY
- See Also:
- Constant Field Values
MAINTAINING_REDUNDANTLY
public static final int MAINTAINING_REDUNDANTLY
- See Also:
- Constant Field Values
MAINTAINING
public static final int MAINTAINING
- See Also:
- Constant Field Values
MEASURED_BY_REDUNDANTLY
public static final int MEASURED_BY_REDUNDANTLY
- See Also:
- Constant Field Values
MEASURED_BY
public static final int MEASURED_BY
- See Also:
- Constant Field Values
METHOD
public static final int METHOD
- See Also:
- Constant Field Values
MODEL
public static final int MODEL
- See Also:
- Constant Field Values
MODEL_PROGRAM
public static final int MODEL_PROGRAM
- See Also:
- Constant Field Values
MODIFIABLE_REDUNDANTLY
public static final int MODIFIABLE_REDUNDANTLY
- See Also:
- Constant Field Values
MODIFIABLE
public static final int MODIFIABLE
- See Also:
- Constant Field Values
MODIFIES_REDUNDANTLY
public static final int MODIFIES_REDUNDANTLY
- See Also:
- Constant Field Values
NESTEDMODIFIERPRAGMA
public static final int NESTEDMODIFIERPRAGMA
- See Also:
- Constant Field Values
NORMAL_BEHAVIOR
public static final int NORMAL_BEHAVIOR
- See Also:
- Constant Field Values
NORMAL_EXAMPLE
public static final int NORMAL_EXAMPLE
- See Also:
- Constant Field Values
OLD
public static final int OLD
- See Also:
- Constant Field Values
MODELPROGRAM_OR
public static final int MODELPROGRAM_OR
- See Also:
- Constant Field Values
PARSEDSPECS
public static final int PARSEDSPECS
- See Also:
- Constant Field Values
POSTCONDITION_REDUNDANTLY
public static final int POSTCONDITION_REDUNDANTLY
- See Also:
- Constant Field Values
POSTCONDITION
public static final int POSTCONDITION
- See Also:
- Constant Field Values
PRECONDITION_REDUNDANTLY
public static final int PRECONDITION_REDUNDANTLY
- See Also:
- Constant Field Values
PRECONDITION
public static final int PRECONDITION
- See Also:
- Constant Field Values
PURE
public static final int PURE
- See Also:
- Constant Field Values
REFINE
public static final int REFINE
- See Also:
- Constant Field Values
REPRESENTS_REDUNDANTLY
public static final int REPRESENTS_REDUNDANTLY
- See Also:
- Constant Field Values
REPRESENTS
public static final int REPRESENTS
- See Also:
- Constant Field Values
REQUIRES_REDUNDANTLY
public static final int REQUIRES_REDUNDANTLY
- See Also:
- Constant Field Values
RETURNS_REDUNDANTLY
public static final int RETURNS_REDUNDANTLY
- See Also:
- Constant Field Values
RETURNS
public static final int RETURNS
- See Also:
- Constant Field Values
SIGNALS_REDUNDANTLY
public static final int SIGNALS_REDUNDANTLY
- See Also:
- Constant Field Values
SIGNALS
public static final int SIGNALS
- See Also:
- Constant Field Values
SIGNALS_ONLY
public static final int SIGNALS_ONLY
- See Also:
- Constant Field Values
SPEC_PROTECTED
public static final int SPEC_PROTECTED
- See Also:
- Constant Field Values
STATIC_INITIALIZER
public static final int STATIC_INITIALIZER
- See Also:
- Constant Field Values
SUBCLASSING_CONTRACT
public static final int SUBCLASSING_CONTRACT
- See Also:
- Constant Field Values
WEAKLY
public static final int WEAKLY
- See Also:
- Constant Field Values
WHEN_REDUNDANTLY
public static final int WHEN_REDUNDANTLY
- See Also:
- Constant Field Values
WHEN
public static final int WHEN
- See Also:
- Constant Field Values
WORKING_SPACE_REDUNDANTLY
public static final int WORKING_SPACE_REDUNDANTLY
- See Also:
- Constant Field Values
WORKING_SPACE
public static final int WORKING_SPACE
- See Also:
- Constant Field Values
LASTJMLKEYWORDTAG
public static final int LASTJMLKEYWORDTAG
- See Also:
- Constant Field Values
FIRSTESCKEYWORDTAG
public static final int FIRSTESCKEYWORDTAG
- See Also:
- Constant Field Values
ALSO_ENSURES
public static final int ALSO_ENSURES
- See Also:
- Constant Field Values
ALSO_EXSURES
public static final int ALSO_EXSURES
- See Also:
- Constant Field Values
ALSO_MODIFIES
public static final int ALSO_MODIFIES
- See Also:
- Constant Field Values
ALSO_REQUIRES
public static final int ALSO_REQUIRES
- See Also:
- Constant Field Values
PEER
public static final int PEER
- See Also:
- Constant Field Values
READONLY
public static final int READONLY
- See Also:
- Constant Field Values
REP
public static final int REP
- See Also:
- Constant Field Values
MAY_BE_NULL
public static final int MAY_BE_NULL
- See Also:
- Constant Field Values
NULL_REF_BY_DEFAULT
public static final int NULL_REF_BY_DEFAULT
- See Also:
- Constant Field Values
NON_NULL_REF_BY_DEFAULT
public static final int NON_NULL_REF_BY_DEFAULT
- See Also:
- Constant Field Values
OBS_PURE
public static final int OBS_PURE
- See Also:
- Constant Field Values
WACK_JAVA_MATH
public static final int WACK_JAVA_MATH
- See Also:
- Constant Field Values
WACK_SAFE_MATH
public static final int WACK_SAFE_MATH
- See Also:
- Constant Field Values
WACK_BIGINT_MATH
public static final int WACK_BIGINT_MATH
- See Also:
- Constant Field Values
CODE_JAVA_MATH
public static final int CODE_JAVA_MATH
- See Also:
- Constant Field Values
CODE_SAFE_MATH
public static final int CODE_SAFE_MATH
- See Also:
- Constant Field Values
CODE_BIGINT_MATH
public static final int CODE_BIGINT_MATH
- See Also:
- Constant Field Values
SPEC_JAVA_MATH
public static final int SPEC_JAVA_MATH
- See Also:
- Constant Field Values
SPEC_SAFE_MATH
public static final int SPEC_SAFE_MATH
- See Also:
- Constant Field Values
SPEC_BIGINT_MATH
public static final int SPEC_BIGINT_MATH
- See Also:
- Constant Field Values
LASTESCKEYWORDTAG
public static final int LASTESCKEYWORDTAG
- See Also:
- Constant Field Values
LAST_TAG
public static final int LAST_TAG
- See Also:
- Constant Field Values
ExsuresIdnName
public static final Identifier ExsuresIdnName
escchecks
public static final java.lang.String[] escchecks
escfunctions
private static java.lang.String[] escfunctions
STRINGCATINFIX
public static final java.lang.String STRINGCATINFIX
- See Also:
- Constant Field Values
jmlkeywords
private static Identifier[] jmlkeywords
esckeywords
private static Identifier[] esckeywords
TagConstants
public TagConstants()
toVcString
public static java.lang.String toVcString(int tag)
toString
public static java.lang.String toString(int tag)
fromIdentifier
public static int fromIdentifier(Identifier keyword)
- Parameters:
keyword
- the keyword to lookup.
- Returns:
- the index of the
TagConstants
attribute
corresponding to the keyword encoded as an Identifier
in the parameter 'keyword'. A TagConstants.NULL
is returned if
the identifier in question is not an ESC/Java or JML keyword
known to TagConstants
.
isKeywordTag
public static boolean isKeywordTag(int tag)
checkFromString
public static int checkFromString(java.lang.String s)
makeRedundant
public static int makeRedundant(int tag)
- Returns:
- a "redundant-fied" version of the passed tag if it can
be made redundant; otherwise, return the parameter unchanged.
unRedundant
public static int unRedundant(int tag)
- Returns:
- an "unredundant-fied" version of the passed tag if it
is redundant; otherwise, return the parameter unchanged.
isRedundant
public static boolean isRedundant(int tag)
main
public static void main(java.lang.String[] args)
comp
private static void comp(int i,
int j,
java.lang.String s)
The ESC/Java2 Project Homepage