public class KeYJMLParser extends Parser
Modifier and Type | Class and Description |
---|---|
protected class |
KeYJMLParser.DFA1 |
protected class |
KeYJMLParser.DFA10 |
protected class |
KeYJMLParser.DFA11 |
protected class |
KeYJMLParser.DFA13 |
protected class |
KeYJMLParser.DFA14 |
protected class |
KeYJMLParser.DFA16 |
protected class |
KeYJMLParser.DFA17 |
protected class |
KeYJMLParser.DFA18 |
protected class |
KeYJMLParser.DFA19 |
protected class |
KeYJMLParser.DFA20 |
protected class |
KeYJMLParser.DFA22 |
protected class |
KeYJMLParser.DFA23 |
protected class |
KeYJMLParser.DFA27 |
protected class |
KeYJMLParser.DFA3 |
protected class |
KeYJMLParser.DFA31 |
protected class |
KeYJMLParser.DFA33 |
protected class |
KeYJMLParser.DFA34 |
protected class |
KeYJMLParser.DFA36 |
protected class |
KeYJMLParser.DFA39 |
protected class |
KeYJMLParser.DFA40 |
protected class |
KeYJMLParser.DFA58 |
protected class |
KeYJMLParser.DFA59 |
protected class |
KeYJMLParser.DFA6 |
protected class |
KeYJMLParser.DFA61 |
protected class |
KeYJMLParser.DFA63 |
protected class |
KeYJMLParser.DFA65 |
protected class |
KeYJMLParser.DFA68 |
protected class |
KeYJMLParser.DFA72 |
protected class |
KeYJMLParser.DFA74 |
protected class |
KeYJMLParser.DFA75 |
protected class |
KeYJMLParser.DFA79 |
protected class |
KeYJMLParser.DFA8 |
protected class |
KeYJMLParser.DFA84 |
protected class |
KeYJMLParser.DFA9 |
DEFAULT_TOKEN_CHANNEL, HIDDEN, INITIAL_FOLLOW_STACK_SIZE, MEMO_RULE_FAILED, MEMO_RULE_UNKNOWN, NEXT_TOKEN_RULE_NAME, state
Modifier | Constructor and Description |
---|---|
private |
KeYJMLParser(KeYJMLLexer lexer,
String fileName,
Services services,
KeYJavaType specInClass,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable result,
ProgramVariable exc,
Map<LocationVariable,Term> atPres) |
|
KeYJMLParser(PositionedString ps,
Services services,
KeYJavaType specInClass,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable result,
ProgramVariable exc,
Map<LocationVariable,Term> atPres) |
|
KeYJMLParser(TokenStream input) |
|
KeYJMLParser(TokenStream input,
RecognizerSharedState state) |
getCurrentInputSymbol, getMissingSymbol, getSourceName, getTokenStream, reset, setTokenStream, traceIn, traceOut
alreadyParsedRule, beginResync, combineFollows, computeContextSensitiveRuleFOLLOW, computeErrorRecoverySet, consumeUntil, consumeUntil, displayRecognitionError, emitErrorMessage, endResync, failed, getBacktrackingLevel, getErrorHeader, getErrorMessage, getNumberOfSyntaxErrors, getRuleInvocationStack, getRuleInvocationStack, getRuleMemoization, getRuleMemoizationCacheSize, getTokenErrorDisplay, match, matchAny, memoize, mismatchIsMissingToken, mismatchIsUnwantedToken, pushFollow, setBacktrackingLevel, toStrings, traceIn, traceOut
public static final String[] tokenNames
public static final int EOF
public static final int ACCESSIBLE
public static final int ALLFIELDS
public static final int ALLOBJECTS
public static final int AND
public static final int ASSIGNABLE
public static final int BACKSLASH_PREFIXED
public static final int BACKUP
public static final int BIGINT
public static final int BITWISENOT
public static final int BOOLEAN
public static final int BREAKS
public static final int BSUM
public static final int BY
public static final int BYTE
public static final int CHAR_LITERAL
public static final int COLON
public static final int COMMA
public static final int CONTINUES
public static final int DECLASSIFIES
public static final int DECREASES
public static final int DEPENDS
public static final int DETERMINES
public static final int DIGIT
public static final int DIGITS
public static final int DISJOINT
public static final int DIV
public static final int DL_ESCAPE
public static final int DOC_COMMENT
public static final int DOMAIN_IMPLIES_CREATED
public static final int DOT
public static final int DOTDOT
public static final int DURATION
public static final int ELEMTYPE
public static final int EMPTYSET
public static final int ENSURES
public static final int ENSURES_FREE
public static final int EQUAL_SINGLE
public static final int EQV_ANTIV
public static final int EQ_NEQ
public static final int ERASES
public static final int ESC
public static final int EVERYTHING
public static final int EXCEPTION
public static final int EXISTS
public static final int FALSE
public static final int FORALL
public static final int FREE
public static final int FRESH
public static final int GEQ
public static final int GT
public static final int HEXDIGIT
public static final int HEXNUMERAL
public static final int IDENT
public static final int IMPLIES
public static final int IMPLIESBACKWARD
public static final int INCLUSIVEOR
public static final int INDEX
public static final int INDEXOF
public static final int INFORMAL_DESCRIPTION
public static final int INSTANCEOF
public static final int INT
public static final int INTERSECT
public static final int INTO
public static final int INV
public static final int INVARIANT_FOR
public static final int IN_DOMAIN
public static final int IS_FINITE
public static final int IS_INITIALIZED
public static final int ITSELF
public static final int JML_IDENT
public static final int JOIN_PROC
public static final int LARROW
public static final int LBLNEG
public static final int LBLPOS
public static final int LBRACE
public static final int LBRACKET
public static final int LEQ
public static final int LETTER
public static final int LETTERORDIGIT
public static final int LOCKSET
public static final int LOCKSET_LEQ
public static final int LOCKSET_LT
public static final int LOCSET
public static final int LOGICALAND
public static final int LOGICALOR
public static final int LONG
public static final int LOOP_DETERMINES
public static final int LOOP_SEPARATES
public static final int LPAREN
public static final int LT
public static final int LT_IMPLICIT_GT_DISPATCH
public static final int MAP
public static final int MAPEMPTY
public static final int MAP_GET
public static final int MAP_OVERRIDE
public static final int MAP_REMOVE
public static final int MAP_SINGLETON
public static final int MAP_SIZE
public static final int MAP_UPDATE
public static final int MAX
public static final int MEASURED_BY
public static final int MIN
public static final int MINUS
public static final int MOD
public static final int MODEL_METHOD_AXIOM
public static final int MULT
public static final int NEW
public static final int NEWELEMSFRESH
public static final int NEW_OBJECTS
public static final int NONNULLELEMENTS
public static final int NON_NULL
public static final int NOT
public static final int NOTHING
public static final int NOT_ASSIGNED
public static final int NOT_MODIFIED
public static final int NOT_SPECIFIED
public static final int NULL
public static final int NULLABLE
public static final int NUM_OF
public static final int OLD
public static final int PERMISSION
public static final int PLUS
public static final int PRAGMA
public static final int PRE
public static final int PRODUCT
public static final int QUESTIONMARK
public static final int RBRACE
public static final int RBRACKET
public static final int REACH
public static final int REACHLOCS
public static final int REAL
public static final int REPRESENTS
public static final int REQUIRES
public static final int REQUIRES_FREE
public static final int RESULT
public static final int RETURNS
public static final int RPAREN
public static final int SAME
public static final int SEMI
public static final int SEPARATES
public static final int SEQ
public static final int SEQ2MAP
public static final int SEQCONCAT
public static final int SEQDEF
public static final int SEQEMPTY
public static final int SEQGET
public static final int SEQREPLACE
public static final int SEQREVERSE
public static final int SEQSINGLETON
public static final int SEQSUB
public static final int SETMINUS
public static final int SHIFTLEFT
public static final int SHIFTRIGHT
public static final int SHORT
public static final int SIGNALS
public static final int SIGNALS_ONLY
public static final int SINGLETON
public static final int SL_COMMENT
public static final int SPACE
public static final int ST
public static final int STATIC_INVARIANT_FOR
public static final int STRICTLY_NOTHING
public static final int STRING_EQUAL
public static final int STRING_LITERAL
public static final int SUBSET
public static final int SUCH_THAT
public static final int SUM
public static final int SUPER
public static final int THIS
public static final int TRANSACTIONUPDATED
public static final int TRANSIENT
public static final int TRUE
public static final int TYPE
public static final int TYPEOF
public static final int TYPE_SMALL
public static final int UNION
public static final int UNIONINF
public static final int UNSIGNEDSHIFTRIGHT
public static final int VALUES
public static final int VOID
public static final int WORKINGSPACE
public static final int WS
public static final int XOR
public static final int UNION_2
private TermBuilder tb
private Services services
private JavaInfo javaInfo
private KeYJavaType containerType
private IntegerLDT intLDT
private HeapLDT heapLDT
private LocSetLDT locSetLDT
private BooleanLDT booleanLDT
private SLTranslationExceptionManager excManager
private List<PositionedString> warnings
private JMLTranslator translator
private ProgramVariable selfVar
private ImmutableList<ProgramVariable> paramVars
private ProgramVariable resultVar
private ProgramVariable excVar
private Map<LocationVariable,Term> atPres
private JMLResolverManager resolverManager
private JavaIntegerSemanticsHelper intHelper
private boolean representsClauseLhsIsLocSet
protected KeYJMLParser.DFA1 dfa1
protected KeYJMLParser.DFA3 dfa3
protected KeYJMLParser.DFA6 dfa6
protected KeYJMLParser.DFA8 dfa8
protected KeYJMLParser.DFA9 dfa9
protected KeYJMLParser.DFA10 dfa10
protected KeYJMLParser.DFA11 dfa11
protected KeYJMLParser.DFA13 dfa13
protected KeYJMLParser.DFA14 dfa14
protected KeYJMLParser.DFA16 dfa16
protected KeYJMLParser.DFA17 dfa17
protected KeYJMLParser.DFA18 dfa18
protected KeYJMLParser.DFA19 dfa19
protected KeYJMLParser.DFA20 dfa20
protected KeYJMLParser.DFA22 dfa22
protected KeYJMLParser.DFA23 dfa23
protected KeYJMLParser.DFA27 dfa27
protected KeYJMLParser.DFA31 dfa31
protected KeYJMLParser.DFA33 dfa33
protected KeYJMLParser.DFA34 dfa34
protected KeYJMLParser.DFA36 dfa36
protected KeYJMLParser.DFA39 dfa39
protected KeYJMLParser.DFA40 dfa40
protected KeYJMLParser.DFA58 dfa58
protected KeYJMLParser.DFA59 dfa59
protected KeYJMLParser.DFA61 dfa61
protected KeYJMLParser.DFA63 dfa63
protected KeYJMLParser.DFA65 dfa65
protected KeYJMLParser.DFA68 dfa68
protected KeYJMLParser.DFA72 dfa72
protected KeYJMLParser.DFA74 dfa74
protected KeYJMLParser.DFA75 dfa75
protected KeYJMLParser.DFA79 dfa79
protected KeYJMLParser.DFA84 dfa84
static final String DFA1_eotS
static final String DFA1_eofS
static final String DFA1_minS
static final String DFA1_maxS
static final String DFA1_acceptS
static final String DFA1_specialS
static final String[] DFA1_transitionS
static final short[] DFA1_eot
static final short[] DFA1_eof
static final char[] DFA1_min
static final char[] DFA1_max
static final short[] DFA1_accept
static final short[] DFA1_special
static final short[][] DFA1_transition
static final String DFA3_eotS
static final String DFA3_eofS
static final String DFA3_minS
static final String DFA3_maxS
static final String DFA3_acceptS
static final String DFA3_specialS
static final String[] DFA3_transitionS
static final short[] DFA3_eot
static final short[] DFA3_eof
static final char[] DFA3_min
static final char[] DFA3_max
static final short[] DFA3_accept
static final short[] DFA3_special
static final short[][] DFA3_transition
static final String DFA6_eotS
static final String DFA6_eofS
static final String DFA6_minS
static final String DFA6_maxS
static final String DFA6_acceptS
static final String DFA6_specialS
static final String[] DFA6_transitionS
static final short[] DFA6_eot
static final short[] DFA6_eof
static final char[] DFA6_min
static final char[] DFA6_max
static final short[] DFA6_accept
static final short[] DFA6_special
static final short[][] DFA6_transition
static final String DFA8_eotS
static final String DFA8_eofS
static final String DFA8_minS
static final String DFA8_maxS
static final String DFA8_acceptS
static final String DFA8_specialS
static final String[] DFA8_transitionS
static final short[] DFA8_eot
static final short[] DFA8_eof
static final char[] DFA8_min
static final char[] DFA8_max
static final short[] DFA8_accept
static final short[] DFA8_special
static final short[][] DFA8_transition
static final String DFA9_eotS
static final String DFA9_eofS
static final String DFA9_minS
static final String DFA9_maxS
static final String DFA9_acceptS
static final String DFA9_specialS
static final String[] DFA9_transitionS
static final short[] DFA9_eot
static final short[] DFA9_eof
static final char[] DFA9_min
static final char[] DFA9_max
static final short[] DFA9_accept
static final short[] DFA9_special
static final short[][] DFA9_transition
static final String DFA10_eotS
static final String DFA10_eofS
static final String DFA10_minS
static final String DFA10_maxS
static final String DFA10_acceptS
static final String DFA10_specialS
static final String[] DFA10_transitionS
static final short[] DFA10_eot
static final short[] DFA10_eof
static final char[] DFA10_min
static final char[] DFA10_max
static final short[] DFA10_accept
static final short[] DFA10_special
static final short[][] DFA10_transition
static final String DFA11_eotS
static final String DFA11_eofS
static final String DFA11_minS
static final String DFA11_maxS
static final String DFA11_acceptS
static final String DFA11_specialS
static final String[] DFA11_transitionS
static final short[] DFA11_eot
static final short[] DFA11_eof
static final char[] DFA11_min
static final char[] DFA11_max
static final short[] DFA11_accept
static final short[] DFA11_special
static final short[][] DFA11_transition
static final String DFA13_eotS
static final String DFA13_eofS
static final String DFA13_minS
static final String DFA13_maxS
static final String DFA13_acceptS
static final String DFA13_specialS
static final String[] DFA13_transitionS
static final short[] DFA13_eot
static final short[] DFA13_eof
static final char[] DFA13_min
static final char[] DFA13_max
static final short[] DFA13_accept
static final short[] DFA13_special
static final short[][] DFA13_transition
static final String DFA14_eotS
static final String DFA14_eofS
static final String DFA14_minS
static final String DFA14_maxS
static final String DFA14_acceptS
static final String DFA14_specialS
static final String[] DFA14_transitionS
static final short[] DFA14_eot
static final short[] DFA14_eof
static final char[] DFA14_min
static final char[] DFA14_max
static final short[] DFA14_accept
static final short[] DFA14_special
static final short[][] DFA14_transition
static final String DFA16_eotS
static final String DFA16_eofS
static final String DFA16_minS
static final String DFA16_maxS
static final String DFA16_acceptS
static final String DFA16_specialS
static final String[] DFA16_transitionS
static final short[] DFA16_eot
static final short[] DFA16_eof
static final char[] DFA16_min
static final char[] DFA16_max
static final short[] DFA16_accept
static final short[] DFA16_special
static final short[][] DFA16_transition
static final String DFA17_eotS
static final String DFA17_eofS
static final String DFA17_minS
static final String DFA17_maxS
static final String DFA17_acceptS
static final String DFA17_specialS
static final String[] DFA17_transitionS
static final short[] DFA17_eot
static final short[] DFA17_eof
static final char[] DFA17_min
static final char[] DFA17_max
static final short[] DFA17_accept
static final short[] DFA17_special
static final short[][] DFA17_transition
static final String DFA18_eotS
static final String DFA18_eofS
static final String DFA18_minS
static final String DFA18_maxS
static final String DFA18_acceptS
static final String DFA18_specialS
static final String[] DFA18_transitionS
static final short[] DFA18_eot
static final short[] DFA18_eof
static final char[] DFA18_min
static final char[] DFA18_max
static final short[] DFA18_accept
static final short[] DFA18_special
static final short[][] DFA18_transition
static final String DFA19_eotS
static final String DFA19_eofS
static final String DFA19_minS
static final String DFA19_maxS
static final String DFA19_acceptS
static final String DFA19_specialS
static final String[] DFA19_transitionS
static final short[] DFA19_eot
static final short[] DFA19_eof
static final char[] DFA19_min
static final char[] DFA19_max
static final short[] DFA19_accept
static final short[] DFA19_special
static final short[][] DFA19_transition
static final String DFA20_eotS
static final String DFA20_eofS
static final String DFA20_minS
static final String DFA20_maxS
static final String DFA20_acceptS
static final String DFA20_specialS
static final String[] DFA20_transitionS
static final short[] DFA20_eot
static final short[] DFA20_eof
static final char[] DFA20_min
static final char[] DFA20_max
static final short[] DFA20_accept
static final short[] DFA20_special
static final short[][] DFA20_transition
static final String DFA22_eotS
static final String DFA22_eofS
static final String DFA22_minS
static final String DFA22_maxS
static final String DFA22_acceptS
static final String DFA22_specialS
static final String[] DFA22_transitionS
static final short[] DFA22_eot
static final short[] DFA22_eof
static final char[] DFA22_min
static final char[] DFA22_max
static final short[] DFA22_accept
static final short[] DFA22_special
static final short[][] DFA22_transition
static final String DFA23_eotS
static final String DFA23_eofS
static final String DFA23_minS
static final String DFA23_maxS
static final String DFA23_acceptS
static final String DFA23_specialS
static final String[] DFA23_transitionS
static final short[] DFA23_eot
static final short[] DFA23_eof
static final char[] DFA23_min
static final char[] DFA23_max
static final short[] DFA23_accept
static final short[] DFA23_special
static final short[][] DFA23_transition
static final String DFA27_eotS
static final String DFA27_eofS
static final String DFA27_minS
static final String DFA27_maxS
static final String DFA27_acceptS
static final String DFA27_specialS
static final String[] DFA27_transitionS
static final short[] DFA27_eot
static final short[] DFA27_eof
static final char[] DFA27_min
static final char[] DFA27_max
static final short[] DFA27_accept
static final short[] DFA27_special
static final short[][] DFA27_transition
static final String DFA31_eotS
static final String DFA31_eofS
static final String DFA31_minS
static final String DFA31_maxS
static final String DFA31_acceptS
static final String DFA31_specialS
static final String[] DFA31_transitionS
static final short[] DFA31_eot
static final short[] DFA31_eof
static final char[] DFA31_min
static final char[] DFA31_max
static final short[] DFA31_accept
static final short[] DFA31_special
static final short[][] DFA31_transition
static final String DFA33_eotS
static final String DFA33_eofS
static final String DFA33_minS
static final String DFA33_maxS
static final String DFA33_acceptS
static final String DFA33_specialS
static final String[] DFA33_transitionS
static final short[] DFA33_eot
static final short[] DFA33_eof
static final char[] DFA33_min
static final char[] DFA33_max
static final short[] DFA33_accept
static final short[] DFA33_special
static final short[][] DFA33_transition
static final String DFA34_eotS
static final String DFA34_eofS
static final String DFA34_minS
static final String DFA34_maxS
static final String DFA34_acceptS
static final String DFA34_specialS
static final String[] DFA34_transitionS
static final short[] DFA34_eot
static final short[] DFA34_eof
static final char[] DFA34_min
static final char[] DFA34_max
static final short[] DFA34_accept
static final short[] DFA34_special
static final short[][] DFA34_transition
static final String DFA36_eotS
static final String DFA36_eofS
static final String DFA36_minS
static final String DFA36_maxS
static final String DFA36_acceptS
static final String DFA36_specialS
static final String[] DFA36_transitionS
static final short[] DFA36_eot
static final short[] DFA36_eof
static final char[] DFA36_min
static final char[] DFA36_max
static final short[] DFA36_accept
static final short[] DFA36_special
static final short[][] DFA36_transition
static final String DFA39_eotS
static final String DFA39_eofS
static final String DFA39_minS
static final String DFA39_maxS
static final String DFA39_acceptS
static final String DFA39_specialS
static final String[] DFA39_transitionS
static final short[] DFA39_eot
static final short[] DFA39_eof
static final char[] DFA39_min
static final char[] DFA39_max
static final short[] DFA39_accept
static final short[] DFA39_special
static final short[][] DFA39_transition
static final String DFA40_eotS
static final String DFA40_eofS
static final String DFA40_minS
static final String DFA40_maxS
static final String DFA40_acceptS
static final String DFA40_specialS
static final String[] DFA40_transitionS
static final short[] DFA40_eot
static final short[] DFA40_eof
static final char[] DFA40_min
static final char[] DFA40_max
static final short[] DFA40_accept
static final short[] DFA40_special
static final short[][] DFA40_transition
static final String DFA58_eotS
static final String DFA58_eofS
static final String DFA58_minS
static final String DFA58_maxS
static final String DFA58_acceptS
static final String DFA58_specialS
static final String[] DFA58_transitionS
static final short[] DFA58_eot
static final short[] DFA58_eof
static final char[] DFA58_min
static final char[] DFA58_max
static final short[] DFA58_accept
static final short[] DFA58_special
static final short[][] DFA58_transition
static final String DFA59_eotS
static final String DFA59_eofS
static final String DFA59_minS
static final String DFA59_maxS
static final String DFA59_acceptS
static final String DFA59_specialS
static final String[] DFA59_transitionS
static final short[] DFA59_eot
static final short[] DFA59_eof
static final char[] DFA59_min
static final char[] DFA59_max
static final short[] DFA59_accept
static final short[] DFA59_special
static final short[][] DFA59_transition
static final String DFA61_eotS
static final String DFA61_eofS
static final String DFA61_minS
static final String DFA61_maxS
static final String DFA61_acceptS
static final String DFA61_specialS
static final String[] DFA61_transitionS
static final short[] DFA61_eot
static final short[] DFA61_eof
static final char[] DFA61_min
static final char[] DFA61_max
static final short[] DFA61_accept
static final short[] DFA61_special
static final short[][] DFA61_transition
static final String DFA63_eotS
static final String DFA63_eofS
static final String DFA63_minS
static final String DFA63_maxS
static final String DFA63_acceptS
static final String DFA63_specialS
static final String[] DFA63_transitionS
static final short[] DFA63_eot
static final short[] DFA63_eof
static final char[] DFA63_min
static final char[] DFA63_max
static final short[] DFA63_accept
static final short[] DFA63_special
static final short[][] DFA63_transition
static final String DFA65_eotS
static final String DFA65_eofS
static final String DFA65_minS
static final String DFA65_maxS
static final String DFA65_acceptS
static final String DFA65_specialS
static final String[] DFA65_transitionS
static final short[] DFA65_eot
static final short[] DFA65_eof
static final char[] DFA65_min
static final char[] DFA65_max
static final short[] DFA65_accept
static final short[] DFA65_special
static final short[][] DFA65_transition
static final String DFA68_eotS
static final String DFA68_eofS
static final String DFA68_minS
static final String DFA68_maxS
static final String DFA68_acceptS
static final String DFA68_specialS
static final String[] DFA68_transitionS
static final short[] DFA68_eot
static final short[] DFA68_eof
static final char[] DFA68_min
static final char[] DFA68_max
static final short[] DFA68_accept
static final short[] DFA68_special
static final short[][] DFA68_transition
static final String DFA72_eotS
static final String DFA72_eofS
static final String DFA72_minS
static final String DFA72_maxS
static final String DFA72_acceptS
static final String DFA72_specialS
static final String[] DFA72_transitionS
static final short[] DFA72_eot
static final short[] DFA72_eof
static final char[] DFA72_min
static final char[] DFA72_max
static final short[] DFA72_accept
static final short[] DFA72_special
static final short[][] DFA72_transition
static final String DFA74_eotS
static final String DFA74_eofS
static final String DFA74_minS
static final String DFA74_maxS
static final String DFA74_acceptS
static final String DFA74_specialS
static final String[] DFA74_transitionS
static final short[] DFA74_eot
static final short[] DFA74_eof
static final char[] DFA74_min
static final char[] DFA74_max
static final short[] DFA74_accept
static final short[] DFA74_special
static final short[][] DFA74_transition
static final String DFA75_eotS
static final String DFA75_eofS
static final String DFA75_minS
static final String DFA75_maxS
static final String DFA75_acceptS
static final String DFA75_specialS
static final String[] DFA75_transitionS
static final short[] DFA75_eot
static final short[] DFA75_eof
static final char[] DFA75_min
static final char[] DFA75_max
static final short[] DFA75_accept
static final short[] DFA75_special
static final short[][] DFA75_transition
static final String DFA79_eotS
static final String DFA79_eofS
static final String DFA79_minS
static final String DFA79_maxS
static final String DFA79_acceptS
static final String DFA79_specialS
static final String[] DFA79_transitionS
static final short[] DFA79_eot
static final short[] DFA79_eof
static final char[] DFA79_min
static final char[] DFA79_max
static final short[] DFA79_accept
static final short[] DFA79_special
static final short[][] DFA79_transition
static final String DFA84_eotS
static final String DFA84_eofS
static final String DFA84_minS
static final String DFA84_maxS
static final String DFA84_acceptS
static final String DFA84_specialS
static final String[] DFA84_transitionS
static final short[] DFA84_eot
static final short[] DFA84_eof
static final char[] DFA84_min
static final char[] DFA84_max
static final short[] DFA84_accept
static final short[] DFA84_special
static final short[][] DFA84_transition
public static final BitSet FOLLOW_accessibleclause_in_top74
public static final BitSet FOLLOW_assignableclause_in_top86
public static final BitSet FOLLOW_breaksclause_in_top98
public static final BitSet FOLLOW_continuesclause_in_top110
public static final BitSet FOLLOW_dependsclause_in_top122
public static final BitSet FOLLOW_ensuresclause_in_top134
public static final BitSet FOLLOW_ensuresfreeclause_in_top146
public static final BitSet FOLLOW_representsclause_in_top158
public static final BitSet FOLLOW_axiomsclause_in_top170
public static final BitSet FOLLOW_requiresclause_in_top182
public static final BitSet FOLLOW_joinprocclause_in_top194
public static final BitSet FOLLOW_requiresfreeclause_in_top206
public static final BitSet FOLLOW_decreasesclause_in_top218
public static final BitSet FOLLOW_separatesclause_in_top230
public static final BitSet FOLLOW_determinesclause_in_top243
public static final BitSet FOLLOW_loopseparatesclause_in_top256
public static final BitSet FOLLOW_loopdeterminesclause_in_top269
public static final BitSet FOLLOW_returnsclause_in_top282
public static final BitSet FOLLOW_signalsclause_in_top294
public static final BitSet FOLLOW_signalsonlyclause_in_top306
public static final BitSet FOLLOW_termexpression_in_top318
public static final BitSet FOLLOW_SEMI_in_top333
public static final BitSet FOLLOW_EOF_in_top337
public static final BitSet FOLLOW_ACCESSIBLE_in_accessibleclause368
public static final BitSet FOLLOW_storeRefUnion_in_accessibleclause372
public static final BitSet FOLLOW_ASSIGNABLE_in_assignableclause414
public static final BitSet FOLLOW_storeRefUnion_in_assignableclause424
public static final BitSet FOLLOW_STRICTLY_NOTHING_in_assignableclause442
public static final BitSet FOLLOW_DEPENDS_in_dependsclause486
public static final BitSet FOLLOW_expression_in_dependsclause490
public static final BitSet FOLLOW_COLON_in_dependsclause496
public static final BitSet FOLLOW_storeRefUnion_in_dependsclause500
public static final BitSet FOLLOW_MEASURED_BY_in_dependsclause507
public static final BitSet FOLLOW_expression_in_dependsclause511
public static final BitSet FOLLOW_SEMI_in_dependsclause515
public static final BitSet FOLLOW_DECREASES_in_decreasesclause556
public static final BitSet FOLLOW_termexpression_in_decreasesclause560
public static final BitSet FOLLOW_COMMA_in_decreasesclause571
public static final BitSet FOLLOW_termexpression_in_decreasesclause575
public static final BitSet FOLLOW_REQUIRES_in_requiresclause607
public static final BitSet FOLLOW_predornot_in_requiresclause611
public static final BitSet FOLLOW_REQUIRES_FREE_in_requiresfreeclause652
public static final BitSet FOLLOW_predornot_in_requiresfreeclause656
public static final BitSet FOLLOW_JOIN_PROC_in_joinprocclause697
public static final BitSet FOLLOW_predornot_in_joinprocclause701
public static final BitSet FOLLOW_ENSURES_in_ensuresclause742
public static final BitSet FOLLOW_predornot_in_ensuresclause746
public static final BitSet FOLLOW_ENSURES_FREE_in_ensuresfreeclause787
public static final BitSet FOLLOW_predornot_in_ensuresfreeclause791
public static final BitSet FOLLOW_MODEL_METHOD_AXIOM_in_axiomsclause832
public static final BitSet FOLLOW_termexpression_in_axiomsclause836
public static final BitSet FOLLOW_REPRESENTS_in_representsclause877
public static final BitSet FOLLOW_expression_in_representsclause881
public static final BitSet FOLLOW_set_in_representsclause915
public static final BitSet FOLLOW_expression_in_representsclause958
public static final BitSet FOLLOW_storeRefUnion_in_representsclause998
public static final BitSet FOLLOW_SUCH_THAT_in_representsclause1057
public static final BitSet FOLLOW_predicate_in_representsclause1061
public static final BitSet FOLLOW_SEPARATES_in_separatesclause1115
public static final BitSet FOLLOW_NOTHING_in_separatesclause1118
public static final BitSet FOLLOW_infflowspeclist_in_separatesclause1126
public static final BitSet FOLLOW_DECLASSIFIES_in_separatesclause1138
public static final BitSet FOLLOW_NOTHING_in_separatesclause1141
public static final BitSet FOLLOW_infflowspeclist_in_separatesclause1149
public static final BitSet FOLLOW_ERASES_in_separatesclause1166
public static final BitSet FOLLOW_NOTHING_in_separatesclause1169
public static final BitSet FOLLOW_infflowspeclist_in_separatesclause1177
public static final BitSet FOLLOW_NEW_OBJECTS_in_separatesclause1194
public static final BitSet FOLLOW_NOTHING_in_separatesclause1197
public static final BitSet FOLLOW_infflowspeclist_in_separatesclause1205
public static final BitSet FOLLOW_LOOP_SEPARATES_in_loopseparatesclause1254
public static final BitSet FOLLOW_NOTHING_in_loopseparatesclause1257
public static final BitSet FOLLOW_infflowspeclist_in_loopseparatesclause1265
public static final BitSet FOLLOW_NEW_OBJECTS_in_loopseparatesclause1279
public static final BitSet FOLLOW_NOTHING_in_loopseparatesclause1282
public static final BitSet FOLLOW_infflowspeclist_in_loopseparatesclause1290
public static final BitSet FOLLOW_DETERMINES_in_determinesclause1339
public static final BitSet FOLLOW_NOTHING_in_determinesclause1342
public static final BitSet FOLLOW_infflowspeclist_in_determinesclause1352
public static final BitSet FOLLOW_BY_in_determinesclause1359
public static final BitSet FOLLOW_NOTHING_in_determinesclause1362
public static final BitSet FOLLOW_ITSELF_in_determinesclause1369
public static final BitSet FOLLOW_infflowspeclist_in_determinesclause1380
public static final BitSet FOLLOW_DECLASSIFIES_in_determinesclause1392
public static final BitSet FOLLOW_NOTHING_in_determinesclause1395
public static final BitSet FOLLOW_infflowspeclist_in_determinesclause1403
public static final BitSet FOLLOW_ERASES_in_determinesclause1420
public static final BitSet FOLLOW_NOTHING_in_determinesclause1423
public static final BitSet FOLLOW_infflowspeclist_in_determinesclause1431
public static final BitSet FOLLOW_NEW_OBJECTS_in_determinesclause1448
public static final BitSet FOLLOW_NOTHING_in_determinesclause1451
public static final BitSet FOLLOW_infflowspeclist_in_determinesclause1459
public static final BitSet FOLLOW_LOOP_DETERMINES_in_loopdeterminesclause1508
public static final BitSet FOLLOW_NOTHING_in_loopdeterminesclause1511
public static final BitSet FOLLOW_infflowspeclist_in_loopdeterminesclause1519
public static final BitSet FOLLOW_BY_in_loopdeterminesclause1526
public static final BitSet FOLLOW_ITSELF_in_loopdeterminesclause1528
public static final BitSet FOLLOW_NEW_OBJECTS_in_loopdeterminesclause1539
public static final BitSet FOLLOW_NOTHING_in_loopdeterminesclause1542
public static final BitSet FOLLOW_infflowspeclist_in_loopdeterminesclause1550
public static final BitSet FOLLOW_termexpression_in_infflowspeclist1598
public static final BitSet FOLLOW_COMMA_in_infflowspeclist1607
public static final BitSet FOLLOW_termexpression_in_infflowspeclist1613
public static final BitSet FOLLOW_SIGNALS_in_signalsclause1661
public static final BitSet FOLLOW_LPAREN_in_signalsclause1663
public static final BitSet FOLLOW_referencetype_in_signalsclause1667
public static final BitSet FOLLOW_IDENT_in_signalsclause1672
public static final BitSet FOLLOW_RPAREN_in_signalsclause1678
public static final BitSet FOLLOW_predornot_in_signalsclause1689
public static final BitSet FOLLOW_SIGNALS_ONLY_in_signalsonlyclause1727
public static final BitSet FOLLOW_NOTHING_in_signalsonlyclause1737
public static final BitSet FOLLOW_referencetype_in_signalsonlyclause1751
public static final BitSet FOLLOW_COMMA_in_signalsonlyclause1764
public static final BitSet FOLLOW_referencetype_in_signalsonlyclause1770
public static final BitSet FOLLOW_expression_in_termexpression1814
public static final BitSet FOLLOW_BREAKS_in_breaksclause1846
public static final BitSet FOLLOW_LPAREN_in_breaksclause1848
public static final BitSet FOLLOW_IDENT_in_breaksclause1853
public static final BitSet FOLLOW_RPAREN_in_breaksclause1859
public static final BitSet FOLLOW_predornot_in_breaksclause1867
public static final BitSet FOLLOW_CONTINUES_in_continuesclause1898
public static final BitSet FOLLOW_LPAREN_in_continuesclause1900
public static final BitSet FOLLOW_IDENT_in_continuesclause1905
public static final BitSet FOLLOW_RPAREN_in_continuesclause1911
public static final BitSet FOLLOW_predornot_in_continuesclause1919
public static final BitSet FOLLOW_RETURNS_in_returnsclause1950
public static final BitSet FOLLOW_predornot_in_returnsclause1958
public static final BitSet FOLLOW_storeRefList_in_storeRefUnion1991
public static final BitSet FOLLOW_storeref_in_storeRefList2020
public static final BitSet FOLLOW_COMMA_in_storeRefList2026
public static final BitSet FOLLOW_storeref_in_storeRefList2032
public static final BitSet FOLLOW_storeRefList_in_storeRefIntersect2061
public static final BitSet FOLLOW_NOTHING_in_storeref2090
public static final BitSet FOLLOW_EVERYTHING_in_storeref2102
public static final BitSet FOLLOW_NOT_SPECIFIED_in_storeref2114
public static final BitSet FOLLOW_storeRefExpr_in_storeref2130
public static final BitSet FOLLOW_set_in_createLocset2151
public static final BitSet FOLLOW_LPAREN_in_createLocset2159
public static final BitSet FOLLOW_exprList_in_createLocset2163
public static final BitSet FOLLOW_RPAREN_in_createLocset2165
public static final BitSet FOLLOW_expression_in_exprList2199
public static final BitSet FOLLOW_COMMA_in_exprList2205
public static final BitSet FOLLOW_expression_in_exprList2211
public static final BitSet FOLLOW_expression_in_storeRefExpr2239
public static final BitSet FOLLOW_expression_in_specarrayrefexpr2309
public static final BitSet FOLLOW_DOTDOT_in_specarrayrefexpr2312
public static final BitSet FOLLOW_expression_in_specarrayrefexpr2316
public static final BitSet FOLLOW_MULT_in_specarrayrefexpr2325
public static final BitSet FOLLOW_predicate_in_predornot2362
public static final BitSet FOLLOW_NOT_SPECIFIED_in_predornot2374
public static final BitSet FOLLOW_SAME_in_predornot2394
public static final BitSet FOLLOW_expression_in_predicate2418
public static final BitSet FOLLOW_conditionalexpr_in_expression2446
public static final BitSet FOLLOW_equivalenceexpr_in_conditionalexpr2477
public static final BitSet FOLLOW_QUESTIONMARK_in_conditionalexpr2487
public static final BitSet FOLLOW_conditionalexpr_in_conditionalexpr2491
public static final BitSet FOLLOW_COLON_in_conditionalexpr2493
public static final BitSet FOLLOW_conditionalexpr_in_conditionalexpr2497
public static final BitSet FOLLOW_impliesexpr_in_equivalenceexpr2539
public static final BitSet FOLLOW_EQV_ANTIV_in_equivalenceexpr2555
public static final BitSet FOLLOW_impliesexpr_in_equivalenceexpr2559
public static final BitSet FOLLOW_logicalorexpr_in_impliesexpr2614
public static final BitSet FOLLOW_IMPLIES_in_impliesexpr2624
public static final BitSet FOLLOW_impliesforwardexpr_in_impliesexpr2628
public static final BitSet FOLLOW_IMPLIESBACKWARD_in_impliesexpr2652
public static final BitSet FOLLOW_logicalorexpr_in_impliesexpr2656
public static final BitSet FOLLOW_logicalorexpr_in_impliesforwardexpr2696
public static final BitSet FOLLOW_IMPLIES_in_impliesforwardexpr2706
public static final BitSet FOLLOW_impliesforwardexpr_in_impliesforwardexpr2710
public static final BitSet FOLLOW_logicalandexpr_in_logicalorexpr2745
public static final BitSet FOLLOW_LOGICALOR_in_logicalorexpr2755
public static final BitSet FOLLOW_logicalandexpr_in_logicalorexpr2759
public static final BitSet FOLLOW_inclusiveorexpr_in_logicalandexpr2794
public static final BitSet FOLLOW_LOGICALAND_in_logicalandexpr2804
public static final BitSet FOLLOW_inclusiveorexpr_in_logicalandexpr2808
public static final BitSet FOLLOW_exclusiveorexpr_in_inclusiveorexpr2844
public static final BitSet FOLLOW_INCLUSIVEOR_in_inclusiveorexpr2854
public static final BitSet FOLLOW_exclusiveorexpr_in_inclusiveorexpr2858
public static final BitSet FOLLOW_andexpr_in_exclusiveorexpr2894
public static final BitSet FOLLOW_XOR_in_exclusiveorexpr2904
public static final BitSet FOLLOW_andexpr_in_exclusiveorexpr2908
public static final BitSet FOLLOW_equalityexpr_in_andexpr2944
public static final BitSet FOLLOW_AND_in_andexpr2957
public static final BitSet FOLLOW_equalityexpr_in_andexpr2961
public static final BitSet FOLLOW_relationalexpr_in_equalityexpr2998
public static final BitSet FOLLOW_EQ_NEQ_in_equalityexpr3007
public static final BitSet FOLLOW_relationalexpr_in_equalityexpr3011
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3055
public static final BitSet FOLLOW_LT_in_relationalexpr3067
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3071
public static final BitSet FOLLOW_LT_in_relationalexpr3087
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3091
public static final BitSet FOLLOW_GT_in_relationalexpr3113
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3117
public static final BitSet FOLLOW_LEQ_in_relationalexpr3136
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3140
public static final BitSet FOLLOW_LT_in_relationalexpr3155
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3159
public static final BitSet FOLLOW_GEQ_in_relationalexpr3181
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3185
public static final BitSet FOLLOW_LOCKSET_LT_in_relationalexpr3204
public static final BitSet FOLLOW_postfixexpr_in_relationalexpr3208
public static final BitSet FOLLOW_LOCKSET_LEQ_in_relationalexpr3227
public static final BitSet FOLLOW_postfixexpr_in_relationalexpr3231
public static final BitSet FOLLOW_INSTANCEOF_in_relationalexpr3250
public static final BitSet FOLLOW_typespec_in_relationalexpr3254
public static final BitSet FOLLOW_ST_in_relationalexpr3273
public static final BitSet FOLLOW_shiftexpr_in_relationalexpr3277
public static final BitSet FOLLOW_additiveexpr_in_shiftexpr3318
public static final BitSet FOLLOW_SHIFTRIGHT_in_shiftexpr3329
public static final BitSet FOLLOW_additiveexpr_in_shiftexpr3333
public static final BitSet FOLLOW_SHIFTLEFT_in_shiftexpr3347
public static final BitSet FOLLOW_additiveexpr_in_shiftexpr3351
public static final BitSet FOLLOW_UNSIGNEDSHIFTRIGHT_in_shiftexpr3365
public static final BitSet FOLLOW_additiveexpr_in_shiftexpr3369
public static final BitSet FOLLOW_multexpr_in_additiveexpr3407
public static final BitSet FOLLOW_PLUS_in_additiveexpr3418
public static final BitSet FOLLOW_multexpr_in_additiveexpr3422
public static final BitSet FOLLOW_MINUS_in_additiveexpr3436
public static final BitSet FOLLOW_multexpr_in_additiveexpr3440
public static final BitSet FOLLOW_unaryexpr_in_multexpr3479
public static final BitSet FOLLOW_MULT_in_multexpr3488
public static final BitSet FOLLOW_unaryexpr_in_multexpr3492
public static final BitSet FOLLOW_DIV_in_multexpr3504
public static final BitSet FOLLOW_unaryexpr_in_multexpr3508
public static final BitSet FOLLOW_MOD_in_multexpr3520
public static final BitSet FOLLOW_unaryexpr_in_multexpr3524
public static final BitSet FOLLOW_PLUS_in_unaryexpr3561
public static final BitSet FOLLOW_unaryexpr_in_unaryexpr3565
public static final BitSet FOLLOW_MINUS_in_unaryexpr3577
public static final BitSet FOLLOW_unaryexpr_in_unaryexpr3581
public static final BitSet FOLLOW_castexpr_in_unaryexpr3608
public static final BitSet FOLLOW_unaryexprnotplusminus_in_unaryexpr3623
public static final BitSet FOLLOW_LPAREN_in_castexpr3646
public static final BitSet FOLLOW_typespec_in_castexpr3650
public static final BitSet FOLLOW_RPAREN_in_castexpr3652
public static final BitSet FOLLOW_unaryexpr_in_castexpr3656
public static final BitSet FOLLOW_NOT_in_unaryexprnotplusminus3681
public static final BitSet FOLLOW_unaryexpr_in_unaryexprnotplusminus3685
public static final BitSet FOLLOW_BITWISENOT_in_unaryexprnotplusminus3697
public static final BitSet FOLLOW_unaryexpr_in_unaryexprnotplusminus3701
public static final BitSet FOLLOW_postfixexpr_in_unaryexprnotplusminus3716
public static final BitSet FOLLOW_primaryexpr_in_postfixexpr3747
public static final BitSet FOLLOW_primarysuffix_in_postfixexpr3769
public static final BitSet FOLLOW_constant_in_primaryexpr3817
public static final BitSet FOLLOW_IDENT_in_primaryexpr3829
public static final BitSet FOLLOW_INV_in_primaryexpr3847
public static final BitSet FOLLOW_TRUE_in_primaryexpr3864
public static final BitSet FOLLOW_FALSE_in_primaryexpr3884
public static final BitSet FOLLOW_NULL_in_primaryexpr3903
public static final BitSet FOLLOW_jmlprimary_in_primaryexpr3925
public static final BitSet FOLLOW_THIS_in_primaryexpr3935
public static final BitSet FOLLOW_new_expr_in_primaryexpr3955
public static final BitSet FOLLOW_array_initializer_in_primaryexpr3965
public static final BitSet FOLLOW_TRANSACTIONUPDATED_in_transactionUpdated3997
public static final BitSet FOLLOW_LPAREN_in_transactionUpdated3999
public static final BitSet FOLLOW_expression_in_transactionUpdated4003
public static final BitSet FOLLOW_RPAREN_in_transactionUpdated4005
public static final BitSet FOLLOW_DOT_in_primarysuffix4046
public static final BitSet FOLLOW_IDENT_in_primarysuffix4056
public static final BitSet FOLLOW_TRANSIENT_in_primarysuffix4069
public static final BitSet FOLLOW_THIS_in_primarysuffix4092
public static final BitSet FOLLOW_INV_in_primarysuffix4106
public static final BitSet FOLLOW_MULT_in_primarysuffix4120
public static final BitSet FOLLOW_LPAREN_in_primarysuffix4147
public static final BitSet FOLLOW_expressionlist_in_primarysuffix4152
public static final BitSet FOLLOW_RPAREN_in_primarysuffix4156
public static final BitSet FOLLOW_LBRACKET_in_primarysuffix4170
public static final BitSet FOLLOW_specarrayrefexpr_in_primarysuffix4174
public static final BitSet FOLLOW_RBRACKET_in_primarysuffix4177
public static final BitSet FOLLOW_NEW_in_new_expr4194
public static final BitSet FOLLOW_type_in_new_expr4198
public static final BitSet FOLLOW_LPAREN_in_new_expr4207
public static final BitSet FOLLOW_expressionlist_in_new_expr4213
public static final BitSet FOLLOW_RPAREN_in_new_expr4218
public static final BitSet FOLLOW_array_dimensions_in_new_expr4231
public static final BitSet FOLLOW_array_initializer_in_new_expr4234
public static final BitSet FOLLOW_array_dimension_in_array_dimensions4273
public static final BitSet FOLLOW_LBRACKET_in_array_dimension4295
public static final BitSet FOLLOW_expression_in_array_dimension4300
public static final BitSet FOLLOW_RBRACKET_in_array_dimension4304
public static final BitSet FOLLOW_LBRACE_in_array_initializer4321
public static final BitSet FOLLOW_expressionlist_in_array_initializer4325
public static final BitSet FOLLOW_RBRACE_in_array_initializer4327
public static final BitSet FOLLOW_expression_in_expressionlist4368
public static final BitSet FOLLOW_COMMA_in_expressionlist4373
public static final BitSet FOLLOW_expression_in_expressionlist4377
public static final BitSet FOLLOW_javaliteral_in_constant4402
public static final BitSet FOLLOW_integerliteral_in_javaliteral4428
public static final BitSet FOLLOW_STRING_LITERAL_in_javaliteral4439
public static final BitSet FOLLOW_CHAR_LITERAL_in_javaliteral4453
public static final BitSet FOLLOW_decimalintegerliteral_in_integerliteral4485
public static final BitSet FOLLOW_hexintegerliteral_in_integerliteral4496
public static final BitSet FOLLOW_HEXNUMERAL_in_hexintegerliteral4519
public static final BitSet FOLLOW_decimalnumeral_in_decimalintegerliteral4545
public static final BitSet FOLLOW_DIGITS_in_decimalnumeral4569
public static final BitSet FOLLOW_RESULT_in_jmlprimary4598
public static final BitSet FOLLOW_EXCEPTION_in_jmlprimary4609
public static final BitSet FOLLOW_specquantifiedexpression_in_jmlprimary4634
public static final BitSet FOLLOW_bsumterm_in_jmlprimary4660
public static final BitSet FOLLOW_seqdefterm_in_jmlprimary4686
public static final BitSet FOLLOW_oldexpression_in_jmlprimary4707
public static final BitSet FOLLOW_transactionUpdated_in_jmlprimary4722
public static final BitSet FOLLOW_BACKUP_in_jmlprimary4731
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4733
public static final BitSet FOLLOW_expression_in_jmlprimary4737
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4739
public static final BitSet FOLLOW_PERMISSION_in_jmlprimary4758
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4760
public static final BitSet FOLLOW_expression_in_jmlprimary4764
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4766
public static final BitSet FOLLOW_NONNULLELEMENTS_in_jmlprimary4785
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4787
public static final BitSet FOLLOW_expression_in_jmlprimary4791
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4793
public static final BitSet FOLLOW_INFORMAL_DESCRIPTION_in_jmlprimary4809
public static final BitSet FOLLOW_DL_ESCAPE_in_jmlprimary4825
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4835
public static final BitSet FOLLOW_expressionlist_in_jmlprimary4841
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4846
public static final BitSet FOLLOW_MAPEMPTY_in_jmlprimary4880
public static final BitSet FOLLOW_mapExpression_in_jmlprimary4903
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4905
public static final BitSet FOLLOW_expressionlist_in_jmlprimary4911
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4916
public static final BitSet FOLLOW_SEQ2MAP_in_jmlprimary4933
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4935
public static final BitSet FOLLOW_expressionlist_in_jmlprimary4941
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4946
public static final BitSet FOLLOW_NOT_MODIFIED_in_jmlprimary4961
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4963
public static final BitSet FOLLOW_storeRefUnion_in_jmlprimary4967
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4969
public static final BitSet FOLLOW_NOT_ASSIGNED_in_jmlprimary4991
public static final BitSet FOLLOW_LPAREN_in_jmlprimary4993
public static final BitSet FOLLOW_storeRefUnion_in_jmlprimary4997
public static final BitSet FOLLOW_RPAREN_in_jmlprimary4999
public static final BitSet FOLLOW_FRESH_in_jmlprimary5026
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5028
public static final BitSet FOLLOW_expressionlist_in_jmlprimary5032
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5034
public static final BitSet FOLLOW_REACH_in_jmlprimary5048
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5050
public static final BitSet FOLLOW_storeref_in_jmlprimary5054
public static final BitSet FOLLOW_COMMA_in_jmlprimary5056
public static final BitSet FOLLOW_expression_in_jmlprimary5060
public static final BitSet FOLLOW_COMMA_in_jmlprimary5062
public static final BitSet FOLLOW_expression_in_jmlprimary5066
public static final BitSet FOLLOW_COMMA_in_jmlprimary5069
public static final BitSet FOLLOW_expression_in_jmlprimary5073
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5077
public static final BitSet FOLLOW_REACHLOCS_in_jmlprimary5091
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5093
public static final BitSet FOLLOW_storeref_in_jmlprimary5097
public static final BitSet FOLLOW_COMMA_in_jmlprimary5099
public static final BitSet FOLLOW_expression_in_jmlprimary5103
public static final BitSet FOLLOW_COMMA_in_jmlprimary5106
public static final BitSet FOLLOW_expression_in_jmlprimary5110
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5114
public static final BitSet FOLLOW_DURATION_in_jmlprimary5130
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5132
public static final BitSet FOLLOW_expression_in_jmlprimary5136
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5138
public static final BitSet FOLLOW_SPACE_in_jmlprimary5154
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5156
public static final BitSet FOLLOW_expression_in_jmlprimary5160
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5162
public static final BitSet FOLLOW_WORKINGSPACE_in_jmlprimary5178
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5180
public static final BitSet FOLLOW_expression_in_jmlprimary5184
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5186
public static final BitSet FOLLOW_MAX_in_jmlprimary5208
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5210
public static final BitSet FOLLOW_expression_in_jmlprimary5214
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5216
public static final BitSet FOLLOW_TYPEOF_in_jmlprimary5232
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5234
public static final BitSet FOLLOW_expression_in_jmlprimary5238
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5240
public static final BitSet FOLLOW_ELEMTYPE_in_jmlprimary5254
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5256
public static final BitSet FOLLOW_expression_in_jmlprimary5260
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5262
public static final BitSet FOLLOW_TYPE_SMALL_in_jmlprimary5276
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5278
public static final BitSet FOLLOW_typespec_in_jmlprimary5282
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5284
public static final BitSet FOLLOW_LOCKSET_in_jmlprimary5300
public static final BitSet FOLLOW_IS_INITIALIZED_in_jmlprimary5314
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5316
public static final BitSet FOLLOW_referencetype_in_jmlprimary5320
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5322
public static final BitSet FOLLOW_INVARIANT_FOR_in_jmlprimary5336
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5338
public static final BitSet FOLLOW_expression_in_jmlprimary5342
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5344
public static final BitSet FOLLOW_STATIC_INVARIANT_FOR_in_jmlprimary5355
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5357
public static final BitSet FOLLOW_referencetype_in_jmlprimary5361
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5363
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5387
public static final BitSet FOLLOW_LBLNEG_in_jmlprimary5391
public static final BitSet FOLLOW_IDENT_in_jmlprimary5393
public static final BitSet FOLLOW_expression_in_jmlprimary5397
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5399
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5423
public static final BitSet FOLLOW_LBLPOS_in_jmlprimary5427
public static final BitSet FOLLOW_IDENT_in_jmlprimary5429
public static final BitSet FOLLOW_expression_in_jmlprimary5433
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5435
public static final BitSet FOLLOW_INDEX_in_jmlprimary5445
public static final BitSet FOLLOW_VALUES_in_jmlprimary5454
public static final BitSet FOLLOW_STRING_EQUAL_in_jmlprimary5466
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5468
public static final BitSet FOLLOW_expression_in_jmlprimary5472
public static final BitSet FOLLOW_COMMA_in_jmlprimary5474
public static final BitSet FOLLOW_expression_in_jmlprimary5478
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5480
public static final BitSet FOLLOW_EMPTYSET_in_jmlprimary5501
public static final BitSet FOLLOW_createLocset_in_jmlprimary5526
public static final BitSet FOLLOW_set_in_jmlprimary5547
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5555
public static final BitSet FOLLOW_storeRefUnion_in_jmlprimary5559
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5561
public static final BitSet FOLLOW_INTERSECT_in_jmlprimary5582
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5584
public static final BitSet FOLLOW_storeRefIntersect_in_jmlprimary5588
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5590
public static final BitSet FOLLOW_SETMINUS_in_jmlprimary5611
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5613
public static final BitSet FOLLOW_storeref_in_jmlprimary5617
public static final BitSet FOLLOW_COMMA_in_jmlprimary5619
public static final BitSet FOLLOW_storeref_in_jmlprimary5623
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5625
public static final BitSet FOLLOW_ALLFIELDS_in_jmlprimary5646
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5648
public static final BitSet FOLLOW_expression_in_jmlprimary5652
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5654
public static final BitSet FOLLOW_ALLOBJECTS_in_jmlprimary5674
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5676
public static final BitSet FOLLOW_storeref_in_jmlprimary5680
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5682
public static final BitSet FOLLOW_UNIONINF_in_jmlprimary5702
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5712
public static final BitSet FOLLOW_boundvarmodifiers_in_jmlprimary5725
public static final BitSet FOLLOW_quantifiedvardecls_in_jmlprimary5739
public static final BitSet FOLLOW_SEMI_in_jmlprimary5749
public static final BitSet FOLLOW_predicate_in_jmlprimary5780
public static final BitSet FOLLOW_SEMI_in_jmlprimary5782
public static final BitSet FOLLOW_SEMI_in_jmlprimary5786
public static final BitSet FOLLOW_storeref_in_jmlprimary5801
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5811
public static final BitSet FOLLOW_DISJOINT_in_jmlprimary5834
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5836
public static final BitSet FOLLOW_storeRefList_in_jmlprimary5840
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5842
public static final BitSet FOLLOW_SUBSET_in_jmlprimary5855
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5857
public static final BitSet FOLLOW_storeref_in_jmlprimary5861
public static final BitSet FOLLOW_COMMA_in_jmlprimary5863
public static final BitSet FOLLOW_storeref_in_jmlprimary5867
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5869
public static final BitSet FOLLOW_NEWELEMSFRESH_in_jmlprimary5890
public static final BitSet FOLLOW_LPAREN_in_jmlprimary5892
public static final BitSet FOLLOW_storeref_in_jmlprimary5896
public static final BitSet FOLLOW_RPAREN_in_jmlprimary5898
public static final BitSet FOLLOW_sequence_in_jmlprimary6067
public static final BitSet FOLLOW_LPAREN_in_jmlprimary6086
public static final BitSet FOLLOW_expression_in_jmlprimary6090
public static final BitSet FOLLOW_RPAREN_in_jmlprimary6092
public static final BitSet FOLLOW_SEQEMPTY_in_sequence6128
public static final BitSet FOLLOW_seqdefterm_in_sequence6168
public static final BitSet FOLLOW_set_in_sequence6178
public static final BitSet FOLLOW_LPAREN_in_sequence6186
public static final BitSet FOLLOW_exprList_in_sequence6190
public static final BitSet FOLLOW_RPAREN_in_sequence6192
public static final BitSet FOLLOW_SEQSUB_in_sequence6213
public static final BitSet FOLLOW_LPAREN_in_sequence6215
public static final BitSet FOLLOW_expression_in_sequence6219
public static final BitSet FOLLOW_COMMA_in_sequence6221
public static final BitSet FOLLOW_expression_in_sequence6225
public static final BitSet FOLLOW_COMMA_in_sequence6227
public static final BitSet FOLLOW_expression_in_sequence6231
public static final BitSet FOLLOW_RPAREN_in_sequence6233
public static final BitSet FOLLOW_SEQREVERSE_in_sequence6254
public static final BitSet FOLLOW_LPAREN_in_sequence6256
public static final BitSet FOLLOW_expression_in_sequence6260
public static final BitSet FOLLOW_RPAREN_in_sequence6262
public static final BitSet FOLLOW_SEQREPLACE_in_sequence6282
public static final BitSet FOLLOW_LPAREN_in_sequence6284
public static final BitSet FOLLOW_expression_in_sequence6288
public static final BitSet FOLLOW_COMMA_in_sequence6290
public static final BitSet FOLLOW_expression_in_sequence6294
public static final BitSet FOLLOW_COMMA_in_sequence6296
public static final BitSet FOLLOW_expression_in_sequence6300
public static final BitSet FOLLOW_RPAREN_in_sequence6302
public static final BitSet FOLLOW_SEQCONCAT_in_sequence6335
public static final BitSet FOLLOW_SEQGET_in_sequence6343
public static final BitSet FOLLOW_INDEXOF_in_sequence6351
public static final BitSet FOLLOW_LPAREN_in_sequence6363
public static final BitSet FOLLOW_expression_in_sequence6367
public static final BitSet FOLLOW_COMMA_in_sequence6369
public static final BitSet FOLLOW_expression_in_sequence6373
public static final BitSet FOLLOW_RPAREN_in_sequence6375
public static final BitSet FOLLOW_set_in_mapExpression6400
public static final BitSet FOLLOW_set_in_quantifier6477
public static final BitSet FOLLOW_LPAREN_in_specquantifiedexpression6550
public static final BitSet FOLLOW_quantifier_in_specquantifiedexpression6555
public static final BitSet FOLLOW_boundvarmodifiers_in_specquantifiedexpression6561
public static final BitSet FOLLOW_quantifiedvardecls_in_specquantifiedexpression6568
public static final BitSet FOLLOW_SEMI_in_specquantifiedexpression6570
public static final BitSet FOLLOW_predicate_in_specquantifiedexpression6587
public static final BitSet FOLLOW_SEMI_in_specquantifiedexpression6589
public static final BitSet FOLLOW_SEMI_in_specquantifiedexpression6593
public static final BitSet FOLLOW_expression_in_specquantifiedexpression6600
public static final BitSet FOLLOW_RPAREN_in_specquantifiedexpression6606
public static final BitSet FOLLOW_PRE_in_oldexpression6643
public static final BitSet FOLLOW_LPAREN_in_oldexpression6645
public static final BitSet FOLLOW_expression_in_oldexpression6649
public static final BitSet FOLLOW_RPAREN_in_oldexpression6651
public static final BitSet FOLLOW_OLD_in_oldexpression6663
public static final BitSet FOLLOW_LPAREN_in_oldexpression6665
public static final BitSet FOLLOW_expression_in_oldexpression6669
public static final BitSet FOLLOW_COMMA_in_oldexpression6672
public static final BitSet FOLLOW_IDENT_in_oldexpression6676
public static final BitSet FOLLOW_RPAREN_in_oldexpression6680
public static final BitSet FOLLOW_LPAREN_in_bsumterm6721
public static final BitSet FOLLOW_BSUM_in_bsumterm6733
public static final BitSet FOLLOW_quantifiedvardecls_in_bsumterm6737
public static final BitSet FOLLOW_SEMI_in_bsumterm6757
public static final BitSet FOLLOW_expression_in_bsumterm6783
public static final BitSet FOLLOW_SEMI_in_bsumterm6785
public static final BitSet FOLLOW_expression_in_bsumterm6790
public static final BitSet FOLLOW_SEMI_in_bsumterm6792
public static final BitSet FOLLOW_expression_in_bsumterm6796
public static final BitSet FOLLOW_RPAREN_in_bsumterm6826
public static final BitSet FOLLOW_LPAREN_in_seqdefterm6870
public static final BitSet FOLLOW_SEQDEF_in_seqdefterm6882
public static final BitSet FOLLOW_quantifiedvardecls_in_seqdefterm6886
public static final BitSet FOLLOW_SEMI_in_seqdefterm6906
public static final BitSet FOLLOW_expression_in_seqdefterm6932
public static final BitSet FOLLOW_SEMI_in_seqdefterm6934
public static final BitSet FOLLOW_expression_in_seqdefterm6939
public static final BitSet FOLLOW_SEMI_in_seqdefterm6941
public static final BitSet FOLLOW_expression_in_seqdefterm6945
public static final BitSet FOLLOW_RPAREN_in_seqdefterm6975
public static final BitSet FOLLOW_typespec_in_quantifiedvardecls7033
public static final BitSet FOLLOW_quantifiedvariabledeclarator_in_quantifiedvardecls7037
public static final BitSet FOLLOW_COMMA_in_quantifiedvardecls7053
public static final BitSet FOLLOW_quantifiedvariabledeclarator_in_quantifiedvardecls7057
public static final BitSet FOLLOW_NON_NULL_in_boundvarmodifiers7091
public static final BitSet FOLLOW_NULLABLE_in_boundvarmodifiers7095
public static final BitSet FOLLOW_type_in_typespec7122
public static final BitSet FOLLOW_dims_in_typespec7134
public static final BitSet FOLLOW_LBRACKET_in_dims7164
public static final BitSet FOLLOW_RBRACKET_in_dims7166
public static final BitSet FOLLOW_builtintype_in_type7205
public static final BitSet FOLLOW_referencetype_in_type7216
public static final BitSet FOLLOW_TYPE_in_type7225
public static final BitSet FOLLOW_name_in_referencetype7253
public static final BitSet FOLLOW_BYTE_in_builtintype7281
public static final BitSet FOLLOW_SHORT_in_builtintype7298
public static final BitSet FOLLOW_INT_in_builtintype7315
public static final BitSet FOLLOW_LONG_in_builtintype7332
public static final BitSet FOLLOW_BOOLEAN_in_builtintype7349
public static final BitSet FOLLOW_VOID_in_builtintype7366
public static final BitSet FOLLOW_BIGINT_in_builtintype7383
public static final BitSet FOLLOW_REAL_in_builtintype7400
public static final BitSet FOLLOW_LOCSET_in_builtintype7421
public static final BitSet FOLLOW_SEQ_in_builtintype7449
public static final BitSet FOLLOW_FREE_in_builtintype7475
public static final BitSet FOLLOW_IDENT_in_name7501
public static final BitSet FOLLOW_DOT_in_name7514
public static final BitSet FOLLOW_IDENT_in_name7518
public static final BitSet FOLLOW_IDENT_in_quantifiedvariabledeclarator7557
public static final BitSet FOLLOW_dims_in_quantifiedvariabledeclarator7562
public static final BitSet FOLLOW_LPAREN_in_synpred1_KeYJMLParser3594
public static final BitSet FOLLOW_typespec_in_synpred1_KeYJMLParser3596
public static final BitSet FOLLOW_RPAREN_in_synpred1_KeYJMLParser3598
public static final BitSet FOLLOW_LPAREN_in_synpred2_KeYJMLParser4625
public static final BitSet FOLLOW_quantifier_in_synpred2_KeYJMLParser4627
public static final BitSet FOLLOW_LPAREN_in_synpred3_KeYJMLParser4651
public static final BitSet FOLLOW_BSUM_in_synpred3_KeYJMLParser4653
public static final BitSet FOLLOW_LPAREN_in_synpred4_KeYJMLParser4677
public static final BitSet FOLLOW_SEQDEF_in_synpred4_KeYJMLParser4679
public static final BitSet FOLLOW_LPAREN_in_synpred6_KeYJMLParser4830
public static final BitSet FOLLOW_MAX_in_synpred7_KeYJMLParser5201
public static final BitSet FOLLOW_LPAREN_in_synpred8_KeYJMLParser5379
public static final BitSet FOLLOW_LBLNEG_in_synpred8_KeYJMLParser5381
public static final BitSet FOLLOW_LPAREN_in_synpred9_KeYJMLParser5415
public static final BitSet FOLLOW_LBLPOS_in_synpred9_KeYJMLParser5417
public static final BitSet FOLLOW_predicate_in_synpred10_KeYJMLParser5771
public static final BitSet FOLLOW_SEMI_in_synpred10_KeYJMLParser5773
public static final BitSet FOLLOW_SEQEMPTY_in_synpred11_KeYJMLParser5920
public static final BitSet FOLLOW_LPAREN_in_synpred11_KeYJMLParser5933
public static final BitSet FOLLOW_set_in_synpred11_KeYJMLParser5935
public static final BitSet FOLLOW_quantifiedvardecls_in_synpred11_KeYJMLParser5943
public static final BitSet FOLLOW_SEMI_in_synpred11_KeYJMLParser5945
public static final BitSet FOLLOW_set_in_synpred11_KeYJMLParser5958
public static final BitSet FOLLOW_LPAREN_in_synpred11_KeYJMLParser5966
public static final BitSet FOLLOW_SEQSUB_in_synpred11_KeYJMLParser5978
public static final BitSet FOLLOW_LPAREN_in_synpred11_KeYJMLParser5980
public static final BitSet FOLLOW_SEQREVERSE_in_synpred11_KeYJMLParser5992
public static final BitSet FOLLOW_SEQREPLACE_in_synpred11_KeYJMLParser6004
public static final BitSet FOLLOW_SEQCONCAT_in_synpred11_KeYJMLParser6025
public static final BitSet FOLLOW_SEQGET_in_synpred11_KeYJMLParser6037
public static final BitSet FOLLOW_INDEXOF_in_synpred11_KeYJMLParser6049
public static final BitSet FOLLOW_LPAREN_in_synpred12_KeYJMLParser6149
public static final BitSet FOLLOW_set_in_synpred12_KeYJMLParser6151
public static final BitSet FOLLOW_quantifiedvardecls_in_synpred12_KeYJMLParser6159
public static final BitSet FOLLOW_SEMI_in_synpred12_KeYJMLParser6161
public static final BitSet FOLLOW_predicate_in_synpred13_KeYJMLParser6578
public static final BitSet FOLLOW_SEMI_in_synpred13_KeYJMLParser6580
public static final BitSet FOLLOW_builtintype_in_synpred14_KeYJMLParser7198
public KeYJMLParser(TokenStream input)
public KeYJMLParser(TokenStream input, RecognizerSharedState state)
private KeYJMLParser(KeYJMLLexer lexer, String fileName, Services services, KeYJavaType specInClass, ProgramVariable self, ImmutableList<ProgramVariable> paramVars, ProgramVariable result, ProgramVariable exc, Map<LocationVariable,Term> atPres)
public KeYJMLParser(PositionedString ps, Services services, KeYJavaType specInClass, ProgramVariable self, ImmutableList<ProgramVariable> paramVars, ProgramVariable result, ProgramVariable exc, Map<LocationVariable,Term> atPres)
public Parser[] getDelegates()
public String[] getTokenNames()
getTokenNames
in class BaseRecognizer
public String getGrammarFileName()
getGrammarFileName
in class BaseRecognizer
static ANTLRStringStream createANTLRStringStream(PositionedString ps)
public SLTranslationExceptionManager getExceptionManager()
private void raiseError(String msg) throws SLTranslationException
SLTranslationException
private void raiseError(String msg, Token t) throws SLTranslationException
SLTranslationException
private void raiseNotSupported(String feature) throws SLTranslationException
SLTranslationException
private void addIgnoreWarning(String feature, Token t)
public List<PositionedString> getWarnings()
public Term parseExpression() throws SLTranslationException
SLTranslationException
public ImmutableList<ProgramVariable> parseVariableDeclaration() throws SLTranslationException
SLTranslationException
private Sort[] getSorts(Term[] terms)
private LocationVariable getBaseHeap()
private LocationVariable getSavedHeap()
private LocationVariable getPermissionHeap()
private Term convertToOld(Term term)
private Term convertToPermission(Term term) throws SLTranslationException
SLTranslationException
private String createSignatureString(ImmutableList<SLExpression> signature)
private SLExpression lookupIdentifier(String lookupName, SLExpression receiver, SLParameters params, Token t) throws SLTranslationException
SLTranslationException
public void reportError(RecognitionException ex)
reportError
in class BaseRecognizer
public void recover(IntStream input, RecognitionException re)
recover
in class BaseRecognizer
public Object recoverFromMismatchedSet(IntStream input, RecognitionException e, BitSet follow) throws RecognitionException
recoverFromMismatchedSet
in class BaseRecognizer
RecognitionException
protected Object recoverFromMismatchedToken(IntStream input, int ttype, BitSet follow) throws RecognitionException
recoverFromMismatchedToken
in class BaseRecognizer
RecognitionException
protected void mismatch(IntStream input, int ttype, BitSet follow) throws RecognitionException
RecognitionException
public final Object top() throws RecognitionException, SLTranslationException
public final Term accessibleclause() throws RecognitionException, SLTranslationException
public final Term assignableclause() throws RecognitionException, SLTranslationException
public final Triple<ObserverFunction,Term,Term> dependsclause() throws RecognitionException, SLTranslationException
public final Term decreasesclause() throws RecognitionException, SLTranslationException
public final Term requiresclause() throws RecognitionException, SLTranslationException
public final Term requiresfreeclause() throws RecognitionException, SLTranslationException
public final Term joinprocclause() throws RecognitionException, SLTranslationException
public final Term ensuresclause() throws RecognitionException, SLTranslationException
public final Term ensuresfreeclause() throws RecognitionException, SLTranslationException
public final Term axiomsclause() throws RecognitionException, SLTranslationException
public final Pair<ObserverFunction,Term> representsclause() throws RecognitionException, SLTranslationException
public final InfFlowSpec separatesclause() throws RecognitionException, SLTranslationException
public final InfFlowSpec loopseparatesclause() throws RecognitionException, SLTranslationException
public final InfFlowSpec determinesclause() throws RecognitionException, SLTranslationException
public final InfFlowSpec loopdeterminesclause() throws RecognitionException, SLTranslationException
public final ImmutableList<Term> infflowspeclist() throws RecognitionException, SLTranslationException
public final Term signalsclause() throws RecognitionException, SLTranslationException
public final Term signalsonlyclause() throws RecognitionException, SLTranslationException
public final Term termexpression() throws RecognitionException, SLTranslationException
public final Pair breaksclause() throws RecognitionException, SLTranslationException
public final Pair continuesclause() throws RecognitionException, SLTranslationException
public final Term returnsclause() throws RecognitionException, SLTranslationException
public final Term storeRefUnion() throws RecognitionException, SLTranslationException
public final ImmutableList<Term> storeRefList() throws RecognitionException, SLTranslationException
public final Term storeRefIntersect() throws RecognitionException, SLTranslationException
public final Term storeref() throws RecognitionException, SLTranslationException
public final Term createLocset() throws RecognitionException, SLTranslationException
public final ImmutableList<SLExpression> exprList() throws RecognitionException, SLTranslationException
public final Term storeRefExpr() throws RecognitionException, SLTranslationException
public final SLExpression specarrayrefexpr(SLExpression receiver, String fullyQualifiedName, Token lbrack) throws RecognitionException, SLTranslationException
public final Term predornot() throws RecognitionException, SLTranslationException
public final Term predicate() throws RecognitionException, SLTranslationException
public final SLExpression expression() throws RecognitionException, SLTranslationException
public final SLExpression conditionalexpr() throws RecognitionException, SLTranslationException
public final SLExpression equivalenceexpr() throws RecognitionException, SLTranslationException
public final SLExpression impliesexpr() throws RecognitionException, SLTranslationException
public final SLExpression impliesforwardexpr() throws RecognitionException, SLTranslationException
public final SLExpression logicalorexpr() throws RecognitionException, SLTranslationException
public final SLExpression logicalandexpr() throws RecognitionException, SLTranslationException
public final SLExpression inclusiveorexpr() throws RecognitionException, SLTranslationException
public final SLExpression exclusiveorexpr() throws RecognitionException, SLTranslationException
public final SLExpression andexpr() throws RecognitionException, SLTranslationException
public final SLExpression equalityexpr() throws RecognitionException, SLTranslationException
public final SLExpression relationalexpr() throws RecognitionException, SLTranslationException
public final SLExpression shiftexpr() throws RecognitionException, SLTranslationException
public final SLExpression additiveexpr() throws RecognitionException, SLTranslationException
public final SLExpression multexpr() throws RecognitionException, SLTranslationException
public final SLExpression unaryexpr() throws RecognitionException, SLTranslationException
public final SLExpression castexpr() throws RecognitionException, SLTranslationException
public final SLExpression unaryexprnotplusminus() throws RecognitionException, SLTranslationException
public final SLExpression postfixexpr() throws RecognitionException, SLTranslationException
public final SLExpression primaryexpr() throws RecognitionException, SLTranslationException
public final SLExpression transactionUpdated() throws RecognitionException, SLTranslationException
public final SLExpression primarysuffix(SLExpression receiver, String fullyQualifiedName) throws RecognitionException, SLTranslationException
public final void new_expr() throws RecognitionException, SLTranslationException
public final void array_dimensions() throws RecognitionException, SLTranslationException
public final void array_dimension() throws RecognitionException, SLTranslationException
public final void array_initializer() throws RecognitionException, SLTranslationException
public final ImmutableList<SLExpression> expressionlist() throws RecognitionException, SLTranslationException
public final SLExpression constant() throws RecognitionException, SLTranslationException
public final SLExpression javaliteral() throws RecognitionException, SLTranslationException
public final SLExpression integerliteral() throws RecognitionException, SLTranslationException
public final SLExpression hexintegerliteral() throws RecognitionException, SLTranslationException
public final SLExpression decimalintegerliteral() throws RecognitionException, SLTranslationException
public final SLExpression decimalnumeral() throws RecognitionException, SLTranslationException
public final SLExpression jmlprimary() throws RecognitionException, SLTranslationException
public final SLExpression sequence() throws RecognitionException, SLTranslationException
public final Token mapExpression() throws RecognitionException
RecognitionException
public final Token quantifier() throws RecognitionException
RecognitionException
public final SLExpression specquantifiedexpression() throws RecognitionException, SLTranslationException
public final SLExpression oldexpression() throws RecognitionException, SLTranslationException
public final SLExpression bsumterm() throws RecognitionException, SLTranslationException
public final SLExpression seqdefterm() throws RecognitionException, SLTranslationException
public final Pair<KeYJavaType,ImmutableList<LogicVariable>> quantifiedvardecls() throws RecognitionException, SLTranslationException
public final boolean boundvarmodifiers() throws RecognitionException, SLTranslationException
public final KeYJavaType typespec() throws RecognitionException, SLTranslationException
public final int dims() throws RecognitionException, SLTranslationException
public final KeYJavaType type() throws RecognitionException, SLTranslationException
public final KeYJavaType referencetype() throws RecognitionException, SLTranslationException
public final KeYJavaType builtintype() throws RecognitionException, SLTranslationException
public final String name() throws RecognitionException, SLTranslationException
public final LogicVariable quantifiedvariabledeclarator(KeYJavaType t) throws RecognitionException, SLTranslationException
public final void synpred1_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred2_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred3_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred4_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred5_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred6_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred7_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred8_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred9_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred10_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred11_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred12_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred13_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final void synpred14_KeYJMLParser_fragment() throws RecognitionException
RecognitionException
public final boolean synpred8_KeYJMLParser()
public final boolean synpred9_KeYJMLParser()
public final boolean synpred11_KeYJMLParser()
public final boolean synpred10_KeYJMLParser()
public final boolean synpred4_KeYJMLParser()
public final boolean synpred5_KeYJMLParser()
public final boolean synpred14_KeYJMLParser()
public final boolean synpred2_KeYJMLParser()
public final boolean synpred6_KeYJMLParser()
public final boolean synpred13_KeYJMLParser()
public final boolean synpred7_KeYJMLParser()
public final boolean synpred3_KeYJMLParser()
public final boolean synpred1_KeYJMLParser()
public final boolean synpred12_KeYJMLParser()