org.eclipse.jdt.internal.compiler.parser
Class JmlParserHelper

java.lang.Object
  org.eclipse.jdt.internal.compiler.parser.JmlParserHelper

All Implemented Interfaces:

OperatorIds, TerminalTokens

public class JmlParserHelper
extends java.lang.Object
implements TerminalTokens, OperatorIds

Field Summary

Nullity	defaultNullity
boolean	jmlKeywordHasRedundantSuffix
int	jmlKeywordTokenId
long	ownershipModifiers
boolean	processingSpecVarDecls

Fields inherited from interface org.eclipse.jdt.internal.compiler.parser.TerminalTokens

TokenNameabstract, TokenNamealso, TokenNameAND, TokenNameAND_AND, TokenNameAND_EQUAL, TokenNameassert, TokenNameAssignableOrSynonym, TokenNameAssignableRedundantlyOrSynonym, TokenNameassume, TokenNameassume_redundantly, TokenNameAT, TokenNameaxiom, TokenNameBehaviorOrSynonym, TokenNameboolean, TokenNamebreak, TokenNamebyte, TokenNamecase, TokenNamecatch, TokenNamechar, TokenNameCharacterLiteral, TokenNameclass, TokenNamecode_bigint_math, TokenNamecode_java_math, TokenNamecode_safe_math, TokenNameCOLON, TokenNameCOMMA, TokenNameCOMMENT_BLOCK, TokenNameCOMMENT_JAVADOC, TokenNameCOMMENT_LINE, TokenNameconst, TokenNameconstraint, TokenNameconstraint_redundantly, TokenNamecontinue, TokenNamedecreases, TokenNamedecreases_redundantly, TokenNamedefault, TokenNamediverges, TokenNamediverges_redundantly, TokenNameDIVIDE, TokenNameDIVIDE_EQUAL, TokenNamedo, TokenNameDOT, TokenNameDOTDOT, TokenNamedouble, TokenNameDoubleLiteral, TokenNameELLIPSIS, TokenNameelse, TokenNameEnsuresOrSynonym, TokenNameEnsuresRedundantlyOrSynonym, TokenNameenum, TokenNameEOF, TokenNameEQUAL, TokenNameEQUAL_EQUAL, TokenNameEQUIV, TokenNameERROR, TokenNameextends, TokenNamefalse, TokenNamefinal, TokenNamefinally, TokenNamefloat, TokenNameFloatingPointLiteral, TokenNamefor, TokenNameforall, TokenNameghost, TokenNamegoto, TokenNameGREATER, TokenNameGREATER_EQUAL, TokenNamehelper, TokenNameIdentifier, TokenNameif, TokenNameimplements, TokenNameIMPLIES, TokenNameimplies_that, TokenNameimport, TokenNamein, TokenNamein_redundantly, TokenNameInformalDescription, TokenNameinitially, TokenNameinstance, TokenNameinstanceof, TokenNameint, TokenNameIntegerLiteral, TokenNameinterface, TokenNameinvariant, TokenNameinvariant_redundantly, TokenNamejml_assert, TokenNamejml_assert_redundantly, TokenNameLBRACE, TokenNameLBRACE_OR, TokenNameLBRACKET, TokenNameLEFT_SHIFT, TokenNameLEFT_SHIFT_EQUAL, TokenNameLESS, TokenNameLESS_EQUAL, TokenNamelong, TokenNameLongLiteral, TokenNameloop_invariant, TokenNameloop_invariant_redundantly, TokenNameLPAREN, TokenNamemaps, TokenNamemaps_redundantly, TokenNameMINUS, TokenNameMINUS_EQUAL, TokenNameMINUS_MINUS, TokenNamemodel, TokenNamemono_non_null, TokenNameMULTIPLY, TokenNameMULTIPLY_EQUAL, TokenNamenative, TokenNamenew, TokenNamenon_null, TokenNamenon_null_by_default, TokenNameNOT, TokenNameNOT_EQUAL, TokenNameNOT_EQUIV, TokenNamenowarn, TokenNamenull, TokenNamenullable, TokenNamenullable_by_default, TokenNameold, TokenNameOR, TokenNameOR_EQUAL, TokenNameOR_OR, TokenNameOR_RBRACE, TokenNamepackage, TokenNamepeer, TokenNamePLUS, TokenNamePLUS_EQUAL, TokenNamePLUS_PLUS, TokenNameprivate, TokenNameprotected, TokenNamepublic, TokenNamepure, TokenNameQUESTION, TokenNameRBRACE, TokenNameRBRACKET, TokenNamereadonly, TokenNameREMAINDER, TokenNameREMAINDER_EQUAL, TokenNamerep, TokenNamerepresents, TokenNameREPRESENTS, TokenNamerepresents_redundantly, TokenNameRequiresOrSynonym, TokenNameRequiresRedundantlyOrSynonym, TokenNamereturn, TokenNameREV_IMPLIES, TokenNameRIGHT_SHIFT, TokenNameRIGHT_SHIFT_EQUAL, TokenNameRPAREN, TokenNameSEMICOLON, TokenNameset, TokenNameshort, TokenNamesignals_only, TokenNamesignals_only_redundantly, TokenNameSignalsOrSynonym, TokenNameSignalsRedundantlyOrSynonym, TokenNameslash_elemtype, TokenNameslash_everything, TokenNameslash_exists, TokenNameslash_forall, TokenNameslash_fresh, TokenNameslash_into, TokenNameslash_max, TokenNameslash_min, TokenNameslash_nonnullelements, TokenNameslash_not_assigned, TokenNameslash_not_modified, TokenNameslash_not_specified, TokenNameslash_nothing, TokenNameslash_num_of, TokenNameslash_old, TokenNameslash_peer, TokenNameslash_pre, TokenNameslash_product, TokenNameslash_readonly, TokenNameslash_rep, TokenNameslash_result, TokenNameslash_same, TokenNameslash_sum, TokenNameslash_type, TokenNameslash_typeof, TokenNamespec_bigint_math, TokenNamespec_java_math, TokenNamespec_protected, TokenNamespec_public, TokenNamespec_safe_math, TokenNamestatic, TokenNamestrictfp, TokenNameStringLiteral, TokenNameSUBTYPE, TokenNamesuper, TokenNameswitch, TokenNamesynchronized, TokenNamethis, TokenNamethrow, TokenNamethrows, TokenNametransient, TokenNametrue, TokenNametry, TokenNameTWIDDLE, TokenNameuninitialized, TokenNameUNSIGNED_RIGHT_SHIFT, TokenNameUNSIGNED_RIGHT_SHIFT_EQUAL, TokenNamevoid, TokenNamevolatile, TokenNamewhile, TokenNameWHITESPACE, TokenNameXOR, TokenNameXOR_EQUAL

Fields inherited from interface org.eclipse.jdt.internal.compiler.ast.OperatorIds

AND, AND_AND, DIVIDE, EQUAL, EQUAL_EQUAL, GREATER, GREATER_EQUAL, INSTANCEOF, JML_ELEMTYPE, JML_EQUIV, JML_IMPLIES, JML_NONNULLELEMENTS, JML_NOT_ASSIGNED, JML_NOT_EQUIV, JML_NOT_MODIFIED, JML_OLD, JML_PRE, JML_REPRESENTS, JML_REV_IMPLIES, JML_TYPE, JML_TYPEOF, JmlOtherOpIdStart, LEFT_SHIFT, LESS, LESS_EQUAL, MINUS, MINUS_MINUS, MULTIPLY, NOT, NOT_EQUAL, NumberOfExtraTablesForJML, NumberOfTables, OR, OR_OR, PLUS, PLUS_PLUS, QUESTIONCOLON, REMAINDER, RIGHT_SHIFT, TWIDDLE, UNSIGNED_RIGHT_SHIFT, XOR

Constructor Summary

JmlParserHelper(Parser _this)

Method Summary

void	Assert_isTrue(boolean b)
void	Assert_isTrue(boolean b, java.lang.String msg)
void	consumeCastExpressionWithoutType()
void	consumeClassInstanceCreationExpressionWithSetComprehension()
void	consumeConstraintDeclaration()
void	consumeDataGroupClauseSeq()
void	consumeDefaultNullity()
void	consumeDimLoop()
void	consumeEmptyJmlLabel()
void	consumeEmptyJmlSpecVarDecls()
void	consumeExitJmlClause()
void	consumeFieldDeclarationWithDataGroupClause()
void	consumeHeavyweightSpecCase()
void	consumeInDataGroupClause()
void	consumeInvalidSpecedConstructorDeclaration(boolean isAbstract)
void	consumeInvalidSpecedMethodDeclaration()
void	consumeJmlArrayIndexRange(int i)
void	consumeJmlArrayRangeAccess(boolean unspecifiedReference)
void	consumeJmlAssertStatement()
void	consumeJmlAssumeStatement()
void	consumeJmlClause()
void	consumeJmlElemtypeExpression(int op)
void	consumeJmlFreshExpression()
void	consumeJmlLoopInvariantSeq()
void	consumeJmlLoopVariantSeq()
void	consumeJmlModifierAsModifier()
void	consumeJmlMultiFieldAccess(boolean isSuperAccess)
void	consumeJmlMultiReferenceExpressionAsNameDotStar()
void	consumeJmlPrimaryLabeledOldExpression(int op)
void	consumeJmlPrimaryOldExpression(int op)
void	consumeJmlPrimaryResult()
void	consumeJmlQuantifiedExpression(boolean rangeSpecified)
void	consumeJmlQuantifiedVarDeclarators(boolean isFirst)
void	consumeJmlSetComprehension()
void	consumeJmlSetStatement()
void	consumeJmlSimpleAssertStatement()
void	consumeJmlSimpleAssumeStatement()
void	consumeJmlStoreRefSeqAsStoreRefListExpression()
void	consumeJmlSubtypeExpression()
void	consumeJmlTypeBodyDeclaration()
void	consumeJmlTypeExpression(int op)
void	consumeJmlTypeofExpression(int op)
void	consumeJmlUnaryExpression(int op)
void	consumeJmlVarDecls()
void	consumeLightweightSpecCase()
void	consumeLoopAnnotations(boolean hasInvariantSeq, boolean hasVariantSeq)
void	consumeMapsIntoClause()
void	consumeMethodSpecification(boolean isExtending, boolean hasSpecCaseSeq, boolean hasRedundantPart)
void	consumeMethodSpecRedundantPart()
void	consumeOneDimLoopWithNullity()
void	consumeOwnershipModifiers(int numModifiers)
void	consumeReferenceTypeWithoutOwnershipModifiers()
void	consumeRequiresClauseSeq()
void	consumeSignalsClause(boolean hasIdentifier)
void	consumeSignalsOnlyClause()
void	consumeSignalsOnlyClauseNothing()
void	consumeSpecCaseBlock()
void	consumeSpecCaseBody(boolean hasHeader, boolean hasRest)
void	consumeSpecCaseBodySeq()
void	consumeSpecCaseHeader()
void	consumeSpecCaseRestAsClauseSeq()
void	consumeSpecCaseRestClauseSeq()
void	consumeSpecCaseSeq()
void	consumeSpecedConstructorDeclaration()
void	consumeSpecedMethodDeclaration(boolean isNotAbstract)
void	consumeStartSpecVarDecls()
void	consumeStatementDoWithAnnotations()
void	consumeStatementForWithAnnotations()
void	consumeStatementWhileWithAnnotations()
void	consumeTypeWithOwnershipModifiers()
void	emptyNullityStacks()
Nullity	getAndResetNullity()
long	getAndResetOwnershipModifiers()
void	markNullityStackAsDims()
boolean	nullityStackIsEmpty()
boolean	nullityTopIsDims()
boolean	nullityTopIsDims(int pos)
boolean	nullityTopIsLength(int n)
int	nullityTopLength()
Nullity	popNullityStack()
Nullity[]	popNullityStack(int n)
void	pushOnNullityStack(Nullity nullity)
void	pushOnNullityStack(Nullity[] nullities)
void	resetStacksExtra()
void	setJmlInRecoveryMode()
void	signalEndOfClassAndResetDefaultNullity()
void	signalNewClassAndCheckInnerClassDefaultNullity(TypeDeclaration typedecl, java.lang.String type)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

ownershipModifiers

public long ownershipModifiers

defaultNullity

public Nullity defaultNullity

processingSpecVarDecls

public boolean processingSpecVarDecls

jmlKeywordHasRedundantSuffix

public boolean jmlKeywordHasRedundantSuffix

jmlKeywordTokenId

public int jmlKeywordTokenId

Constructor Detail

JmlParserHelper

public JmlParserHelper(Parser _this)

Method Detail

setJmlInRecoveryMode

public void setJmlInRecoveryMode()

getAndResetNullity

public Nullity getAndResetNullity()

getAndResetOwnershipModifiers

public long getAndResetOwnershipModifiers()

consumeDefaultNullity

public void consumeDefaultNullity()

consumeOneDimLoopWithNullity

public void consumeOneDimLoopWithNullity()

consumeDimLoop

public void consumeDimLoop()

consumeJmlSetStatement

public void consumeJmlSetStatement()

consumeEmptyJmlLabel

public void consumeEmptyJmlLabel()

consumeJmlLoopVariantSeq

public void consumeJmlLoopVariantSeq()

consumeJmlLoopInvariantSeq

public void consumeJmlLoopInvariantSeq()

consumeLoopAnnotations

public void consumeLoopAnnotations(boolean hasInvariantSeq,
                                   boolean hasVariantSeq)

consumeSignalsClause

public void consumeSignalsClause(boolean hasIdentifier)

consumeSignalsOnlyClause

public void consumeSignalsOnlyClause()

consumeSignalsOnlyClauseNothing

public void consumeSignalsOnlyClauseNothing()

consumeFieldDeclarationWithDataGroupClause

public void consumeFieldDeclarationWithDataGroupClause()

consumeDataGroupClauseSeq

public void consumeDataGroupClauseSeq()

consumeInDataGroupClause

public void consumeInDataGroupClause()

consumeMapsIntoClause

public void consumeMapsIntoClause()

consumeExitJmlClause

public void consumeExitJmlClause()

consumeOwnershipModifiers

public void consumeOwnershipModifiers(int numModifiers)

consumeTypeWithOwnershipModifiers

public void consumeTypeWithOwnershipModifiers()

consumeReferenceTypeWithoutOwnershipModifiers

public void consumeReferenceTypeWithoutOwnershipModifiers()

consumeJmlModifierAsModifier

public void consumeJmlModifierAsModifier()

consumeJmlTypeBodyDeclaration

public void consumeJmlTypeBodyDeclaration()

consumeConstraintDeclaration

public void consumeConstraintDeclaration()

consumeJmlPrimaryResult

public void consumeJmlPrimaryResult()

consumeJmlFreshExpression

public void consumeJmlFreshExpression()

consumeJmlTypeExpression

public void consumeJmlTypeExpression(int op)

consumeJmlUnaryExpression

public void consumeJmlUnaryExpression(int op)

consumeJmlTypeofExpression

public void consumeJmlTypeofExpression(int op)

consumeJmlElemtypeExpression

public void consumeJmlElemtypeExpression(int op)

consumeJmlPrimaryOldExpression

public void consumeJmlPrimaryOldExpression(int op)

consumeJmlPrimaryLabeledOldExpression

public void consumeJmlPrimaryLabeledOldExpression(int op)

consumeSpecCaseBodySeq

public void consumeSpecCaseBodySeq()

consumeSpecCaseRestClauseSeq

public void consumeSpecCaseRestClauseSeq()

consumeSpecCaseSeq

public void consumeSpecCaseSeq()

consumeLightweightSpecCase

public void consumeLightweightSpecCase()

consumeHeavyweightSpecCase

public void consumeHeavyweightSpecCase()

consumeSpecCaseRestAsClauseSeq

public void consumeSpecCaseRestAsClauseSeq()

consumeRequiresClauseSeq

public void consumeRequiresClauseSeq()

consumeSpecCaseHeader

public void consumeSpecCaseHeader()

consumeSpecCaseBody

public void consumeSpecCaseBody(boolean hasHeader,
                                boolean hasRest)

consumeStartSpecVarDecls

public void consumeStartSpecVarDecls()

consumeEmptyJmlSpecVarDecls

public void consumeEmptyJmlSpecVarDecls()

consumeJmlVarDecls

public void consumeJmlVarDecls()

consumeSpecCaseBlock

public void consumeSpecCaseBlock()

consumeJmlClause

public void consumeJmlClause()

consumeJmlStoreRefSeqAsStoreRefListExpression

public void consumeJmlStoreRefSeqAsStoreRefListExpression()

consumeMethodSpecification

public void consumeMethodSpecification(boolean isExtending,
                                       boolean hasSpecCaseSeq,
                                       boolean hasRedundantPart)

consumeSpecedMethodDeclaration

public void consumeSpecedMethodDeclaration(boolean isNotAbstract)

consumeInvalidSpecedMethodDeclaration

public void consumeInvalidSpecedMethodDeclaration()

consumeSpecedConstructorDeclaration

public void consumeSpecedConstructorDeclaration()

consumeInvalidSpecedConstructorDeclaration

public void consumeInvalidSpecedConstructorDeclaration(boolean isAbstract)

consumeCastExpressionWithoutType

public void consumeCastExpressionWithoutType()

consumeJmlSimpleAssertStatement

public void consumeJmlSimpleAssertStatement()

consumeJmlAssertStatement

public void consumeJmlAssertStatement()

consumeJmlAssumeStatement

public void consumeJmlAssumeStatement()

consumeJmlSimpleAssumeStatement

public void consumeJmlSimpleAssumeStatement()

consumeStatementDoWithAnnotations

public void consumeStatementDoWithAnnotations()

consumeStatementForWithAnnotations

public void consumeStatementForWithAnnotations()

consumeStatementWhileWithAnnotations

public void consumeStatementWhileWithAnnotations()

consumeMethodSpecRedundantPart

public void consumeMethodSpecRedundantPart()

consumeJmlQuantifiedExpression

public void consumeJmlQuantifiedExpression(boolean rangeSpecified)

consumeJmlQuantifiedVarDeclarators

public void consumeJmlQuantifiedVarDeclarators(boolean isFirst)

consumeClassInstanceCreationExpressionWithSetComprehension

public void consumeClassInstanceCreationExpressionWithSetComprehension()

consumeJmlSetComprehension

public void consumeJmlSetComprehension()

consumeJmlSubtypeExpression

public void consumeJmlSubtypeExpression()

consumeJmlMultiReferenceExpressionAsNameDotStar

public void consumeJmlMultiReferenceExpressionAsNameDotStar()

consumeJmlMultiFieldAccess

public void consumeJmlMultiFieldAccess(boolean isSuperAccess)

consumeJmlArrayRangeAccess

public void consumeJmlArrayRangeAccess(boolean unspecifiedReference)

consumeJmlArrayIndexRange

public void consumeJmlArrayIndexRange(int i)

Assert_isTrue

public void Assert_isTrue(boolean b)

Assert_isTrue

public void Assert_isTrue(boolean b,
                          java.lang.String msg)

pushOnNullityStack

public void pushOnNullityStack(Nullity nullity)

pushOnNullityStack

public void pushOnNullityStack(Nullity[] nullities)

nullityStackIsEmpty

public boolean nullityStackIsEmpty()

popNullityStack

public Nullity popNullityStack()

popNullityStack

public Nullity[] popNullityStack(int n)

markNullityStackAsDims

public void markNullityStackAsDims()

nullityTopIsDims

public boolean nullityTopIsDims()

nullityTopIsDims

public boolean nullityTopIsDims(int pos)

nullityTopIsLength

public boolean nullityTopIsLength(int n)

nullityTopLength

public int nullityTopLength()

emptyNullityStacks

public void emptyNullityStacks()

signalEndOfClassAndResetDefaultNullity

public void signalEndOfClassAndResetDefaultNullity()

signalNewClassAndCheckInnerClassDefaultNullity

public void signalNewClassAndCheckInnerClassDefaultNullity(TypeDeclaration typedecl,
                                                           java.lang.String type)

resetStacksExtra

public void resetStacksExtra()