Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Class JmlParser

java.lang.Object
  extended byantlr.Parser
      extended byantlr.LLkParser
          extended byorg.jmlspecs.checker.JmlParser
All Implemented Interfaces:
JmlTokenTypes
public class JmlParser
extends antlr.LLkParser
implements JmlTokenTypes

Nested Class Summary
(package private) static class JmlParser.TypeBooleanPair
           
(package private) static class JmlParser.TypeWeaklyList
          This nested class represents a list of implemented interfaces for a class declaration (or extends interfaces for an interface declaration) and whether they are implemented (or extended) weakly.
 
Field Summary
static String[] _tokenNames
           
static antlr.collections.impl.BitSet _tokenSet_0
           
static antlr.collections.impl.BitSet _tokenSet_1
           
static antlr.collections.impl.BitSet _tokenSet_10
           
static antlr.collections.impl.BitSet _tokenSet_11
           
static antlr.collections.impl.BitSet _tokenSet_12
           
static antlr.collections.impl.BitSet _tokenSet_13
           
static antlr.collections.impl.BitSet _tokenSet_14
           
static antlr.collections.impl.BitSet _tokenSet_15
           
static antlr.collections.impl.BitSet _tokenSet_16
           
static antlr.collections.impl.BitSet _tokenSet_17
           
static antlr.collections.impl.BitSet _tokenSet_18
           
static antlr.collections.impl.BitSet _tokenSet_19
           
static antlr.collections.impl.BitSet _tokenSet_2
           
static antlr.collections.impl.BitSet _tokenSet_20
           
static antlr.collections.impl.BitSet _tokenSet_21
           
static antlr.collections.impl.BitSet _tokenSet_22
           
static antlr.collections.impl.BitSet _tokenSet_23
           
static antlr.collections.impl.BitSet _tokenSet_24
           
static antlr.collections.impl.BitSet _tokenSet_25
           
static antlr.collections.impl.BitSet _tokenSet_26
           
static antlr.collections.impl.BitSet _tokenSet_27
           
static antlr.collections.impl.BitSet _tokenSet_28
           
static antlr.collections.impl.BitSet _tokenSet_29
           
static antlr.collections.impl.BitSet _tokenSet_3
           
static antlr.collections.impl.BitSet _tokenSet_30
           
static antlr.collections.impl.BitSet _tokenSet_31
           
static antlr.collections.impl.BitSet _tokenSet_32
           
static antlr.collections.impl.BitSet _tokenSet_33
           
static antlr.collections.impl.BitSet _tokenSet_34
           
static antlr.collections.impl.BitSet _tokenSet_35
           
static antlr.collections.impl.BitSet _tokenSet_36
           
static antlr.collections.impl.BitSet _tokenSet_37
           
static antlr.collections.impl.BitSet _tokenSet_38
           
static antlr.collections.impl.BitSet _tokenSet_39
           
static antlr.collections.impl.BitSet _tokenSet_4
           
static antlr.collections.impl.BitSet _tokenSet_40
           
static antlr.collections.impl.BitSet _tokenSet_41
           
static antlr.collections.impl.BitSet _tokenSet_42
           
static antlr.collections.impl.BitSet _tokenSet_43
           
static antlr.collections.impl.BitSet _tokenSet_44
           
static antlr.collections.impl.BitSet _tokenSet_45
           
static antlr.collections.impl.BitSet _tokenSet_46
           
static antlr.collections.impl.BitSet _tokenSet_5
           
static antlr.collections.impl.BitSet _tokenSet_6
           
static antlr.collections.impl.BitSet _tokenSet_7
           
static antlr.collections.impl.BitSet _tokenSet_8
           
static antlr.collections.impl.BitSet _tokenSet_9
           
private  JExpressionFactory exprFactory
           
private  boolean isInModelProgram
           
private  boolean isRefinedCUnit
           
private  int unmatchedTypeLT
           
private  ParserUtility utility
          Instances of JmlParser delegate to utility.
 
Fields inherited from class antlr.LLkParser
 
Fields inherited from class antlr.Parser
astFactory, inputState, returnAST, tokenNames, tokenTypeToASTClassMap, traceDepth
 
Fields inherited from interface org.jmlspecs.checker.JmlTokenTypes
AFFIRM, ASSIGN, AT, BACKWARD_IMPLIES, BAND, BAND_ASSIGN, BNOT, BOR, BOR_ASSIGN, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CHARACTER_LITERAL, COLON, COMMA, DEC, DOT, DOT_DOT, EOF, EQUAL, EQUIV, GE, GT, IDENT, IMPLIES, INC, INFORMAL_DESC, INTEGER_LITERAL, JAVADOC_OPEN, L_ARROW, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LITERAL__nowarn, LITERAL__nowarn_op, LITERAL__warn, LITERAL__warn_op, LITERAL_abrupt_behavior, LITERAL_abrupt_behaviour, LITERAL_abstract, LITERAL_accessible, LITERAL_accessible_redundantly, LITERAL_also, LITERAL_assert, LITERAL_assert_redundantly, LITERAL_assignable, LITERAL_assignable_redundantly, LITERAL_assume, LITERAL_assume_redundantly, LITERAL_axiom, LITERAL_behavior, LITERAL_behaviour, LITERAL_boolean, LITERAL_break, LITERAL_breaks, LITERAL_breaks_redundantly, LITERAL_BS_bigint, LITERAL_BS_bigint_math, LITERAL_BS_duration, LITERAL_BS_elemtype, LITERAL_BS_everything, LITERAL_BS_exists, LITERAL_BS_forall, LITERAL_BS_fresh, LITERAL_BS_into, LITERAL_BS_invariant_for, LITERAL_BS_is_initialized, LITERAL_BS_java_math, LITERAL_BS_lblneg, LITERAL_BS_lblpos, LITERAL_BS_lockset, LITERAL_BS_max, LITERAL_BS_min, LITERAL_BS_nonnullelements, LITERAL_BS_not_assigned, LITERAL_BS_not_modified, LITERAL_BS_not_specified, LITERAL_BS_nothing, LITERAL_BS_nowarn, LITERAL_BS_nowarn_op, LITERAL_BS_num_of, LITERAL_BS_old, LITERAL_BS_only_accessed, LITERAL_BS_only_assigned, LITERAL_BS_only_called, LITERAL_BS_only_captured, LITERAL_BS_other, LITERAL_BS_pre, LITERAL_BS_product, LITERAL_BS_reach, LITERAL_BS_real, LITERAL_BS_result, LITERAL_BS_safe_math, LITERAL_BS_same, LITERAL_BS_space, LITERAL_BS_such_that, LITERAL_BS_sum, LITERAL_BS_TYPE, LITERAL_BS_type, LITERAL_BS_typeof, LITERAL_BS_warn, LITERAL_BS_warn_op, LITERAL_BS_working_space, LITERAL_byte, LITERAL_callable, LITERAL_callable_redundantly, LITERAL_captures, LITERAL_captures_redundantly, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_choose, LITERAL_choose_if, LITERAL_class, LITERAL_code, LITERAL_code_bigint_math, LITERAL_code_contract, LITERAL_code_java_math, LITERAL_code_safe_math, LITERAL_const, LITERAL_constraint, LITERAL_constraint_redundantly, LITERAL_constructor, LITERAL_continue, LITERAL_continues, LITERAL_continues_redundantly, LITERAL_debug, LITERAL_decreases, LITERAL_decreases_redundantly, LITERAL_decreasing, LITERAL_decreasing_redundantly, LITERAL_default, LITERAL_diverges, LITERAL_diverges_redundantly, LITERAL_do, LITERAL_double, LITERAL_duration, LITERAL_duration_redundantly, LITERAL_else, LITERAL_ensures, LITERAL_ensures_redundantly, LITERAL_example, LITERAL_exceptional_behavior, LITERAL_exceptional_behaviour, LITERAL_exceptional_example, LITERAL_exsures, LITERAL_exsures_redundantly, LITERAL_extends, LITERAL_false, LITERAL_field, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_for_example, LITERAL_forall, LITERAL_ghost, LITERAL_goto, LITERAL_helper, LITERAL_hence_by, LITERAL_hence_by_redundantly, LITERAL_if, LITERAL_implements, LITERAL_implies_that, LITERAL_import, LITERAL_in, LITERAL_in_redundantly, LITERAL_initializer, LITERAL_initially, LITERAL_instance, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_invariant, LITERAL_invariant_redundantly, LITERAL_long, LITERAL_loop_invariant, LITERAL_loop_invariant_redundantly, LITERAL_maintaining, LITERAL_maintaining_redundantly, LITERAL_maps, LITERAL_maps_redundantly, LITERAL_measured_by, LITERAL_measured_by_redundantly, LITERAL_method, LITERAL_model, LITERAL_model_program, LITERAL_modifiable, LITERAL_modifiable_redundantly, LITERAL_modifies, LITERAL_modifies_redundantly, LITERAL_monitored, LITERAL_monitors_for, LITERAL_native, LITERAL_new, LITERAL_non_null, LITERAL_non_null_by_default, LITERAL_normal_behavior, LITERAL_normal_behaviour, LITERAL_normal_example, LITERAL_null, LITERAL_nullable, LITERAL_nullable_by_default, LITERAL_old, LITERAL_or, LITERAL_package, LITERAL_peer, LITERAL_post, LITERAL_post_redundantly, LITERAL_pre, LITERAL_pre_redundantly, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_pure, LITERAL_query, LITERAL_readable, LITERAL_readonly, LITERAL_refine, LITERAL_refines, LITERAL_rep, LITERAL_represents, LITERAL_represents_redundantly, LITERAL_requires, LITERAL_requires_redundantly, LITERAL_resend, LITERAL_return, LITERAL_returns, LITERAL_returns_redundantly, LITERAL_secret, LITERAL_set, LITERAL_short, LITERAL_signals, LITERAL_signals_only, LITERAL_signals_only_redundantly, LITERAL_signals_redundantly, LITERAL_spec_bigint_math, LITERAL_spec_java_math, LITERAL_spec_protected, LITERAL_spec_public, LITERAL_spec_safe_math, LITERAL_static, LITERAL_static_initializer, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_U_peer, LITERAL_U_readonly, LITERAL_U_rep, LITERAL_uninitialized, LITERAL_unreachable, LITERAL_void, LITERAL_volatile, LITERAL_weakly, LITERAL_when, LITERAL_when_redundantly, LITERAL_while, LITERAL_working_space, LITERAL_working_space_redundantly, LITERAL_writable, LNOT, LOR, LPAREN, LT, MINUS, MINUS_ASSIGN, NOT_EQUAL, NOT_EQUIV, NULL_TREE_LOOKAHEAD, PERCENT, PERCENT_ASSIGN, PLUS, PLUS_ASSIGN, QUESTION, R_ARROW, RBRACK, RCURLY, REAL_LITERAL, RPAREN, SEMI, SL, SL_ASSIGN, SLASH, SLASH_ASSIGN, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STRING_LITERAL, SUBTYPE_OF, VBAR_RCURLY
 
Constructor Summary
  JmlParser(antlr.ParserSharedInputState state)
           
  JmlParser(antlr.TokenBuffer tokenBuf)
           
protected JmlParser(antlr.TokenBuffer tokenBuf, int k)
           
  JmlParser(antlr.TokenStream lexer)
           
protected JmlParser(antlr.TokenStream lexer, int k)
           
  JmlParser(Main compiler, antlr.TokenStream lexer, ParsingController parsingController, boolean allowGeneric, boolean allowMultiJava, boolean allowRelaxedMultiJava, boolean allowUniverseKeywords)
           
  JmlParser(Main compiler, antlr.TokenStream lexer, ParsingController parsingController, boolean allowGeneric, boolean allowMultiJava, boolean allowRelaxedMultiJava, boolean allowUniverseKeywords, boolean isRefinedCUnit)
           
 
Method Summary
 PositionedError beautifyParserError(antlr.ANTLRException e)
          Returns an exception from our exception hierarchy by wrapping the ANTLR excepton.
private  CParseClassContext getParseClassContext()
          Generates the appropriate data structure for buffering class members during parsing.
static boolean isPrivacyOrNull(long mod)
          Returns true if the argument mod is one of the privacy modifiers (i.e., public, protected or privacy) or null (= 0).
 JSwitchLabel jACase()
           
 JExpression jAdditiveExpression()
           
 JExpression jAndExpression()
           
 JExpression[] jArgList()
           
 JArrayInitializer jArrayInitializer()
           
 JAssertStatement jAssertStatement()
           
 JExpression jAssignmentExpression()
           
 JBreakStatement jBreakStatement()
           
 CType jBuiltInType()
           
 CType jBuiltInTypeSpec(CUniverse array_univ)
           
 JSwitchGroup jCasesGroup()
           
 void jClassBlock(CParseClassContext context)
           
 JClassDeclarationType jClassDefinition(long mods, antlr.Token startToken)
           
 CClassType jClassTypeSpec(CUniverse elem_univ, CUniverse array_univ)
           
 JCompilationUnitType jCompilationUnit()
           
 JStatement[] jCompoundStatement(ParsingController.TokenWrapper declEnd)
           
 JExpression jConditionalExpression()
           
 JExpression jConstant()
           
 JContinueStatement jContinueStatement()
           
 JVariableDeclarationStatement jDeclaration()
           
 JDoStatement jDoStatement()
           
 JExpression jEqualityExpression()
           
 JExpression jExclusiveOrExpression()
           
 JExpression jExpression()
           
 JExpression[] jExpressionList()
           
 JExpression jForCond()
           
 JStatement jForInit()
           
 JExpressionListStatement jForIter()
           
 JForStatement jForStatement()
           
 JCatchClause jHandler()
           
 String jIdentifier()
           
 JIfStatement jIfStatement()
           
 JmlParser.TypeWeaklyList jImplementsClause()
           
 void jImportDefinition(CParseCompilationUnitContext cunit)
           
 JExpression jInclusiveOrExpression()
           
 JExpression jInitializer()
           
 JInterfaceDeclarationType jInterfaceDefinition(long mods, antlr.Token startToken)
           
 JmlParser.TypeWeaklyList jInterfaceExtends()
           
 JLabeledStatement jLabeledStatement()
           
 JExpression jLogicalAndExpression()
           
 JExpression jLogicalOrExpression()
           
 JStatement jLoopStatement()
           
 void jMember(CParseClassContext context)
           
 JmlAbruptSpecBody jmlAbruptSpecBody()
           
 JmlAbruptSpecCase jmlAbruptSpecCase()
           
 JmlGeneralSpecCase[] jmlAbruptSpecCaseSeq()
           
 JmlAccessibleClause jmlAccessibleClause()
           
 JmlAssertStatement jmlAssertStatement()
           
 JmlAssignableClause jmlAssignableClause()
           
 JmlAssumeStatement jmlAssumeStatement()
           
 JExpression jmlBackwardImpliesExpression()
           
 JmlBreaksClause jmlBreaksClause()
           
 CType jmlBuiltInType()
           
 JmlCallableClause jmlCallableClause()
           
 JmlCapturesClause jmlCapturesClause()
           
 JmlCodeContract jmlCodeContract(long mods)
           
 JmlContinuesClause jmlContinuesClause()
           
 void jmlDataGroupClause(JmlDataGroupAccumulator self)
           
 JmlDebugStatement jmlDebugStatement()
           
 void jmlDeclaration(CParseClassContext context, long mods, antlr.Token startToken)
           
 JmlDivergesClause jmlDivergesClause()
           
 JmlDurationClause jmlDurationClause()
           
 JmlEnsuresClause jmlEnsuresClause()
           
 JExpression jmlEquivalenceExpression()
           
 JmlExample jmlExample()
           
 JmlExample[] jmlExamples()
           
 JmlExceptionalSpecBody jmlExceptionalSpecBody()
           
 JmlExceptionalSpecCase jmlExceptionalSpecCase()
           
 JmlGeneralSpecCase[] jmlExceptionalSpecCaseSeq()
           
 JmlExtendingSpecification jmlExtendingSpecification()
           
 JmlForAllVarDecl jmlForAllVarDecl()
           
 JExpression jmlForwardImpliesExpression()
           
 JmlGenericSpecBody jmlGenericSpecBody(boolean isInSpecStatement)
           
 JmlGenericSpecCase jmlGenericSpecCase(boolean isInSpecStatement)
           
 JmlGenericSpecCase[] jmlGenericSpecCaseSeq(boolean isInSpecStatement)
           
 JmlStoreRefExpression[] jmlGroupList()
           
 JmlStoreRefExpression jmlGroupName()
           
 JmlGuardedStatement jmlGuardedStatement()
           
 JmlGuardedStatement[] jmlGuardedStatements()
           
 JmlHeavyweightSpec jmlHeavyweightSpec(long mods)
           
 JmlHenceByStatement jmlHenceByStatement()
           
 JmlSpecCase[] jmlImplications()
           
 JExpression jmlImpliesExpression()
           
 JmlInvariantStatement jmlInvariantStatement()
           
 JmlLetVarDecl jmlLocalSpecVarDecl()
           
 JmlLoopInvariant jmlLoopInvariant()
           
 JmlLoopInvariant[] jmlLoopInvariantList()
           
 void jmlMapsMemberRefExpr(ArrayList namesV)
           
 JmlStoreRefExpression jmlMapsReference()
           
 JExpression jmlMathModeExpression()
           
 JmlMeasuredClause jmlMeasuredClause()
           
 JmlMethodName jmlMethodName()
           
 JmlMethodNameList jmlMethodNameList()
           
 JmlMethodSpecification jmlMethodSpecification(long mods)
           
 JmlModelProgram jmlModelProgram(long mods)
           
 JmlModelProgStatement jmlModelProgStatement()
           
 long jmlModifier()
           
 JmlNondetChoiceStatement jmlNondeterministicChoice()
           
 JmlNondetIfStatement jmlNondeterministicIf()
           
 long jmlNonNullNullityModifier()
           
 JmlNormalSpecBody jmlNormalSpecBody()
           
 JmlNormalSpecCase jmlNormalSpecCase()
           
 JmlGeneralSpecCase[] jmlNormalSpecCaseSeq()
           
 long jmlNullityModifier()
           
 CType jmlParamDisambig()
           
 CType[] jmlParamDisambigList()
           
 JmlPredicate jmlPredicate()
           
 JExpression jmlPrimary()
           
 JmlVariableDefinition[] jmlQuantifiedVarDecls()
           
 JmlRedundantSpec jmlRedundantSpec()
           
 JmlRefinePrefix jmlRefinePrefix()
           
 JmlRequiresClause jmlRequiresClause()
           
 JmlReturnsClause jmlReturnsClause()
           
 JExpression jmlSetComprehension(CType type)
           
 JmlSetStatement jmlSetStatement()
           
 JmlSignalsClause jmlSignalsClause()
           
 JmlSignalsOnlyClause jmlSignalsOnlyClause()
           
 JArrayInitializer jmlSpecArrayInitializer()
           
 JmlName jmlSpecArrayRefExpr(TokenReference sourceRef)
           
 JmlSpecBodyClause[] jmlSpecBody()
           
 JmlSpecBodyClause jmlSpecBodyClause()
           
 JmlSpecCase jmlSpecCase(long mods)
           
 JmlSpecCase[] jmlSpecCaseSeq(long mods)
           
 JmlSpecExpression jmlSpecExpression()
           
 JmlSpecExpression[] jmlSpecExpressionList()
           
 JmlRequiresClause[] jmlSpecHeader()
           
 JmlSpecification jmlSpecification(long mods)
           
 JExpression jmlSpecInitializer()
           
 JmlSpecQuantifiedExpression jmlSpecQuantifiedExprRest(TokenReference sourceRef)
           
 JmlSpecStatement jmlSpecStatement()
           
 JmlSpecVarDecl[] jmlSpecVarDecls()
           
 JVariableDefinition jmlSpecVariableDeclarator(long mods, CType type)
           
 JVariableDefinition[] jmlSpecVariableDeclarators(long mods, CType type)
           
 JmlStoreRef jmlStoreRef()
           
 JmlStoreRefExpression jmlStoreRefExpression()
           
 JmlStoreRefKeyword jmlStoreRefKeyword()
           
 JmlStoreRef[] jmlStoreRefList()
           
 JmlName jmlStoreRefNameSuffix()
           
 CUniverse jmlUniversePeerSpec()
           
 CUniverse jmlUniverseReadonlySpec()
           
 CUniverse jmlUniverseRepSpec()
           
 JmlUnreachableStatement jmlUnreachableStatement()
           
 JmlVariantFunction jmlVariantFunction()
           
 JmlVariantFunction[] jmlVariantFunctionList()
           
 JExpression jmlWarnExpression()
           
 JmlWhenClause jmlWhenClause()
           
 JmlWorkingSpaceClause jmlWorkingSpaceClause()
           
 long jModifier()
           
 long jModifiers()
           
 JExpression jMultiplicativeExpression()
           
 CClassType[] jNameList()
           
 void jNameWeaklyList(JmlParser.TypeWeaklyList self)
           
 JExpression[] jNewArrayDeclarator()
           
 JExpression jNewExpression(JExpression expr)
           
 JPackageName jPackageDefinition()
           
 JFormalParameter jParameterDeclaration(int desc)
           
 JFormalParameter[] jParameterDeclarationList(int desc)
           
 CClassType[] jParameterizedClassTypeList()
           
 JExpression jParenthesizedExpression()
           
 JExpression jParenthesizedExpressionRest(TokenReference sourceRef)
           
 JExpression jPostfixExpression()
           
 JExpression jPrimaryExpression()
           
 JExpression jRelationalExpression()
           
 JReturnStatement jReturnStatement()
           
 JExpression jShiftExpression()
           
 JLoopStatement jSimpleLoopStatement()
           
 JStatement jStatement()
           
 JmlParser.TypeBooleanPair jSuperClassClause()
           
 JExpression jSuperSuffix(JSuperExpression supExpr)
           
 JSwitchStatement jSwitchStatement()
           
 JSynchronizedStatement jSynchronizedStatement()
           
 CClassType[] jThrowsClause()
           
 JThrowStatement jThrowStatement()
           
 JStatement jTryBlock()
           
 CType jType(CUniverse elem_univ)
           
 void jTypeDefinition(CParseCompilationUnitContext context, long mods, antlr.Token startToken)
           
 CClassType jTypeName(CUniverse elem_univ)
           
 CClassType jTypeParameter()
           
 CType jTypeSpec()
           
 CTypeVariable jTypeVariableDeclaration()
           
 CTypeVariable[] jTypeVariableDeclarationList()
           
 JExpression jUnaryExpression()
           
 JExpression jUnaryExpressionNotPlusMinus()
           
 CUniverse jUniverseExceptionSpec()
           
 CUniverse jUniversePeerSpec()
           
 CUniverse jUniverseReadonlySpec()
           
 CUniverse jUniverseRepSpec()
           
 CUniverse jUniverseSpec()
           
 CUniverse jUniverseType()
           
 CType jValueSpecializer(CType type, TokenReference sourceRef)
           
 JVariableDefinition jVariableDeclarator(long mods, CType type)
           
 JVariableDefinition[] jVariableDefinitions(long mods, CType type)
           
 JExpression jVarInitializer()
           
 JWhileStatement jWhileStatement()
           
 CClassType jWildCard()
           
 CClassType jWildcardBound()
           
 CType mjBuiltInType()
           
 CType mjExternalClassTypeSpec()
           
 long mjModifier()
           
 JExpression mjOrJmlUnaryExpressionNotPlusMinus()
           
 JExpression mjPrimaryExpression()
           
 JExpression mjResendSuffix(JExpression prefix)
           
 JStatement mjStatement()
           
 void mjTopLevelDeclaration(CParseCompilationUnitContext context, long mods, antlr.Token startToken)
           
 void mjTopLevelDefinition(CParseCompilationUnitContext context)
           
 MJTopLevelMethodDeclaration mjTopLevelMethodDeclaration(long mods, antlr.Token startToken)
           
 CType mjTypeSpec()
           
 CUniverse mjUniverseImplicitPeerSpec()
           
 CUniverse mjUniverseImplicitReadonlySpec()
           
 CUniverse mjUniversePeerSpec()
           
 CUniverse mjUniverseReadonlySpec()
           
 CUniverse mjUniverseRepSpec()
           
 JExpression mjWarnExpression()
           
private static long[] mk_tokenSet_0()
           
private static long[] mk_tokenSet_1()
           
private static long[] mk_tokenSet_10()
           
private static long[] mk_tokenSet_11()
           
private static long[] mk_tokenSet_12()
           
private static long[] mk_tokenSet_13()
           
private static long[] mk_tokenSet_14()
           
private static long[] mk_tokenSet_15()
           
private static long[] mk_tokenSet_16()
           
private static long[] mk_tokenSet_17()
           
private static long[] mk_tokenSet_18()
           
private static long[] mk_tokenSet_19()
           
private static long[] mk_tokenSet_2()
           
private static long[] mk_tokenSet_20()
           
private static long[] mk_tokenSet_21()
           
private static long[] mk_tokenSet_22()
           
private static long[] mk_tokenSet_23()
           
private static long[] mk_tokenSet_24()
           
private static long[] mk_tokenSet_25()
           
private static long[] mk_tokenSet_26()
           
private static long[] mk_tokenSet_27()
           
private static long[] mk_tokenSet_28()
           
private static long[] mk_tokenSet_29()
           
private static long[] mk_tokenSet_3()
           
private static long[] mk_tokenSet_30()
           
private static long[] mk_tokenSet_31()
           
private static long[] mk_tokenSet_32()
           
private static long[] mk_tokenSet_33()
           
private static long[] mk_tokenSet_34()
           
private static long[] mk_tokenSet_35()
           
private static long[] mk_tokenSet_36()
           
private static long[] mk_tokenSet_37()
           
private static long[] mk_tokenSet_38()
           
private static long[] mk_tokenSet_39()
           
private static long[] mk_tokenSet_4()
           
private static long[] mk_tokenSet_40()
           
private static long[] mk_tokenSet_41()
           
private static long[] mk_tokenSet_42()
           
private static long[] mk_tokenSet_43()
           
private static long[] mk_tokenSet_44()
           
private static long[] mk_tokenSet_45()
           
private static long[] mk_tokenSet_46()
           
private static long[] mk_tokenSet_5()
           
private static long[] mk_tokenSet_6()
           
private static long[] mk_tokenSet_7()
           
private static long[] mk_tokenSet_8()
           
private static long[] mk_tokenSet_9()
           
 boolean verifyAbruptSpecBody(JmlSpecBodyClause[] clauses)
          Returns true if all elements of the argument are abrupt spec body clauses; otherwise, print an appropriate error message and return false
 boolean verifyExceptionalSpecBody(JmlSpecBodyClause[] clauses)
          Returns true if all elements of the argument are exceptional spec body clauses; otherwise, print an appropriate error message and return false
 boolean verifyNormalSpecBody(JmlSpecBodyClause[] clauses)
          Returns true if all elements of the argument are normal spec body clauses; otherwise, print an appropriate error message and return false
 boolean verifySimpleSpecBody(JmlSpecBodyClause[] clauses)
          Returns true if all elements of the argument are simple spec body clauses; otherwise, print an appropriate error message and return false
 boolean verifySimpleSpecStatementBody(JmlSpecBodyClause[] clauses)
          Returns true if all elements of the argument are simple spec statement body clauses; otherwise, print an appropriate error message and return false
 
Methods inherited from class antlr.LLkParser
consume, LA, LT, traceIn, traceOut
 
Methods inherited from class antlr.Parser
addMessageListener, addParserListener, addParserMatchListener, addParserTokenListener, addSemanticPredicateListener, addSyntacticPredicateListener, addTraceListener, consumeUntil, consumeUntil, defaultDebuggingSetup, getAST, getASTFactory, getFilename, getInputState, getTokenName, getTokenNames, getTokenTypeToASTClassMap, isDebugMode, mark, match, match, matchNot, panic, removeMessageListener, removeParserListener, removeParserMatchListener, removeParserTokenListener, removeSemanticPredicateListener, removeSyntacticPredicateListener, removeTraceListener, reportError, reportError, reportWarning, rewind, setASTFactory, setASTNodeClass, setASTNodeType, setDebugMode, setFilename, setIgnoreInvalidDebugCalls, setInputState, setTokenBuffer, traceIndent
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

utility

private ParserUtility utility
Instances of JmlParser delegate to utility.

isInModelProgram

private boolean isInModelProgram

isRefinedCUnit

private boolean isRefinedCUnit

exprFactory

private JExpressionFactory exprFactory

unmatchedTypeLT

private int unmatchedTypeLT

_tokenNames

public static final String[] _tokenNames

_tokenSet_0

public static final antlr.collections.impl.BitSet _tokenSet_0

_tokenSet_1

public static final antlr.collections.impl.BitSet _tokenSet_1

_tokenSet_2

public static final antlr.collections.impl.BitSet _tokenSet_2

_tokenSet_3

public static final antlr.collections.impl.BitSet _tokenSet_3

_tokenSet_4

public static final antlr.collections.impl.BitSet _tokenSet_4

_tokenSet_5

public static final antlr.collections.impl.BitSet _tokenSet_5

_tokenSet_6

public static final antlr.collections.impl.BitSet _tokenSet_6

_tokenSet_7

public static final antlr.collections.impl.BitSet _tokenSet_7

_tokenSet_8

public static final antlr.collections.impl.BitSet _tokenSet_8

_tokenSet_9

public static final antlr.collections.impl.BitSet _tokenSet_9

_tokenSet_10

public static final antlr.collections.impl.BitSet _tokenSet_10

_tokenSet_11

public static final antlr.collections.impl.BitSet _tokenSet_11

_tokenSet_12

public static final antlr.collections.impl.BitSet _tokenSet_12

_tokenSet_13

public static final antlr.collections.impl.BitSet _tokenSet_13

_tokenSet_14

public static final antlr.collections.impl.BitSet _tokenSet_14

_tokenSet_15

public static final antlr.collections.impl.BitSet _tokenSet_15

_tokenSet_16

public static final antlr.collections.impl.BitSet _tokenSet_16

_tokenSet_17

public static final antlr.collections.impl.BitSet _tokenSet_17

_tokenSet_18

public static final antlr.collections.impl.BitSet _tokenSet_18

_tokenSet_19

public static final antlr.collections.impl.BitSet _tokenSet_19

_tokenSet_20

public static final antlr.collections.impl.BitSet _tokenSet_20

_tokenSet_21

public static final antlr.collections.impl.BitSet _tokenSet_21

_tokenSet_22

public static final antlr.collections.impl.BitSet _tokenSet_22

_tokenSet_23

public static final antlr.collections.impl.BitSet _tokenSet_23

_tokenSet_24

public static final antlr.collections.impl.BitSet _tokenSet_24

_tokenSet_25

public static final antlr.collections.impl.BitSet _tokenSet_25

_tokenSet_26

public static final antlr.collections.impl.BitSet _tokenSet_26

_tokenSet_27

public static final antlr.collections.impl.BitSet _tokenSet_27

_tokenSet_28

public static final antlr.collections.impl.BitSet _tokenSet_28

_tokenSet_29

public static final antlr.collections.impl.BitSet _tokenSet_29

_tokenSet_30

public static final antlr.collections.impl.BitSet _tokenSet_30

_tokenSet_31

public static final antlr.collections.impl.BitSet _tokenSet_31

_tokenSet_32

public static final antlr.collections.impl.BitSet _tokenSet_32

_tokenSet_33

public static final antlr.collections.impl.BitSet _tokenSet_33

_tokenSet_34

public static final antlr.collections.impl.BitSet _tokenSet_34

_tokenSet_35

public static final antlr.collections.impl.BitSet _tokenSet_35

_tokenSet_36

public static final antlr.collections.impl.BitSet _tokenSet_36

_tokenSet_37

public static final antlr.collections.impl.BitSet _tokenSet_37

_tokenSet_38

public static final antlr.collections.impl.BitSet _tokenSet_38

_tokenSet_39

public static final antlr.collections.impl.BitSet _tokenSet_39

_tokenSet_40

public static final antlr.collections.impl.BitSet _tokenSet_40

_tokenSet_41

public static final antlr.collections.impl.BitSet _tokenSet_41

_tokenSet_42

public static final antlr.collections.impl.BitSet _tokenSet_42

_tokenSet_43

public static final antlr.collections.impl.BitSet _tokenSet_43

_tokenSet_44

public static final antlr.collections.impl.BitSet _tokenSet_44

_tokenSet_45

public static final antlr.collections.impl.BitSet _tokenSet_45

_tokenSet_46

public static final antlr.collections.impl.BitSet _tokenSet_46
Constructor Detail

JmlParser

public JmlParser(Main compiler,
                 antlr.TokenStream lexer,
                 ParsingController parsingController,
                 boolean allowGeneric,
                 boolean allowMultiJava,
                 boolean allowRelaxedMultiJava,
                 boolean allowUniverseKeywords)

JmlParser

public JmlParser(Main compiler,
                 antlr.TokenStream lexer,
                 ParsingController parsingController,
                 boolean allowGeneric,
                 boolean allowMultiJava,
                 boolean allowRelaxedMultiJava,
                 boolean allowUniverseKeywords,
                 boolean isRefinedCUnit)

JmlParser

protected JmlParser(antlr.TokenBuffer tokenBuf,
                    int k)

JmlParser

public JmlParser(antlr.TokenBuffer tokenBuf)

JmlParser

protected JmlParser(antlr.TokenStream lexer,
                    int k)

JmlParser

public JmlParser(antlr.TokenStream lexer)

JmlParser

public JmlParser(antlr.ParserSharedInputState state)
Method Detail

beautifyParserError

public PositionedError beautifyParserError(antlr.ANTLRException e)
Returns an exception from our exception hierarchy by wrapping the ANTLR excepton. The exception is really positioned, by the positioning information is embedded in the message.

isPrivacyOrNull

public static boolean isPrivacyOrNull(long mod)
Returns true if the argument mod is one of the privacy modifiers (i.e., public, protected or privacy) or null (= 0).

verifySimpleSpecBody

public boolean verifySimpleSpecBody(JmlSpecBodyClause[] clauses)
Returns true if all elements of the argument are simple spec body clauses; otherwise, print an appropriate error message and return false

verifyNormalSpecBody

public boolean verifyNormalSpecBody(JmlSpecBodyClause[] clauses)
Returns true if all elements of the argument are normal spec body clauses; otherwise, print an appropriate error message and return false

verifyExceptionalSpecBody

public boolean verifyExceptionalSpecBody(JmlSpecBodyClause[] clauses)
Returns true if all elements of the argument are exceptional spec body clauses; otherwise, print an appropriate error message and return false

verifySimpleSpecStatementBody

public boolean verifySimpleSpecStatementBody(JmlSpecBodyClause[] clauses)
Returns true if all elements of the argument are simple spec statement body clauses; otherwise, print an appropriate error message and return false

verifyAbruptSpecBody

public boolean verifyAbruptSpecBody(JmlSpecBodyClause[] clauses)
Returns true if all elements of the argument are abrupt spec body clauses; otherwise, print an appropriate error message and return false

getParseClassContext

private CParseClassContext getParseClassContext()
Generates the appropriate data structure for buffering class members during parsing. Implemented as a method for sub-grammars can use a different data structure (of the same name). This is a hack that takes advantage of ANTLR's textual grammar inheritance.

jCompilationUnit

public final JCompilationUnitType jCompilationUnit()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jPackageDefinition

public final JPackageName jPackageDefinition()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlRefinePrefix

public final JmlRefinePrefix jmlRefinePrefix()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jImportDefinition

public final void jImportDefinition(CParseCompilationUnitContext cunit)
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjTopLevelDefinition

public final void mjTopLevelDefinition(CParseCompilationUnitContext context)
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jModifier

public final long jModifier()
                     throws antlr.RecognitionException,
                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjModifier

public final long mjModifier()
                      throws antlr.RecognitionException,
                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlModifier

public final long jmlModifier()
                       throws antlr.RecognitionException,
                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jBuiltInType

public final CType jBuiltInType()
                         throws antlr.RecognitionException,
                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjBuiltInType

public final CType mjBuiltInType()
                          throws antlr.RecognitionException,
                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlBuiltInType

public final CType jmlBuiltInType()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTypeSpec

public final CType jTypeSpec()
                      throws antlr.RecognitionException,
                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjTypeSpec

public final CType mjTypeSpec()
                       throws antlr.RecognitionException,
                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUniversePeerSpec

public final CUniverse jUniversePeerSpec()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjUniversePeerSpec

public final CUniverse mjUniversePeerSpec()
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlUniversePeerSpec

public final CUniverse jmlUniversePeerSpec()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUniverseRepSpec

public final CUniverse jUniverseRepSpec()
                                 throws antlr.RecognitionException,
                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjUniverseRepSpec

public final CUniverse mjUniverseRepSpec()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlUniverseRepSpec

public final CUniverse jmlUniverseRepSpec()
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUniverseReadonlySpec

public final CUniverse jUniverseReadonlySpec()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjUniverseReadonlySpec

public final CUniverse mjUniverseReadonlySpec()
                                       throws antlr.RecognitionException,
                                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlUniverseReadonlySpec

public final CUniverse jmlUniverseReadonlySpec()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jClassDefinition

public final JClassDeclarationType jClassDefinition(long mods,
                                                    antlr.Token startToken)
                                             throws antlr.RecognitionException,
                                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTypeVariableDeclarationList

public final CTypeVariable[] jTypeVariableDeclarationList()
                                                   throws antlr.RecognitionException,
                                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jSuperClassClause

public final JmlParser.TypeBooleanPair jSuperClassClause()
                                                  throws antlr.RecognitionException,
                                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jImplementsClause

public final JmlParser.TypeWeaklyList jImplementsClause()
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jClassBlock

public final void jClassBlock(CParseClassContext context)
                       throws antlr.RecognitionException,
                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTypeName

public final CClassType jTypeName(CUniverse elem_univ)
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jInterfaceDefinition

public final JInterfaceDeclarationType jInterfaceDefinition(long mods,
                                                            antlr.Token startToken)
                                                     throws antlr.RecognitionException,
                                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jInterfaceExtends

public final JmlParser.TypeWeaklyList jInterfaceExtends()
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjTopLevelMethodDeclaration

public final MJTopLevelMethodDeclaration mjTopLevelMethodDeclaration(long mods,
                                                                     antlr.Token startToken)
                                                              throws antlr.RecognitionException,
                                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMethodSpecification

public final JmlMethodSpecification jmlMethodSpecification(long mods)
                                                    throws antlr.RecognitionException,
                                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jModifiers

public final long jModifiers()
                      throws antlr.RecognitionException,
                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjExternalClassTypeSpec

public final CType mjExternalClassTypeSpec()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jParameterDeclarationList

public final JFormalParameter[] jParameterDeclarationList(int desc)
                                                   throws antlr.RecognitionException,
                                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jThrowsClause

public final CClassType[] jThrowsClause()
                                 throws antlr.RecognitionException,
                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jCompoundStatement

public final JStatement[] jCompoundStatement(ParsingController.TokenWrapper declEnd)
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jNameWeaklyList

public final void jNameWeaklyList(JmlParser.TypeWeaklyList self)
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jMember

public final void jMember(CParseClassContext context)
                   throws antlr.RecognitionException,
                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jVariableDefinitions

public final JVariableDefinition[] jVariableDefinitions(long mods,
                                                        CType type)
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlDataGroupClause

public final void jmlDataGroupClause(JmlDataGroupAccumulator self)
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlDeclaration

public final void jmlDeclaration(CParseClassContext context,
                                 long mods,
                                 antlr.Token startToken)
                          throws antlr.RecognitionException,
                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlPredicate

public final JmlPredicate jmlPredicate()
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jParameterDeclaration

public final JFormalParameter jParameterDeclaration(int desc)
                                             throws antlr.RecognitionException,
                                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jValueSpecializer

public final CType jValueSpecializer(CType type,
                                     TokenReference sourceRef)
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGroupList

public final JmlStoreRefExpression[] jmlGroupList()
                                           throws antlr.RecognitionException,
                                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMapsReference

public final JmlStoreRefExpression jmlMapsReference()
                                             throws antlr.RecognitionException,
                                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecArrayRefExpr

public final JmlName jmlSpecArrayRefExpr(TokenReference sourceRef)
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMapsMemberRefExpr

public final void jmlMapsMemberRefExpr(ArrayList namesV)
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGroupName

public final JmlStoreRefExpression jmlGroupName()
                                         throws antlr.RecognitionException,
                                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMethodNameList

public final JmlMethodNameList jmlMethodNameList()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlStoreRefExpression

public final JmlStoreRefExpression jmlStoreRefExpression()
                                                  throws antlr.RecognitionException,
                                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecExpression

public final JmlSpecExpression jmlSpecExpression()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecExpressionList

public final JmlSpecExpression[] jmlSpecExpressionList()
                                                throws antlr.RecognitionException,
                                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMethodName

public final JmlMethodName jmlMethodName()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUniverseType

public final CUniverse jUniverseType()
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jClassTypeSpec

public final CClassType jClassTypeSpec(CUniverse elem_univ,
                                       CUniverse array_univ)
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlParamDisambigList

public final CType[] jmlParamDisambigList()
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlParamDisambig

public final CType jmlParamDisambig()
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlStoreRef

public final JmlStoreRef jmlStoreRef()
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlStoreRefKeyword

public final JmlStoreRefKeyword jmlStoreRefKeyword()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlStoreRefList

public final JmlStoreRef[] jmlStoreRefList()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlStoreRefNameSuffix

public final JmlName jmlStoreRefNameSuffix()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jExpression

public final JExpression jExpression()
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecification

public final JmlSpecification jmlSpecification(long mods)
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlExtendingSpecification

public final JmlExtendingSpecification jmlExtendingSpecification()
                                                          throws antlr.RecognitionException,
                                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecCaseSeq

public final JmlSpecCase[] jmlSpecCaseSeq(long mods)
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlRedundantSpec

public final JmlRedundantSpec jmlRedundantSpec()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecCase

public final JmlSpecCase jmlSpecCase(long mods)
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGenericSpecCase

public final JmlGenericSpecCase jmlGenericSpecCase(boolean isInSpecStatement)
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlHeavyweightSpec

public final JmlHeavyweightSpec jmlHeavyweightSpec(long mods)
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlModelProgram

public final JmlModelProgram jmlModelProgram(long mods)
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlImplications

public final JmlSpecCase[] jmlImplications()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlExamples

public final JmlExample[] jmlExamples()
                               throws antlr.RecognitionException,
                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlExample

public final JmlExample jmlExample()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecVarDecls

public final JmlSpecVarDecl[] jmlSpecVarDecls()
                                       throws antlr.RecognitionException,
                                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecHeader

public final JmlRequiresClause[] jmlSpecHeader()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGenericSpecBody

public final JmlGenericSpecBody jmlGenericSpecBody(boolean isInSpecStatement)
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlRequiresClause

public final JmlRequiresClause jmlRequiresClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecBody

public final JmlSpecBodyClause[] jmlSpecBody()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGenericSpecCaseSeq

public final JmlGenericSpecCase[] jmlGenericSpecCaseSeq(boolean isInSpecStatement)
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecBodyClause

public final JmlSpecBodyClause jmlSpecBodyClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlEnsuresClause

public final JmlEnsuresClause jmlEnsuresClause()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSignalsOnlyClause

public final JmlSignalsOnlyClause jmlSignalsOnlyClause()
                                                throws antlr.RecognitionException,
                                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSignalsClause

public final JmlSignalsClause jmlSignalsClause()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAssignableClause

public final JmlAssignableClause jmlAssignableClause()
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlCapturesClause

public final JmlCapturesClause jmlCapturesClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlDivergesClause

public final JmlDivergesClause jmlDivergesClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlWhenClause

public final JmlWhenClause jmlWhenClause()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlWorkingSpaceClause

public final JmlWorkingSpaceClause jmlWorkingSpaceClause()
                                                  throws antlr.RecognitionException,
                                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlDurationClause

public final JmlDurationClause jmlDurationClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlContinuesClause

public final JmlContinuesClause jmlContinuesClause()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlBreaksClause

public final JmlBreaksClause jmlBreaksClause()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlReturnsClause

public final JmlReturnsClause jmlReturnsClause()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAccessibleClause

public final JmlAccessibleClause jmlAccessibleClause()
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlCallableClause

public final JmlCallableClause jmlCallableClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMeasuredClause

public final JmlMeasuredClause jmlMeasuredClause()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlExceptionalSpecCase

public final JmlExceptionalSpecCase jmlExceptionalSpecCase()
                                                    throws antlr.RecognitionException,
                                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNormalSpecCase

public final JmlNormalSpecCase jmlNormalSpecCase()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlExceptionalSpecBody

public final JmlExceptionalSpecBody jmlExceptionalSpecBody()
                                                    throws antlr.RecognitionException,
                                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlExceptionalSpecCaseSeq

public final JmlGeneralSpecCase[] jmlExceptionalSpecCaseSeq()
                                                     throws antlr.RecognitionException,
                                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNormalSpecBody

public final JmlNormalSpecBody jmlNormalSpecBody()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNormalSpecCaseSeq

public final JmlGeneralSpecCase[] jmlNormalSpecCaseSeq()
                                                throws antlr.RecognitionException,
                                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlCodeContract

public final JmlCodeContract jmlCodeContract(long mods)
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlForAllVarDecl

public final JmlForAllVarDecl jmlForAllVarDecl()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlLocalSpecVarDecl

public final JmlLetVarDecl jmlLocalSpecVarDecl()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlQuantifiedVarDecls

public final JmlVariableDefinition[] jmlQuantifiedVarDecls()
                                                    throws antlr.RecognitionException,
                                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNullityModifier

public final long jmlNullityModifier()
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecVariableDeclarators

public final JVariableDefinition[] jmlSpecVariableDeclarators(long mods,
                                                              CType type)
                                                       throws antlr.RecognitionException,
                                                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jNameList

public final CClassType[] jNameList()
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlPrimary

public final JExpression jmlPrimary()
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlWarnExpression

public final JExpression jmlWarnExpression()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlMathModeExpression

public final JExpression jmlMathModeExpression()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSetComprehension

public final JExpression jmlSetComprehension(CType type)
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jPostfixExpression

public final JExpression jPostfixExpression()
                                     throws antlr.RecognitionException,
                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecQuantifiedExprRest

public final JmlSpecQuantifiedExpression jmlSpecQuantifiedExprRest(TokenReference sourceRef)
                                                            throws antlr.RecognitionException,
                                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNonNullNullityModifier

public final long jmlNonNullNullityModifier()
                                     throws antlr.RecognitionException,
                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecVariableDeclarator

public final JVariableDefinition jmlSpecVariableDeclarator(long mods,
                                                           CType type)
                                                    throws antlr.RecognitionException,
                                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecInitializer

public final JExpression jmlSpecInitializer()
                                     throws antlr.RecognitionException,
                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecArrayInitializer

public final JArrayInitializer jmlSpecArrayInitializer()
                                                throws antlr.RecognitionException,
                                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jStatement

public final JStatement jStatement()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjStatement

public final JStatement mjStatement()
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlHenceByStatement

public final JmlHenceByStatement jmlHenceByStatement()
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAssertStatement

public final JmlAssertStatement jmlAssertStatement()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAssumeStatement

public final JmlAssumeStatement jmlAssumeStatement()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlDebugStatement

public final JmlDebugStatement jmlDebugStatement()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSetStatement

public final JmlSetStatement jmlSetStatement()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlUnreachableStatement

public final JmlUnreachableStatement jmlUnreachableStatement()
                                                      throws antlr.RecognitionException,
                                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlModelProgStatement

public final JmlModelProgStatement jmlModelProgStatement()
                                                  throws antlr.RecognitionException,
                                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jDeclaration

public final JVariableDeclarationStatement jDeclaration()
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jLoopStatement

public final JStatement jLoopStatement()
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlLoopInvariantList

public final JmlLoopInvariant[] jmlLoopInvariantList()
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlVariantFunctionList

public final JmlVariantFunction[] jmlVariantFunctionList()
                                                  throws antlr.RecognitionException,
                                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jLabeledStatement

public final JLabeledStatement jLabeledStatement()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jSimpleLoopStatement

public final JLoopStatement jSimpleLoopStatement()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjOrJmlUnaryExpressionNotPlusMinus

public final JExpression mjOrJmlUnaryExpressionNotPlusMinus()
                                                     throws antlr.RecognitionException,
                                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUnaryExpression

public final JExpression jUnaryExpression()
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUniverseSpec

public final CUniverse jUniverseSpec()
                              throws antlr.RecognitionException,
                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jBuiltInTypeSpec

public final CType jBuiltInTypeSpec(CUniverse array_univ)
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUnaryExpressionNotPlusMinus

public final JExpression jUnaryExpressionNotPlusMinus()
                                               throws antlr.RecognitionException,
                                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjUniverseImplicitPeerSpec

public final CUniverse mjUniverseImplicitPeerSpec()
                                           throws antlr.RecognitionException,
                                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jForStatement

public final JForStatement jForStatement()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jWhileStatement

public final JWhileStatement jWhileStatement()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jDoStatement

public final JDoStatement jDoStatement()
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlLoopInvariant

public final JmlLoopInvariant jmlLoopInvariant()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlVariantFunction

public final JmlVariantFunction jmlVariantFunction()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jAssignmentExpression

public final JExpression jAssignmentExpression()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNondeterministicChoice

public final JmlNondetChoiceStatement jmlNondeterministicChoice()
                                                         throws antlr.RecognitionException,
                                                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlNondeterministicIf

public final JmlNondetIfStatement jmlNondeterministicIf()
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlInvariantStatement

public final JmlInvariantStatement jmlInvariantStatement()
                                                  throws antlr.RecognitionException,
                                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlSpecStatement

public final JmlSpecStatement jmlSpecStatement()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGuardedStatements

public final JmlGuardedStatement[] jmlGuardedStatements()
                                                 throws antlr.RecognitionException,
                                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlGuardedStatement

public final JmlGuardedStatement jmlGuardedStatement()
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAbruptSpecCase

public final JmlAbruptSpecCase jmlAbruptSpecCase()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAbruptSpecBody

public final JmlAbruptSpecBody jmlAbruptSpecBody()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlAbruptSpecCaseSeq

public final JmlGeneralSpecCase[] jmlAbruptSpecCaseSeq()
                                                throws antlr.RecognitionException,
                                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jConditionalExpression

public final JExpression jConditionalExpression()
                                         throws antlr.RecognitionException,
                                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlEquivalenceExpression

public final JExpression jmlEquivalenceExpression()
                                           throws antlr.RecognitionException,
                                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jEqualityExpression

public final JExpression jEqualityExpression()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jRelationalExpression

public final JExpression jRelationalExpression()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jShiftExpression

public final JExpression jShiftExpression()
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlImpliesExpression

public final JExpression jmlImpliesExpression()
                                       throws antlr.RecognitionException,
                                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jLogicalOrExpression

public final JExpression jLogicalOrExpression()
                                       throws antlr.RecognitionException,
                                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlForwardImpliesExpression

public final JExpression jmlForwardImpliesExpression()
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jmlBackwardImpliesExpression

public final JExpression jmlBackwardImpliesExpression()
                                               throws antlr.RecognitionException,
                                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jPrimaryExpression

public final JExpression jPrimaryExpression()
                                     throws antlr.RecognitionException,
                                            antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjPrimaryExpression

public final JExpression mjPrimaryExpression()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jParenthesizedExpression

public final JExpression jParenthesizedExpression()
                                           throws antlr.RecognitionException,
                                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jParenthesizedExpressionRest

public final JExpression jParenthesizedExpressionRest(TokenReference sourceRef)
                                               throws antlr.RecognitionException,
                                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jNewExpression

public final JExpression jNewExpression(JExpression expr)
                                 throws antlr.RecognitionException,
                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jType

public final CType jType(CUniverse elem_univ)
                  throws antlr.RecognitionException,
                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jArgList

public final JExpression[] jArgList()
                             throws antlr.RecognitionException,
                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jNewArrayDeclarator

public final JExpression[] jNewArrayDeclarator()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jArrayInitializer

public final JArrayInitializer jArrayInitializer()
                                          throws antlr.RecognitionException,
                                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jIdentifier

public final String jIdentifier()
                         throws antlr.RecognitionException,
                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTypeDefinition

public final void jTypeDefinition(CParseCompilationUnitContext context,
                                  long mods,
                                  antlr.Token startToken)
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjTopLevelDeclaration

public final void mjTopLevelDeclaration(CParseCompilationUnitContext context,
                                        long mods,
                                        antlr.Token startToken)
                                 throws antlr.RecognitionException,
                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jWildCard

public final CClassType jWildCard()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jWildcardBound

public final CClassType jWildcardBound()
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jParameterizedClassTypeList

public final CClassType[] jParameterizedClassTypeList()
                                               throws antlr.RecognitionException,
                                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTypeParameter

public final CClassType jTypeParameter()
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTypeVariableDeclaration

public final CTypeVariable jTypeVariableDeclaration()
                                             throws antlr.RecognitionException,
                                                    antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jUniverseExceptionSpec

public final CUniverse jUniverseExceptionSpec()
                                       throws antlr.RecognitionException,
                                              antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjUniverseImplicitReadonlySpec

public final CUniverse mjUniverseImplicitReadonlySpec()
                                               throws antlr.RecognitionException,
                                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jVariableDeclarator

public final JVariableDefinition jVariableDeclarator(long mods,
                                                     CType type)
                                              throws antlr.RecognitionException,
                                                     antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jVarInitializer

public final JExpression jVarInitializer()
                                  throws antlr.RecognitionException,
                                         antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jInitializer

public final JExpression jInitializer()
                               throws antlr.RecognitionException,
                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jIfStatement

public final JIfStatement jIfStatement()
                                throws antlr.RecognitionException,
                                       antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jBreakStatement

public final JBreakStatement jBreakStatement()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jContinueStatement

public final JContinueStatement jContinueStatement()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jReturnStatement

public final JReturnStatement jReturnStatement()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jSwitchStatement

public final JSwitchStatement jSwitchStatement()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jTryBlock

public final JStatement jTryBlock()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jThrowStatement

public final JThrowStatement jThrowStatement()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jAssertStatement

public final JAssertStatement jAssertStatement()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jSynchronizedStatement

public final JSynchronizedStatement jSynchronizedStatement()
                                                    throws antlr.RecognitionException,
                                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jCasesGroup

public final JSwitchGroup jCasesGroup()
                               throws antlr.RecognitionException,
                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jACase

public final JSwitchLabel jACase()
                          throws antlr.RecognitionException,
                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jForInit

public final JStatement jForInit()
                          throws antlr.RecognitionException,
                                 antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jForCond

public final JExpression jForCond()
                           throws antlr.RecognitionException,
                                  antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jForIter

public final JExpressionListStatement jForIter()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jExpressionList

public final JExpression[] jExpressionList()
                                    throws antlr.RecognitionException,
                                           antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jHandler

public final JCatchClause jHandler()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jLogicalAndExpression

public final JExpression jLogicalAndExpression()
                                        throws antlr.RecognitionException,
                                               antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jInclusiveOrExpression

public final JExpression jInclusiveOrExpression()
                                         throws antlr.RecognitionException,
                                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jExclusiveOrExpression

public final JExpression jExclusiveOrExpression()
                                         throws antlr.RecognitionException,
                                                antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jAndExpression

public final JExpression jAndExpression()
                                 throws antlr.RecognitionException,
                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jAdditiveExpression

public final JExpression jAdditiveExpression()
                                      throws antlr.RecognitionException,
                                             antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jMultiplicativeExpression

public final JExpression jMultiplicativeExpression()
                                            throws antlr.RecognitionException,
                                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jSuperSuffix

public final JExpression jSuperSuffix(JSuperExpression supExpr)
                               throws antlr.RecognitionException,
                                      antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjResendSuffix

public final JExpression mjResendSuffix(JExpression prefix)
                                 throws antlr.RecognitionException,
                                        antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

jConstant

public final JExpression jConstant()
                            throws antlr.RecognitionException,
                                   antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mjWarnExpression

public final JExpression mjWarnExpression()
                                   throws antlr.RecognitionException,
                                          antlr.TokenStreamException
Throws:
antlr.RecognitionException
antlr.TokenStreamException

mk_tokenSet_0

private static final long[] mk_tokenSet_0()

mk_tokenSet_1

private static final long[] mk_tokenSet_1()

mk_tokenSet_2

private static final long[] mk_tokenSet_2()

mk_tokenSet_3

private static final long[] mk_tokenSet_3()

mk_tokenSet_4

private static final long[] mk_tokenSet_4()

mk_tokenSet_5

private static final long[] mk_tokenSet_5()

mk_tokenSet_6

private static final long[] mk_tokenSet_6()

mk_tokenSet_7

private static final long[] mk_tokenSet_7()

mk_tokenSet_8

private static final long[] mk_tokenSet_8()

mk_tokenSet_9

private static final long[] mk_tokenSet_9()

mk_tokenSet_10

private static final long[] mk_tokenSet_10()

mk_tokenSet_11

private static final long[] mk_tokenSet_11()

mk_tokenSet_12

private static final long[] mk_tokenSet_12()

mk_tokenSet_13

private static final long[] mk_tokenSet_13()

mk_tokenSet_14

private static final long[] mk_tokenSet_14()

mk_tokenSet_15

private static final long[] mk_tokenSet_15()

mk_tokenSet_16

private static final long[] mk_tokenSet_16()

mk_tokenSet_17

private static final long[] mk_tokenSet_17()

mk_tokenSet_18

private static final long[] mk_tokenSet_18()

mk_tokenSet_19

private static final long[] mk_tokenSet_19()

mk_tokenSet_20

private static final long[] mk_tokenSet_20()

mk_tokenSet_21

private static final long[] mk_tokenSet_21()

mk_tokenSet_22

private static final long[] mk_tokenSet_22()

mk_tokenSet_23

private static final long[] mk_tokenSet_23()

mk_tokenSet_24

private static final long[] mk_tokenSet_24()

mk_tokenSet_25

private static final long[] mk_tokenSet_25()

mk_tokenSet_26

private static final long[] mk_tokenSet_26()

mk_tokenSet_27

private static final long[] mk_tokenSet_27()

mk_tokenSet_28

private static final long[] mk_tokenSet_28()

mk_tokenSet_29

private static final long[] mk_tokenSet_29()

mk_tokenSet_30

private static final long[] mk_tokenSet_30()

mk_tokenSet_31

private static final long[] mk_tokenSet_31()

mk_tokenSet_32

private static final long[] mk_tokenSet_32()

mk_tokenSet_33

private static final long[] mk_tokenSet_33()

mk_tokenSet_34

private static final long[] mk_tokenSet_34()

mk_tokenSet_35

private static final long[] mk_tokenSet_35()

mk_tokenSet_36

private static final long[] mk_tokenSet_36()

mk_tokenSet_37

private static final long[] mk_tokenSet_37()

mk_tokenSet_38

private static final long[] mk_tokenSet_38()

mk_tokenSet_39

private static final long[] mk_tokenSet_39()

mk_tokenSet_40

private static final long[] mk_tokenSet_40()

mk_tokenSet_41

private static final long[] mk_tokenSet_41()

mk_tokenSet_42

private static final long[] mk_tokenSet_42()

mk_tokenSet_43

private static final long[] mk_tokenSet_43()

mk_tokenSet_44

private static final long[] mk_tokenSet_44()

mk_tokenSet_45

private static final long[] mk_tokenSet_45()

mk_tokenSet_46

private static final long[] mk_tokenSet_46()
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.