public class JmlParser
extends org.antlr.v4.runtime.Parser
Modifier and Type | Field and Description |
---|---|
static org.antlr.v4.runtime.atn.ATN |
_ATN |
protected static org.antlr.v4.runtime.dfa.DFA[] |
_decisionToDFA |
static java.lang.String |
_serializedATN |
protected static org.antlr.v4.runtime.atn.PredictionContextCache |
_sharedContextCache |
static int |
ABSTRACT |
static int |
ACCESSIBLE |
static int |
ALLFIELDS |
static int |
ALLOBJECTS |
static int |
ALSO |
static int |
AND |
static int |
ASSERT |
static int |
ASSIGNABLE |
static int |
ASSIGNS |
static int |
ASSUME |
static int |
AXIOM |
static int |
BACKUP |
static int |
BEFORE |
static int |
BEHAVIOR |
static int |
BIGINT |
static int |
BINLITERAL |
static int |
BITWISENOT |
static int |
BODY |
static int |
BOOLEAN |
static int |
BREAK_BEHAVIOR |
static int |
BREAKS |
static int |
BSUM |
static int |
BY |
static int |
BYTE |
static int |
C_COLON |
static int |
C_COMMA |
static int |
C_DOT |
static int |
C_LBRACE |
static int |
C_LBRACKET |
static int |
C_LPAREN |
static int |
C_RBRACE |
static int |
C_RBRACKET |
static int |
C_RPAREN |
static int |
C_STRING_LITERAL |
static int |
CAPTURES |
static int |
CHAR_LITERAL |
static int |
CODE |
static int |
CODE_BIGINT_MATH |
static int |
CODE_JAVA_MATH |
static int |
CODE_SAFE_MATH |
static int |
CODE_SAVE_MATH |
static int |
COLON |
static int |
COMMA |
static int |
COMMENT |
static int |
CONST |
static int |
CONSTRAINT |
static int |
CONTINUE_BEHAVIOR |
static int |
CONTINUES |
static int |
DEBUG |
static int |
DECLASSIFIES |
static int |
DECLITERAL |
static int |
DECREASING |
static int |
DEPENDS |
static int |
DETERMINES |
static int |
DISJOINT |
static int |
DIV |
static int |
DIVERGES |
static int |
DOC_COMMENT |
static int |
DOMAIN_IMPLIES_CREATED |
static int |
DOT |
static int |
DOTDOT |
static int |
DURATION |
static int |
E_JML_ML_END |
static int |
E_MEASURED_BY |
static int |
E_TRANSIENT |
static int |
ELEMTYPE |
static int |
EMPTYSET |
static int |
ENSURES |
static int |
EQ_NEQ |
static int |
EQUAL_SINGLE |
static int |
EQV_ANTIV |
static int |
ERASES |
static int |
ERROR_CHAR |
static int |
EVERYTHING |
static int |
EXCEPTION |
static int |
EXCEPTIONAL_BEHAVIOUR |
static int |
EXISTS |
static int |
FALSE |
static int |
FINAL |
static int |
FOR_EXAMPLE |
static int |
FORALL |
static int |
FREE |
static int |
FRESH |
static int |
GEQ |
static int |
GHOST |
static int |
GT |
static int |
HELPER |
static int |
HEXLITERAL |
static int |
IDENT |
static int |
IMPLIES |
static int |
IMPLIES_THAT |
static int |
IMPLIESBACKWARD |
static int |
IN |
static int |
IN_DOMAIN |
static int |
INCLUSIVEOR |
static int |
INDEX |
static int |
INDEXOF |
static int |
INFORMAL_DESCRIPTION |
static int |
INITIALLY |
static int |
INSTANCE |
static int |
INSTANCEOF |
static int |
INT |
static int |
INTERSECT |
static int |
INTO |
static int |
INV |
static int |
INVARIANT |
static int |
INVARIANT_FOR |
static int |
IS_FINITE |
static int |
IS_INITIALIZED |
static int |
ITSELF |
static int |
JML_IDENT |
static int |
JML_ML_END |
static int |
JML_ML_START |
static int |
JML_SL_START |
static int |
LARROW |
static int |
LBLNEG |
static int |
LBLPOS |
static int |
LBRACE |
static int |
LBRACKET |
static int |
LEQ |
static int |
LOCKSET |
static int |
LOCKSET_LEQ |
static int |
LOCKSET_LT |
static int |
LOCSET |
static int |
LOGICALAND |
static int |
LOGICALOR |
static int |
LONG |
static int |
LOOP_CONTRACT |
static int |
LOOP_DETERMINES |
static int |
LOOP_INVARIANT |
static int |
LOOP_SEPARATES |
static int |
LPAREN |
static int |
LT |
static int |
MAP |
static int |
MAP_GET |
static int |
MAP_OVERRIDE |
static int |
MAP_REMOVE |
static int |
MAP_SINGLETON |
static int |
MAP_SIZE |
static int |
MAP_UPDATE |
static int |
MAPEMPTY |
static int |
MAPS |
static int |
MAX |
static int |
MEASURED_BY |
static int |
MERGE_PARAMS |
static int |
MERGE_POINT |
static int |
MERGE_PROC |
static int |
MIN |
static int |
MINUS |
static int |
MOD |
static int |
MODEL |
static int |
MODEL_BEHAVIOUR |
static int |
MODIFIABLE |
static int |
MODIFIES |
static int |
MONITORED |
static int |
MONITORS_FOR |
static int |
MULT |
static int |
NATIVE |
static int |
NEST_END |
static int |
NEST_START |
static int |
NEW |
static int |
NEW_OBJECTS |
static int |
NEWELEMSFRESH |
static int |
NO_STATE |
static int |
NON_NULL |
static int |
NONNULLELEMENTS |
static int |
NORMAL_BEHAVIOR |
static int |
NOT |
static int |
NOT_ASSIGNED |
static int |
NOT_MODIFIED |
static int |
NOT_SPECIFIED |
static int |
NOTHING |
static int |
NOWARN |
static int |
NULL |
static int |
NULLABLE |
static int |
NULLABLE_BY_DEFAULT |
static int |
NUM_OF |
static int |
OCTLITERAL |
static int |
OLD |
static int |
PERMISSION |
static int |
PLUS |
static int |
PRE |
static int |
PRIVATE |
static int |
PRODUCT |
static int |
PROTECTED |
static int |
PUBLIC |
static int |
PURE |
static int |
QUESTIONMARK |
static int |
RARROW |
static int |
RBRACE |
static int |
RBRACKET |
static int |
REACH |
static int |
REACHLOCS |
static int |
READABLE |
static int |
REAL |
static int |
REPRESENTS |
static int |
REQUIRES |
static int |
RESPECTS |
static int |
RESULT |
static int |
RETURN |
static int |
RETURN_BEHAVIOR |
static int |
RETURNS |
static int |
RPAREN |
static int |
RULE_accessible_clause |
static int |
RULE_additiveexpr |
static int |
RULE_also_keyword |
static int |
RULE_andexpr |
static int |
RULE_array_dimension |
static int |
RULE_array_dimensions |
static int |
RULE_array_initializer |
static int |
RULE_assert_statement |
static int |
RULE_assignable_clause |
static int |
RULE_assume_statement |
static int |
RULE_beforeexpression |
static int |
RULE_block_loop_specification |
static int |
RULE_block_specification |
static int |
RULE_boundvarmodifiers |
static int |
RULE_breaks_clause |
static int |
RULE_bsumterm |
static int |
RULE_builtintype |
static int |
RULE_captures_clause |
static int |
RULE_castexpr |
static int |
RULE_charliteral |
static int |
RULE_class_axiom |
static int |
RULE_class_invariant |
static int |
RULE_classlevel_comment |
static int |
RULE_classlevel_comments |
static int |
RULE_classlevel_element |
static int |
RULE_classlevel_element0 |
static int |
RULE_clause |
static int |
RULE_clauseEOF |
static int |
RULE_conditionalexpr |
static int |
RULE_constant |
static int |
RULE_continues_clause |
static int |
RULE_createLocset |
static int |
RULE_datagroup_clause |
static int |
RULE_debug_statement |
static int |
RULE_determines_clause |
static int |
RULE_dims |
static int |
RULE_diverges_clause |
static int |
RULE_duration_clause |
static int |
RULE_ensures_clause |
static int |
RULE_equalityexpr |
static int |
RULE_equivalenceexpr |
static int |
RULE_exclusiveorexpr |
static int |
RULE_expression |
static int |
RULE_expressionEOF |
static int |
RULE_expressionlist |
static int |
RULE_exprList |
static int |
RULE_false_ |
static int |
RULE_field_declaration |
static int |
RULE_fieldarrayaccess |
static int |
RULE_fieldarrayaccess_suffix |
static int |
RULE_history_constraint |
static int |
RULE_ident |
static int |
RULE_impliesexpr |
static int |
RULE_impliesforwardexpr |
static int |
RULE_in_group_clause |
static int |
RULE_inclusiveorexpr |
static int |
RULE_infflowspeclist |
static int |
RULE_infinite_union_expr |
static int |
RULE_initialiser |
static int |
RULE_initially_clause |
static int |
RULE_instance_of |
static int |
RULE_integerliteral |
static int |
RULE_inv |
static int |
RULE_javaliteral |
static int |
RULE_jmlprimary |
static int |
RULE_logicalandexpr |
static int |
RULE_logicalorexpr |
static int |
RULE_loop_contract_keyword |
static int |
RULE_loop_determines_clause |
static int |
RULE_loop_invariant |
static int |
RULE_loop_separates_clause |
static int |
RULE_loop_specification |
static int |
RULE_mapExpression |
static int |
RULE_maps_into_clause |
static int |
RULE_measured_by_clause |
static int |
RULE_merge_point_statement |
static int |
RULE_mergeparamsspec |
static int |
RULE_method_body |
static int |
RULE_method_declaration |
static int |
RULE_method_specification |
static int |
RULE_methodlevel_comment |
static int |
RULE_methodlevel_element |
static int |
RULE_modifier |
static int |
RULE_modifiers |
static int |
RULE_monitors_for_clause |
static int |
RULE_multexpr |
static int |
RULE_name |
static int |
RULE_name_clause |
static int |
RULE_new_expr |
static int |
RULE_nowarn_pragma |
static int |
RULE_null_ |
static int |
RULE_oldexpression |
static int |
RULE_param_decl |
static int |
RULE_param_list |
static int |
RULE_postfixexpr |
static int |
RULE_predicate |
static int |
RULE_predornot |
static int |
RULE_primaryexpr |
static int |
RULE_primarysuffix |
static int |
RULE_quantifiedvardecls |
static int |
RULE_quantifiedvariabledeclarator |
static int |
RULE_quantifier |
static int |
RULE_readable_if_clause |
static int |
RULE_referencetype |
static int |
RULE_relational_chain |
static int |
RULE_relational_lockset |
static int |
RULE_relationalexpr |
static int |
RULE_represents_clause |
static int |
RULE_requires_clause |
static int |
RULE_returns_clause |
static int |
RULE_separates_clause |
static int |
RULE_seqdefterm |
static int |
RULE_sequence |
static int |
RULE_set_statement |
static int |
RULE_shiftexpr |
static int |
RULE_signals_clause |
static int |
RULE_signals_only_clause |
static int |
RULE_spec_body |
static int |
RULE_spec_case |
static int |
RULE_specquantifiedexpression |
static int |
RULE_st_expr |
static int |
RULE_storeref |
static int |
RULE_storeRefExpr |
static int |
RULE_storeRefIntersect |
static int |
RULE_storeRefList |
static int |
RULE_storeRefUnion |
static int |
RULE_stringliteral |
static int |
RULE_super_ |
static int |
RULE_targetHeap |
static int |
RULE_termexpression |
static int |
RULE_this_ |
static int |
RULE_transactionUpdated |
static int |
RULE_true_ |
static int |
RULE_type |
static int |
RULE_typespec |
static int |
RULE_unaryexpr |
static int |
RULE_unaryexprnotplusminus |
static int |
RULE_variant_function |
static int |
RULE_when_clause |
static int |
RULE_working_space_clause |
static int |
RULE_writable_if_clause |
static java.lang.String[] |
ruleNames |
static int |
S_ESC |
static int |
SAME |
static int |
SEMI |
static int |
SEMI_TOPLEVEL |
static int |
SEMICOLON |
static int |
SEPARATES |
static int |
SEQ |
static int |
SEQ2MAP |
static int |
SEQCONCAT |
static int |
SEQDEF |
static int |
SEQEMPTY |
static int |
SEQGET |
static int |
SEQREPLACE |
static int |
SEQREVERSE |
static int |
SEQSINGLETON |
static int |
SEQSUB |
static int |
SET |
static int |
SETMINUS |
static int |
SHIFTLEFT |
static int |
SHIFTRIGHT |
static int |
SHORT |
static int |
SIGNALS |
static int |
SIGNALS_ONLY |
static int |
SINGLETON |
static int |
SL_COMMENT |
static int |
SPACE |
static int |
SPEC_BIGINT_MATH |
static int |
SPEC_JAVA_MATH |
static int |
SPEC_NAME |
static int |
SPEC_PROTECTED |
static int |
SPEC_PUBLIC |
static int |
SPEC_SAFE_MATH |
static int |
SPEC_SAVE_MATH |
static int |
SPECIAL_IDENT |
static int |
ST |
static int |
STATIC |
static int |
STATIC_INVARIANT_FOR |
static int |
STOREREF |
static int |
STRICTFP |
static int |
STRICTLY_NOTHING |
static int |
STRICTLY_PURE |
static int |
STRING_EQUAL |
static int |
STRING_LITERAL |
static int |
SUBSET |
static int |
SUCH_THAT |
static int |
SUM |
static int |
SUPER |
static int |
SYNCHRONIZED |
static int |
THIS |
static java.lang.String[] |
tokenNames
Deprecated.
Use
VOCABULARY instead. |
static int |
TRANSACTIONUPDATED |
static int |
TRANSIENT |
static int |
TRUE |
static int |
TWO_STATE |
static int |
TYPE |
static int |
TYPE_SMALL |
static int |
TYPEOF |
static int |
UNINITIALIZED |
static int |
UNION |
static int |
UNIONINF |
static int |
UNREACHABLE |
static int |
UNSIGNEDSHIFTRIGHT |
static int |
VALUES |
static org.antlr.v4.runtime.Vocabulary |
VOCABULARY |
static int |
VOID |
static int |
VOLATILE |
static int |
WHEN |
static int |
WORKING_SPACE |
static int |
WORKINGSPACE |
static int |
WRITABLE |
static int |
WS |
static int |
XOR |
Constructor and Description |
---|
JmlParser(org.antlr.v4.runtime.TokenStream input) |
addContextToParseTree, addParseListener, compileParseTreePattern, compileParseTreePattern, consume, createErrorNode, createTerminalNode, dumpDFA, enterOuterAlt, enterRecursionRule, enterRecursionRule, enterRule, exitRule, getATNWithBypassAlts, getBuildParseTree, getContext, getCurrentToken, getDFAStrings, getErrorHandler, getExpectedTokens, getExpectedTokensWithinCurrentRule, getInputStream, getInvokingContext, getNumberOfSyntaxErrors, getParseInfo, getParseListeners, getPrecedence, getRuleContext, getRuleIndex, getRuleInvocationStack, getRuleInvocationStack, getSourceName, getTokenFactory, getTokenStream, getTrimParseTree, inContext, isExpectedToken, isMatchedEOF, isTrace, match, matchWildcard, notifyErrorListeners, notifyErrorListeners, precpred, pushNewRecursionContext, removeParseListener, removeParseListeners, reset, setBuildParseTree, setContext, setErrorHandler, setInputStream, setProfile, setTokenFactory, setTokenStream, setTrace, setTrimParseTree, triggerEnterRuleEvent, triggerExitRuleEvent, unrollRecursionContexts
action, addErrorListener, getErrorHeader, getErrorListenerDispatch, getErrorListeners, getInterpreter, getRuleIndexMap, getState, getTokenErrorDisplay, getTokenType, getTokenTypeMap, removeErrorListener, removeErrorListeners, sempred, setInterpreter, setState
protected static final org.antlr.v4.runtime.dfa.DFA[] _decisionToDFA
protected static final org.antlr.v4.runtime.atn.PredictionContextCache _sharedContextCache
public static final int BODY
public static final int COMMENT
public static final int STRING_LITERAL
public static final int MODEL_BEHAVIOUR
public static final int ABSTRACT
public static final int BEHAVIOR
public static final int EXCEPTIONAL_BEHAVIOUR
public static final int BREAK_BEHAVIOR
public static final int CONTINUE_BEHAVIOR
public static final int ALSO
public static final int CODE_BIGINT_MATH
public static final int CODE_JAVA_MATH
public static final int CODE_SAFE_MATH
public static final int CONST
public static final int NATIVE
public static final int NON_NULL
public static final int NORMAL_BEHAVIOR
public static final int NO_STATE
public static final int NOWARN
public static final int NULLABLE
public static final int NULLABLE_BY_DEFAULT
public static final int SPEC_SAVE_MATH
public static final int CODE_SAVE_MATH
public static final int SPEC_BIGINT_MATH
public static final int SPEC_JAVA_MATH
public static final int SPEC_PROTECTED
public static final int SPEC_PUBLIC
public static final int GHOST
public static final int SPEC_NAME
public static final int SPEC_SAFE_MATH
public static final int STATIC
public static final int STRICTFP
public static final int STRICTLY_PURE
public static final int SYNCHRONIZED
public static final int TRANSIENT
public static final int TWO_STATE
public static final int UNINITIALIZED
public static final int UNREACHABLE
public static final int VOLATILE
public static final int PRIVATE
public static final int PROTECTED
public static final int PUBLIC
public static final int PURE
public static final int RETURN_BEHAVIOR
public static final int FINAL
public static final int MODEL
public static final int ACCESSIBLE
public static final int ASSERT
public static final int ASSUME
public static final int ASSIGNABLE
public static final int ASSIGNS
public static final int AXIOM
public static final int BREAKS
public static final int CAPTURES
public static final int CODE
public static final int CONSTRAINT
public static final int CONTINUES
public static final int DEBUG
public static final int DECREASING
public static final int DETERMINES
public static final int DIVERGES
public static final int ENSURES
public static final int FOR_EXAMPLE
public static final int HELPER
public static final int IMPLIES_THAT
public static final int IN
public static final int INITIALLY
public static final int INSTANCE
public static final int INVARIANT
public static final int LOOP_CONTRACT
public static final int LOOP_INVARIANT
public static final int LOOP_DETERMINES
public static final int LOOP_SEPARATES
public static final int MAPS
public static final int MEASURED_BY
public static final int MERGE_POINT
public static final int MERGE_PROC
public static final int MERGE_PARAMS
public static final int MODIFIABLE
public static final int MODIFIES
public static final int MONITORED
public static final int MONITORS_FOR
public static final int READABLE
public static final int REPRESENTS
public static final int REQUIRES
public static final int RETURN
public static final int RETURNS
public static final int RESPECTS
public static final int SEPARATES
public static final int SET
public static final int SIGNALS
public static final int SIGNALS_ONLY
public static final int WHEN
public static final int WORKING_SPACE
public static final int WRITABLE
public static final int JML_ML_END
public static final int WS
public static final int NEST_START
public static final int NEST_END
public static final int SL_COMMENT
public static final int JML_SL_START
public static final int JML_ML_START
public static final int ERROR_CHAR
public static final int BOOLEAN
public static final int BYTE
public static final int FALSE
public static final int INSTANCEOF
public static final int INT
public static final int LONG
public static final int NEW
public static final int NULL
public static final int SHORT
public static final int SUPER
public static final int THIS
public static final int TRUE
public static final int VOID
public static final int DEPENDS
public static final int ALLFIELDS
public static final int ALLOBJECTS
public static final int BACKUP
public static final int BEFORE
public static final int BIGINT
public static final int BSUM
public static final int BY
public static final int DECLASSIFIES
public static final int DISJOINT
public static final int DOMAIN_IMPLIES_CREATED
public static final int DURATION
public static final int ELEMTYPE
public static final int EMPTYSET
public static final int ERASES
public static final int EVERYTHING
public static final int EXCEPTION
public static final int EXISTS
public static final int FORALL
public static final int FREE
public static final int FRESH
public static final int INDEX
public static final int INDEXOF
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 LBLNEG
public static final int LBLPOS
public static final int LOCKSET
public static final int LOCSET
public static final int STOREREF
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 MIN
public static final int NEWELEMSFRESH
public static final int NEW_OBJECTS
public static final int NONNULLELEMENTS
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 NUM_OF
public static final int OLD
public static final int PERMISSION
public static final int PRE
public static final int PRODUCT
public static final int REACH
public static final int REACHLOCS
public static final int REAL
public static final int RESULT
public static final int SAME
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 SINGLETON
public static final int SPACE
public static final int STATIC_INVARIANT_FOR
public static final int STRICTLY_NOTHING
public static final int STRING_EQUAL
public static final int SUBSET
public static final int SUCH_THAT
public static final int SUM
public static final int TRANSACTIONUPDATED
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 VALUES
public static final int WORKINGSPACE
public static final int E_JML_ML_END
public static final int AND
public static final int BITWISENOT
public static final int COLON
public static final int COMMA
public static final int DIV
public static final int DOT
public static final int DOTDOT
public static final int EQUAL_SINGLE
public static final int EQV_ANTIV
public static final int EQ_NEQ
public static final int GEQ
public static final int IMPLIES
public static final int IMPLIESBACKWARD
public static final int INCLUSIVEOR
public static final int LARROW
public static final int LEQ
public static final int LOCKSET_LEQ
public static final int LOCKSET_LT
public static final int LOGICALAND
public static final int LOGICALOR
public static final int MINUS
public static final int MOD
public static final int MULT
public static final int NOT
public static final int PLUS
public static final int QUESTIONMARK
public static final int RARROW
public static final int SHIFTLEFT
public static final int SHIFTRIGHT
public static final int ST
public static final int UNSIGNEDSHIFTRIGHT
public static final int XOR
public static final int GT
public static final int LT
public static final int LPAREN
public static final int RPAREN
public static final int LBRACE
public static final int RBRACE
public static final int LBRACKET
public static final int RBRACKET
public static final int SEMI_TOPLEVEL
public static final int SEMI
public static final int BINLITERAL
public static final int OCTLITERAL
public static final int DECLITERAL
public static final int HEXLITERAL
public static final int IDENT
public static final int JML_IDENT
public static final int SPECIAL_IDENT
public static final int CHAR_LITERAL
public static final int INFORMAL_DESCRIPTION
public static final int DOC_COMMENT
public static final int C_RBRACKET
public static final int C_LBRACKET
public static final int SEMICOLON
public static final int C_LBRACE
public static final int C_RBRACE
public static final int C_LPAREN
public static final int C_RPAREN
public static final int C_STRING_LITERAL
public static final int C_COLON
public static final int C_DOT
public static final int C_COMMA
public static final int E_MEASURED_BY
public static final int E_TRANSIENT
public static final int S_ESC
public static final int RULE_classlevel_comments
public static final int RULE_classlevel_comment
public static final int RULE_classlevel_element0
public static final int RULE_classlevel_element
public static final int RULE_methodlevel_comment
public static final int RULE_methodlevel_element
public static final int RULE_modifiers
public static final int RULE_modifier
public static final int RULE_class_axiom
public static final int RULE_initially_clause
public static final int RULE_class_invariant
public static final int RULE_method_specification
public static final int RULE_also_keyword
public static final int RULE_spec_case
public static final int RULE_spec_body
public static final int RULE_clauseEOF
public static final int RULE_clause
public static final int RULE_targetHeap
public static final int RULE_ensures_clause
public static final int RULE_requires_clause
public static final int RULE_measured_by_clause
public static final int RULE_captures_clause
public static final int RULE_diverges_clause
public static final int RULE_working_space_clause
public static final int RULE_duration_clause
public static final int RULE_when_clause
public static final int RULE_accessible_clause
public static final int RULE_assignable_clause
public static final int RULE_represents_clause
public static final int RULE_separates_clause
public static final int RULE_loop_separates_clause
public static final int RULE_infflowspeclist
public static final int RULE_determines_clause
public static final int RULE_loop_determines_clause
public static final int RULE_signals_clause
public static final int RULE_signals_only_clause
public static final int RULE_breaks_clause
public static final int RULE_continues_clause
public static final int RULE_returns_clause
public static final int RULE_name_clause
public static final int RULE_field_declaration
public static final int RULE_method_declaration
public static final int RULE_method_body
public static final int RULE_param_list
public static final int RULE_param_decl
public static final int RULE_history_constraint
public static final int RULE_datagroup_clause
public static final int RULE_monitors_for_clause
public static final int RULE_readable_if_clause
public static final int RULE_writable_if_clause
public static final int RULE_in_group_clause
public static final int RULE_maps_into_clause
public static final int RULE_nowarn_pragma
public static final int RULE_debug_statement
public static final int RULE_set_statement
public static final int RULE_merge_point_statement
public static final int RULE_loop_specification
public static final int RULE_loop_invariant
public static final int RULE_variant_function
public static final int RULE_assume_statement
public static final int RULE_initialiser
public static final int RULE_block_specification
public static final int RULE_block_loop_specification
public static final int RULE_loop_contract_keyword
public static final int RULE_assert_statement
public static final int RULE_mergeparamsspec
public static final int RULE_termexpression
public static final int RULE_storeRefUnion
public static final int RULE_storeRefList
public static final int RULE_storeRefIntersect
public static final int RULE_storeref
public static final int RULE_createLocset
public static final int RULE_exprList
public static final int RULE_storeRefExpr
public static final int RULE_predornot
public static final int RULE_predicate
public static final int RULE_expressionEOF
public static final int RULE_expression
public static final int RULE_conditionalexpr
public static final int RULE_equivalenceexpr
public static final int RULE_impliesexpr
public static final int RULE_impliesforwardexpr
public static final int RULE_logicalorexpr
public static final int RULE_logicalandexpr
public static final int RULE_inclusiveorexpr
public static final int RULE_exclusiveorexpr
public static final int RULE_andexpr
public static final int RULE_equalityexpr
public static final int RULE_relationalexpr
public static final int RULE_st_expr
public static final int RULE_instance_of
public static final int RULE_relational_chain
public static final int RULE_relational_lockset
public static final int RULE_shiftexpr
public static final int RULE_additiveexpr
public static final int RULE_multexpr
public static final int RULE_unaryexpr
public static final int RULE_castexpr
public static final int RULE_unaryexprnotplusminus
public static final int RULE_postfixexpr
public static final int RULE_primaryexpr
public static final int RULE_this_
public static final int RULE_ident
public static final int RULE_inv
public static final int RULE_true_
public static final int RULE_false_
public static final int RULE_null_
public static final int RULE_transactionUpdated
public static final int RULE_primarysuffix
public static final int RULE_new_expr
public static final int RULE_array_dimensions
public static final int RULE_array_dimension
public static final int RULE_array_initializer
public static final int RULE_expressionlist
public static final int RULE_constant
public static final int RULE_javaliteral
public static final int RULE_stringliteral
public static final int RULE_charliteral
public static final int RULE_integerliteral
public static final int RULE_jmlprimary
public static final int RULE_fieldarrayaccess
public static final int RULE_fieldarrayaccess_suffix
public static final int RULE_super_
public static final int RULE_sequence
public static final int RULE_mapExpression
public static final int RULE_quantifier
public static final int RULE_infinite_union_expr
public static final int RULE_specquantifiedexpression
public static final int RULE_oldexpression
public static final int RULE_beforeexpression
public static final int RULE_bsumterm
public static final int RULE_seqdefterm
public static final int RULE_quantifiedvardecls
public static final int RULE_boundvarmodifiers
public static final int RULE_typespec
public static final int RULE_dims
public static final int RULE_type
public static final int RULE_referencetype
public static final int RULE_builtintype
public static final int RULE_name
public static final int RULE_quantifiedvariabledeclarator
public static final java.lang.String[] ruleNames
public static final org.antlr.v4.runtime.Vocabulary VOCABULARY
@Deprecated public static final java.lang.String[] tokenNames
VOCABULARY
instead.public static final java.lang.String _serializedATN
public static final org.antlr.v4.runtime.atn.ATN _ATN
@Deprecated public java.lang.String[] getTokenNames()
getTokenNames
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public org.antlr.v4.runtime.Vocabulary getVocabulary()
getVocabulary
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public java.lang.String getGrammarFileName()
getGrammarFileName
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public java.lang.String[] getRuleNames()
getRuleNames
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public java.lang.String getSerializedATN()
getSerializedATN
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public org.antlr.v4.runtime.atn.ATN getATN()
getATN
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public SyntaxErrorReporter getErrorReporter()
public final JmlParser.Classlevel_commentsContext classlevel_comments() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Classlevel_commentContext classlevel_comment() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Classlevel_element0Context classlevel_element0() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Classlevel_elementContext classlevel_element() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Methodlevel_commentContext methodlevel_comment() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Methodlevel_elementContext methodlevel_element() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ModifiersContext modifiers() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ModifierContext modifier() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Class_axiomContext class_axiom() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Initially_clauseContext initially_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Class_invariantContext class_invariant() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Method_specificationContext method_specification() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Also_keywordContext also_keyword() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Spec_caseContext spec_case() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Spec_bodyContext spec_body() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ClauseEOFContext clauseEOF() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ClauseContext clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.TargetHeapContext targetHeap() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Ensures_clauseContext ensures_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Requires_clauseContext requires_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Measured_by_clauseContext measured_by_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Captures_clauseContext captures_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Diverges_clauseContext diverges_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Working_space_clauseContext working_space_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Duration_clauseContext duration_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.When_clauseContext when_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Accessible_clauseContext accessible_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Assignable_clauseContext assignable_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Represents_clauseContext represents_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Separates_clauseContext separates_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Loop_separates_clauseContext loop_separates_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.InfflowspeclistContext infflowspeclist() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Determines_clauseContext determines_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Loop_determines_clauseContext loop_determines_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Signals_clauseContext signals_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Signals_only_clauseContext signals_only_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Breaks_clauseContext breaks_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Continues_clauseContext continues_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Returns_clauseContext returns_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Name_clauseContext name_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Field_declarationContext field_declaration() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Method_declarationContext method_declaration() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Method_bodyContext method_body() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Param_listContext param_list() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Param_declContext param_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.History_constraintContext history_constraint() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Datagroup_clauseContext datagroup_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Monitors_for_clauseContext monitors_for_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Readable_if_clauseContext readable_if_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Writable_if_clauseContext writable_if_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.In_group_clauseContext in_group_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Maps_into_clauseContext maps_into_clause() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Nowarn_pragmaContext nowarn_pragma() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Debug_statementContext debug_statement() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Set_statementContext set_statement() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Merge_point_statementContext merge_point_statement() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Loop_specificationContext loop_specification() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Loop_invariantContext loop_invariant() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Variant_functionContext variant_function() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Assume_statementContext assume_statement() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.InitialiserContext initialiser() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Block_specificationContext block_specification() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Block_loop_specificationContext block_loop_specification() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Loop_contract_keywordContext loop_contract_keyword() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Assert_statementContext assert_statement() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.MergeparamsspecContext mergeparamsspec() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.TermexpressionContext termexpression() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.StoreRefUnionContext storeRefUnion() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.StoreRefListContext storeRefList() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.StoreRefIntersectContext storeRefIntersect() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.StorerefContext storeref() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.CreateLocsetContext createLocset() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ExprListContext exprList() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.StoreRefExprContext storeRefExpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.PredornotContext predornot() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.PredicateContext predicate() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ExpressionEOFContext expressionEOF() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ExpressionContext expression() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ConditionalexprContext conditionalexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.EquivalenceexprContext equivalenceexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ImpliesexprContext impliesexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ImpliesforwardexprContext impliesforwardexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.LogicalorexprContext logicalorexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.LogicalandexprContext logicalandexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.InclusiveorexprContext inclusiveorexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ExclusiveorexprContext exclusiveorexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.AndexprContext andexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.EqualityexprContext equalityexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.RelationalexprContext relationalexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.St_exprContext st_expr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Instance_ofContext instance_of() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Relational_chainContext relational_chain() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Relational_locksetContext relational_lockset() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ShiftexprContext shiftexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.AdditiveexprContext additiveexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.MultexprContext multexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.UnaryexprContext unaryexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.CastexprContext castexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.UnaryexprnotplusminusContext unaryexprnotplusminus() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.PostfixexprContext postfixexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.PrimaryexprContext primaryexpr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.This_Context this_() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.IdentContext ident() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.InvContext inv() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.True_Context true_() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.False_Context false_() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Null_Context null_() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.TransactionUpdatedContext transactionUpdated() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.PrimarysuffixContext primarysuffix() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.New_exprContext new_expr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Array_dimensionsContext array_dimensions() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Array_dimensionContext array_dimension() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Array_initializerContext array_initializer() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ExpressionlistContext expressionlist() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ConstantContext constant() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.JavaliteralContext javaliteral() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.StringliteralContext stringliteral() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.CharliteralContext charliteral() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.IntegerliteralContext integerliteral() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.JmlprimaryContext jmlprimary() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.FieldarrayaccessContext fieldarrayaccess() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Fieldarrayaccess_suffixContext fieldarrayaccess_suffix() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Super_Context super_() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.SequenceContext sequence() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.MapExpressionContext mapExpression() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.QuantifierContext quantifier() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.Infinite_union_exprContext infinite_union_expr() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.SpecquantifiedexpressionContext specquantifiedexpression() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.OldexpressionContext oldexpression() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.BeforeexpressionContext beforeexpression() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.BsumtermContext bsumterm() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.SeqdeftermContext seqdefterm() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.QuantifiedvardeclsContext quantifiedvardecls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.BoundvarmodifiersContext boundvarmodifiers() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.TypespecContext typespec() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.DimsContext dims() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.TypeContext type() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.ReferencetypeContext referencetype() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.BuiltintypeContext builtintype() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.NameContext name() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final JmlParser.QuantifiedvariabledeclaratorContext quantifiedvariabledeclarator() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
Copyright © 2003-2019 The KeY-Project.