Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.parser
Class EscPragmaParser

    java.lang.Object
      javafe.parser.ParseUtil
          javafe.parser.ParseType
              javafe.parser.ParseExpr
                  javafe.parser.ParseStmt
                      javafe.parser.Parse
                          escjava.parser.EscPragmaParser

All Implemented Interfaces:
  PragmaParser

public class EscPragmaParser
extends Parse
implements PragmaParser

Grammar:

     Pragma ::= LexicalPragma | ModifierPragma | TypeDeclElemPragma | StmtPragma

     LexicalPragma ::= "nowarn" [ Idn [',' Idn]* ] [';']

     StmtPragma ::= SimpleStmtPragma [';']
     | ExprStmtPragma SpecExpr [';']
     | 'set' PrimaryExpr '=' SpecExpr [';']

     SimpleStmtPragma ::= 'unreachable'

     ExprStmtPragma ::= 'assume' | 'assume_redundantly'
     | 'assert' | 'assert_redundantly'
     | 'loop_inv' | 'loop_invariant' | 'loop_invariant_redundantly'
     | 'decreases' | 'decreases_redundantly'
     | 'loop_predicate'
     | 'maintaining' | 'maintaining_redundantly'
     | 'decreasing' | 'decreasing_redundantly'

     TypeDeclElemPragma ::=
     ExprDeclPragma SpecExpr [';']
     | 'ghost' Modifiers Type VariableDeclarator [';']
     | 'still_deferred' Idn [',' Idn]* [';']

     ExprDeclPragma ::= 'axiom' | 'invariant' | 'invariant_redundantly'

     ModifierPragma ::=
     [PrivacyPragma] [BehaviorPragma] SimpleModifierPragma
     [PrivacyPragma] [BehaviorPragma] NonSimpleModifierPragma

     NonSimpleModifierPragma ::=
     | ['also'] ExprModifierPragma SpecExpr [';']
     | ['also'] VarExprModifierPragma '(' Type Idn ')' SpecExpr [';']
     | ['also'] 'monitored_by' SpecExpr [',' SpecExpr]* [';']
     | ['also'] ModifierPragma SpecDesignator [',' SpecDesignator]* [';']

     PrivacyPragma ::= 'public' | 'private' | 'protected'

     BehaviorPragma ::= 'behavior' | 'normal_behavior' | 'exceptional_behavior'

     SimpleModifierPragma ::= 'uninitialized' | 'monitored'
     | 'non_null' | 'instance' | 'pure'
     | 'spec_public' | 'writable_deferred' | 'helper'
     | 'public' | 'private' | 'protected'
     | 'spec_protected' | 'model' | 'transient' | '\peer' | '\readonly' | '\rep'
     | 'may_be_null' | 'non_null_ref_by_default' | 'null_ref_by_default' | 'obs_pure'
     | 'code_java_math' | 'code_safe_math' | 'code_bigint_math'
     | 'spec_java_math' | 'spec_safe_math' | 'spec_bigint_math'

     ExprModifierPragma ::= 'readable_if' | 'writable_if'
     | 'requires' | 'requires_redundantly' | 'also_requires' (if Main.allowAlsoRequires)
     | 'ensures' | 'ensures_redundantly' | 'also_ensures'
     | 'pre' | 'pre_redundantly' | 'post' | 'post_redundantly'

     VarExprModifierPragma ::= 'exsures' | 'exsures_redundantly' | 'also_exsures"
     | 'signals' | 'signals_redundantly'

     ModifierPragma ::= 'modifies' | 'modifies_redundantly' | 'also_modifies'
     | 'modifiable' | 'modifiable_redundantly'
     | 'assignable' | 'assignable_redundantly'

     DurationClause ::= DurationKeyword '\not_specified' ';'
     | DurationKeyword DurSpecExpr [ 'if' predicate ] ';'

     DurSpecExpr ::= SpecExpr (of type long) OpWithLongResult DurSpecExpr
     | '\duration' '(' MethodInvOrConstructor ')' LongOp DurSpecExpr;

     MethodInvOrConstructorOrNotSpecified ::= MethodInvOrConstructor | '\not_specified';

     InvariantForExpr ::= '\invariant_for' '(' SpecExpr ')' ';'

     SpaceExpr ::= '\space' '(' SpecExpr ')'

     IsInitializedExpr ::= '\is_initialized' '(' Idn ')' ';'

     InvariantFor ::= '\invariant_for' '(' SpecExpr ')' ';'

     WorkingSpaceClause ::= WorkingSpaceKeyword '\not_specified' ';'
     | WorkingSpaceKeyword WorkingSpaceSpecExpr [ 'if' predicate ] ';'

     WorkingSpaceSpecExpr ::= SpecExpr (of type int) OpWithIntResult WorkingSpaceSpecExpr
     | '\working_space' '(' MethodInvOrConstructor ')' IntOp WorkingSpaceSpecExpr

     MethodInvOrConstructor ::= MethodInvocation | ConstructorInvocation

     OpWithIntResult ::= STAR | '/' | '%' | PLUS | '-' | '&' | BITOR | '^'

     WorkingSpaceKeyword ::= 'working_space' | 'working_space_redundantly'

     DurationKeyword ::= 'duration' | 'duration_redundantly'

     PrivateDataKeyword ::= '\private_data'

     NotModifiedExpr ::= '\not_modified' '(' SpecDesignator [',' SpecDesignator]* ')' ';'

     ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';'

     FieldsOfExpr ::= '\fields_of' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';'

     OtherExpr ::= '\other' [ StoreRefNameSuffix ] ';'

     ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';'

     StoreRefList ::= StoreRef [ ',' StoreRef ] ...

     StoreRef ::= StoreRefExpr
     | FieldsOfExpr
     | InformalDescription
     | StoreRefKeyword

     StoreRefExpr ::= StoreRefName [ StoreRefNameSuffix ] ...

     StoreRefName ::= Idn | 'super' | 'this'

     StoreRefNameSuffix ::= '.' Idn | '.' 'this' | '[' SpecArrayRefExpr ']'

     SpecArrayRefExpr ::= SpecExpr | SpecExpr '..' SpecExpr | '*'

     StoreRefKeyword ::= '\nothing' | '\everything' | '\not_specified' | '\private_data'

     ConditionalStoreRefList ::= ConditionalStoreRef [ ',' ConditionalStoreRef ] ...

     ConditionalStoreRef ::= StoreRef [ 'if' Predicate ]

     InformalDescription ::= '(*' NonStarClose [ NonStarClose ] ... '*)'

     NonStarClose ::= NonStar | StarsNonClose

     StarsNonClose ::= '*' [ '*' ] ... NonClose

     NonClose ::= any character except ')'

The grammar of SpecExpr is:

     SpecExpr:
     Name
     | \result
     | \lockset
     | this
     | Literal
     | SpecExpr '.' Idn
     | SpecExpr '[' SpecExpr ']'
     | UnOp SpecExpr
     | '(' Type ')' SpecExpr
     | SpecExpr BinOp SpecExpr
     | SpecExpr 'instanceof' Type
     | Function '(' [ SpecExpr [ ',' SpecExpr ]* ] ')'
     | '\type' '(' Type ')'
     | SpecExpr '?' SpecExpr ':' SpecExpr
     | '(' {'\forall'|'\exists'} Type Idn [',' Idn]* ';' [[SpecExpr] ';'] SpecExpr ')'
     | '(' {'\lblpos'|'\lblneg'} Idn SpecExpr ')'
     | '(' SpecExpr ')'
     | Name '.' this                         [1.1]
     | Name ([])* '.' class                  [1.1]
     | JmlSpecExpr

     JmlSpecExpr ::= '\nothing' | '\everything' | '\not_specified'

     Function ::= '\fresh' | '\nonnullelements' | '\elemtype' | '\max' | '\old'
     | '\typeof' | '\not_modified' | '\nowarn' | '\nowarn_op' | '\warn' | '\warn_op'
     | '\java_math' | '\safe_math' | \bigint_math

     UnOp ::= '+' | '-' | '!' | '~'

     BinOp ::= '+' | '-' | '*' | '/' | '%' | '<<' | '>>' | '>>>'
     | '<' | '<=' | '==' | '!=' | '>=' | '>'
     | '&' | '|' | '^' | '&&' | '||'

Also, the grammar for Type is extended (recursively) with the new base type 'TYPE'.

Expressions in redundant specifications (e.g., requires_redundantly ...) are only parsed if `Main.checkRedundantSpecs` is true.

See Also:
  `Options.checkRedundantSpecs`
Todo:
  kiniry 24 Jan 2003 - Make semicolon at end of 'nowarn' lexical pragma non-optional. This requires updating spec files &c., kiniry 24 Jan 2003 - Permit splitting syntactic constructs across multiple @code{//@@} comments., kiniry 19 May 2003 - Need to add grammar expressions above for constraints., kiniry 9 July 2003 - Support for \not_specified is scattered all over the code right now---perhaps we can refactor and clean up? It is sometimes parsed and discarded, sometimes recognized and ignored, etc.
Note:
  'SC' == Statically Checkable or otherwise useful 'HPT' == Handle at Parse-time 'AAST' == 'Augments Abstract Symbol Tree' Final 0-5 indicates difficulty of implementation; 0 being easiest. All estimates and implementation/design guesses were made by Joe Kiniry on 29 April 2003., kiniry 24 Jan 2003 - All rules named Jml* added by kiniry@cs.kun.nl starting on 24 Jan 2003.

Nested Class Summary
`protected class` | `EscPragmaParser.SavedPragma`

Field Summary
`private boolean` | `argListInAnnotation`
`private static boolean` | `DEBUG`
`private java.lang.String` | `endTag`
`static ASTDecoration` | `informalPredicateDecoration` The informal-predicate decoration is associated with a true-valued boolean literal expression, if the concrete syntax of this expression was an informal comment.
`(package private) boolean` | `inModelRoutine`
`(package private) boolean` | `inModelType`
`private int` | `inProcessLoc`
`private int` | `inProcessTag` The value NOTHING_ELSE_TO_PROCESS means there is nothing else to process.
`(package private) static int` | `maxAnnotationNestingLevel` Maximum # of levels of nesting of annotation comments allowed. 0 == no nesting of annotation comments allowed.
`protected int` | `modifiers`
`int` | `NEXT_TOKEN_STARTS_NEW_PRAGMA`
`int` | `NOTHING_ELSE_TO_PROCESS`
`private CorrelatedReader` | `pendingJavadocComment`
`private java.util.LinkedList` | `pragmaQueue`
`(package private) ModifierPragma` | `savedGhostModelPragma`
`private EscPragmaLex` | `scanner` The lexer associated with this pragma parser from which we will read tokens.

Fields inherited from class javafe.parser.Parse
`seqFormalParaDecl, seqImportDecl, seqTypeDecl, seqTypeName`

Fields inherited from class javafe.parser.ParseStmt
`seqCatchClause, seqStmt`

Fields inherited from class javafe.parser.ParseExpr
`seqExpr, seqTypeDeclElem, seqVarInit`

Fields inherited from class javafe.parser.ParseType
`seqIdentifier`

Fields inherited from class javafe.parser.ParseUtil
`modifierKeywords, modifierPragmas, seqModifierPragma`

Constructor Summary
`EscPragmaParser()` Constructs a new pragma parser with zero nesting level.
`EscPragmaParser(int level)` Constructs a new prama parser at the indicated nesting level.

Method Summary
`protected void` | `addStmt(Lex l)` Internal method for parsing a `Stmt`.
`private void` | `checkNoModifiers(int tag, int loc)` Issues an error if any Java modifiers have accumulated, and resets the accumulated modifiers to NONE.
`boolean` | `checkTag(int tag)` Decide whether a comment contains pragmas.
`void` | `close()` Closes this pragma parser including its scanner and pending Javadoc comment.
`private void` | `continuePragma(Token dst)`
`private void` | `eatAts(CorrelatedReader in)` Eats any extra @ symbols.
`private void` | `eatSemiColon(Identifier kw)` Eat the next token if it is a semi-colon and, if the next token is a pragma (not EOF, thus not the end of the pragma) then issue an error message indicating that the specified identifier must be semi-colon terminated if it is followed by more pragmas.
`private void` | `eatThroughSemiColon()` Eat tokens up through and including terminating semi-colon.
`private void` | `eatUpToCommaOrSemiColon()`
`private void` | `eatWizardComment(CorrelatedReader in)` Eat any wizard inserted comment at the start of an escjava annotation.
`boolean` | `getNextPragma(Token dst)` Parse the next pragma, putting information about it in the provided token `dst`, and return a flag indicating if there are further pragmas to be parsed.
`boolean` | `getNextPragmaHelper(Token dst)`
`boolean` | `getPragma(Token dst)`
`FieldDecl` | `isPragmaDecl(Token l)`
`boolean` | `isPrimitiveKeywordTag(int tag)` Is a `tag` a PrimitiveType keyword?
`boolean` | `isStartOfUnaryExpressionNotPlusMinus(int tag)` Determines whether the tag is the first token of a `UnaryExpressionNotPlusMinus`.
`private void` | `noteUnsupportedCheckableJmlPragma(int loc, int tag)` Emit a caution to the user if verbosity is enabled that the supplied tag at the specified location is unsupported by the current version of ESC/Java but is statically checkable.
`boolean` | `parseConstructorDeclTail(Token dst, int loc, Type type, int locType, ModifierPragmaVec modifierPragmas)`
`boolean` | `parseDeclaration(Token dst, int loc, int kwtag)` Parses a declaration that appears in a ghost or model annotation - can be a ghost or model field or a model method or constructor.
`FormalParaDecl` | `parseExsuresFormalParaDecl(EscPragmaLex l)` Parse the formal parameter declaration (the type and name of the associated exception) of an `exsures` or `signals` pragma.
`PrimitiveType` | `parseExsuresPrimitiveType(EscPragmaLex l)` Parse the primitive type used in an `exsures` or `signals` pragma.
`Type` | `parseExsuresPrimitiveTypeOrTypeName(EscPragmaLex l)` Parse the type associated with an `exsures` or `signals` pragma parameter.
`Type` | `parseExsuresType(EscPragmaLex l)` Parse the type of the of an `exsures` or `signals` pragma parameter.
`TypeName` | `parseExsuresTypeName(EscPragmaLex l)` Parse the type name used in an `exsures` or `signals` pragma.
`boolean` | `parseFieldDeclTail(Token dst, int loc, int locId, Type type, Identifier id, ModifierPragmaVec modifierPragmas)`
`FormalParaDeclVec` | `parseFormalParameterList(Lex l)` Parse a `FormalParameterList`, which includes enclosing parens.
`java.util.LinkedList` | `parseGroupList()`
`private boolean` | `parseInPragmas(int tag, int loc, Token dst, boolean first)`
`void` | `parseJavaModifiers()`
`Expr` | `parseMapsMemberFieldRef(Lex scanner)`
`boolean` | `parseMethodDeclTail(Token dst, int loc, Type type, int locType, Identifier id, int locId, ModifierPragmaVec modifierPragmas)`
`protected Expr` | `parsePrimaryExpression(Lex l)` Parse a "primary expression" from `l`.
`protected Expr` | `parsePrimarySuffix(Lex l, Expr primary)` Parse the suffix of a "primary expression" from `l`, given the prefix primary expression `primary`.
`PrimitiveType` | `parsePrimitiveType(Lex l)` Parses a PrimitiveType.
`private GCExpr` | `parseQuantifierRemainder(Lex l, int tag, Type type, int loc)` Parse the balance (everything after the quantifier to the end of the current quantified scope) of a quantifier expression from `l`.
`Expr` | `parseStoreRef(EscPragmaLex l)` Parse a StoreRef
`Expr` | `parseStoreRefExpr(EscPragmaLex l)` Parse a StoreRefExpr
`protected TypeDeclElem` | `parseTypeDeclElemIntoSeqTDE(Lex l, int keyword, Identifier containerId, boolean specOnly)` Parse a `TypeDeclElem`, which is either a field, method, or constructor declaration, a static block, or a TypeDecl [1.1].
`protected TypeDecl` | `parseTypeDeclTail(Lex l, boolean specOnly, int loc, int modifiers, ModifierPragmaVec modifierPragmas)` Parse a `TypeDeclTail` (ie a class or interface declaration starting at the keyword 'class' or 'interface').
`boolean` | `parseTypeDeclTail(Token dst, int loc)`
`private boolean` | `processJavadocComment()` Parse embedded <esc&gr; ...
`void` | `restart(CorrelatedReader in, boolean eolComment)` Restart a pragma parser on a new input stream.
`void` | `savePragma(int l, int t, java.lang.Object o)`
`void` | `savePragma(Token d)`
`private int` | `scanFor(CorrelatedReader in, java.lang.String match)` Scans input stream for a string matching the parameter `match`.
`private int` | `scanForOpeningTag(CorrelatedReader in)` Scans for one of <esc> <jml> <ESC> <JML>.

Methods inherited from class javafe.parser.Parse
`parseCompilationUnit, parseImportDeclaration, parseStream, parseTypeDeclaration, parseTypeDeclaration, parseTypeNames`

Methods inherited from class javafe.parser.ParseStmt
`isStatementExpression, parseBlock, parseConstructorBody, parseFormalParaDecl, parseStatement`

Methods inherited from class javafe.parser.ParseExpr
`addOperator, parseArgumentList, parseArrayInitializer, parseCastExpression, parseClassLiteralSuffix, parseExpression, parseExpressionList, parseNewExpression, parseNewExpressionTail, parseSuper, parseUnaryExpression, parseVariableInitializer`

Methods inherited from class javafe.parser.ParseType
`parseBracketPairs, parseIdentifier, parseName, parsePrimitiveTypeOrTypeName, parseType, parseTypeModifierPragmas, parseTypeName`

Methods inherited from class javafe.parser.ParseUtil
`arrayToString, error, expect, fail, getJavaModifier, isJavaModifier, parseModifierPragmas, parseModifiers, parseMoreModifierPragmas`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### DEBUG

    private static final boolean DEBUG

See Also:
  Constant Field Values

### informalPredicateDecoration

    public static final ASTDecoration informalPredicateDecoration

  The informal-predicate decoration is associated with a true-valued boolean literal expression, if the concrete syntax of this expression was an informal comment. The value associated with the decoration is the string of the informal predicate (i.e., the comment itself).

### scanner

    private EscPragmaLex scanner

  The lexer associated with this pragma parser from which we will read tokens.

### NOTHING_ELSE_TO_PROCESS

    public int NOTHING_ELSE_TO_PROCESS

### NEXT_TOKEN_STARTS_NEW_PRAGMA

    public int NEXT_TOKEN_STARTS_NEW_PRAGMA

### inProcessTag

    private int inProcessTag

  The value NOTHING_ELSE_TO_PROCESS means there is nothing else to process. The value NEXT_TOKEN_STARTS_NEW_PRAGMA means there is something to process and the next thing to read begins a new pragma (or ends the pragma-containing comment). The other values indicate that the pragma parser is in the middle of parsing some pragma, and is expected to continue this parsing next time it gets control.

### inProcessLoc

    private int inProcessLoc

### pendingJavadocComment

    private CorrelatedReader pendingJavadocComment

### maxAnnotationNestingLevel

    static final int maxAnnotationNestingLevel

  Maximum # of levels of nesting of annotation comments allowed. 0 == no nesting of annotation comments allowed.

  If you change this, change the error message in EscPragmaParser(int) below as well.

  See Also:
    Constant Field Values

### endTag

    private java.lang.String endTag

### pragmaQueue

    private java.util.LinkedList pragmaQueue

### savedGhostModelPragma

    ModifierPragma savedGhostModelPragma

### modifiers

    protected int modifiers

### argListInAnnotation

    private boolean argListInAnnotation

### inModelType

    boolean inModelType

### inModelRoutine

    boolean inModelRoutine

Constructor Detail

### EscPragmaParser

    public EscPragmaParser()

  Constructs a new pragma parser with zero nesting level.

See Also:
  `EscPragmaParser(int)`

### EscPragmaParser

    public EscPragmaParser(int level)

  Constructs a new prama parser at the indicated nesting level.

Parameters:
  `level` - the nesting level of this instance.

Method Detail

### checkTag

    public boolean checkTag(int tag)

  Description copied from interface: `PragmaParser`
  Decide whether a comment contains pragmas. When it encounters a comment, a `Lex` object passes the first character of the comment to the `checkTag` method of its `PragmaParser`. If this call returns false, the comment is assumed to contain no pragmas and thus is discarded. If this call returns true, the comment may contain pragmas, so it is converted into a `CorrelatedReader` and passed to `restart`. (The `tag` argument is either a `char` or `-1`; `-1` indicates the empty comment.)

  Specified by:
    `checkTag` in interface `PragmaParser`
  Parameters:
    `tag` - the comment tag character to check.
  Returns:
    true iff tag is an '@' or an '*' character.

### restart

    public void restart(CorrelatedReader in,
                        boolean eolComment)

  Restart a pragma parser on a new input stream. If `this` is already opened on another `CorrelatedReader`, close the old reader.

  Specified by:
    `restart` in interface `PragmaParser`
  Parameters:
    `in` - the reader from which to read.
    `eolComment` - a flag that indicates we are parsing an EOL comment (a comment that starts with "//").

### processJavadocComment

    private boolean processJavadocComment()
                                   throws java.io.IOException

  Parse embedded <esc&gr; ... </esc> in Javadoc comments.

  Returns:
    a flag indicating if an embedded comment was recognized.
  Throws:
    `java.io.IOException` - if something goes wrong during reading.

### eatAts

    private void eatAts(CorrelatedReader in)
                 throws java.io.IOException

  Eats any extra @ symbols.

  Throws:
    `java.io.IOException`

### eatWizardComment

    private void eatWizardComment(CorrelatedReader in)
                           throws java.io.IOException

  Eat any wizard inserted comment at the start of an escjava annotation.

  May side-effect the mark of `in`.

  Eats "([^)]*)", if present, from `in`.

  Parameters:
    `in` - the stream from which to read.
  Throws:
    `java.io.IOException`

### scanFor

    private int scanFor(CorrelatedReader in,
                        java.lang.String match)
                 throws java.io.IOException

  Scans input stream for a string matching the parameter `match`. Only works if the first character is not repeated in the string.

  If present, the location of the match is returned. If not present, `Location.NULL` is returned.

  Requires that `in` is not closed.

  Parameters:
    `in` - the stream from which to read.
    `match` - the string to match against the input stream.
  Returns:
    the location of the match, or `Location.NULL` if there is no match.
  Throws:
    `java.io.IOException`

### scanForOpeningTag

    private int scanForOpeningTag(CorrelatedReader in)
                           throws java.io.IOException

  Scans for one of <esc> <jml> <ESC> <JML>. This is hard-coded to simplify the code. Also sets the variable endTag to the corresponding tag that closes the opening tag that was found (null if none was found).

  Throws:
    `java.io.IOException`

### close

    public void close()

  Closes this pragma parser including its scanner and pending Javadoc comment.

  Specified by:
    `close` in interface `PragmaParser`

### savePragma

    public void savePragma(int l,
                           int t,
                           java.lang.Object o)

### savePragma

    public void savePragma(Token d)

### getPragma

    public boolean getPragma(Token dst)

### getNextPragma

    public boolean getNextPragma(Token dst)

  Parse the next pragma, putting information about it in the provided token `dst`, and return a flag indicating if there are further pragmas to be parsed. Note: All worrying about 'also' is now done during the desugaring of specs. JML style of using also is preferred.

  Specified by:
    `getNextPragma` in interface `PragmaParser`
  Parameters:
    `dst` - the token in which to store information about the current pragma.
  Returns:
    a flag indicating if further pragmas need to be parsed.
  See Also:
    `Lex`

### getNextPragmaHelper

    public boolean getNextPragmaHelper(Token dst)

### checkNoModifiers

    private void checkNoModifiers(int tag,
                                  int loc)

  Issues an error if any Java modifiers have accumulated, and resets the accumulated modifiers to NONE.

### noteUnsupportedCheckableJmlPragma

    private void noteUnsupportedCheckableJmlPragma(int loc,
                                                   int tag)

  Emit a caution to the user if verbosity is enabled that the supplied tag at the specified location is unsupported by the current version of ESC/Java but is statically checkable.

### eatThroughSemiColon

    private void eatThroughSemiColon()

  Eat tokens up through and including terminating semi-colon. This method is used to pretend like we are parsing semi-colon-terminated expressions in pragmas that we do not yet really parse or handle.

### eatUpToCommaOrSemiColon

    private void eatUpToCommaOrSemiColon()

### eatSemiColon

    private void eatSemiColon(Identifier kw)

  Eat the next token if it is a semi-colon and, if the next token is a pragma (not EOF, thus not the end of the pragma) then issue an error message indicating that the specified identifier must be semi-colon terminated if it is followed by more pragmas.

### continuePragma

    private void continuePragma(Token dst)
                         throws java.io.IOException

  Throws:
    `java.io.IOException`

### parsePrimaryExpression

    protected Expr parsePrimaryExpression(Lex l)

  Parse a "primary expression" from `l`. A primary expression is an expression of the form:

       \result
       \lockset
       (*...*)
       Function '('
       '\type' '('
       '(' {'\forall'|'\exists'} Type
       '(' {'\lblpos'|'\lblneg'} Idn

  or is a "normal" primary expression parsed with `ParseExpr.parsePrimaryExpression()`.

  Overrides:
    `parsePrimaryExpression` in class `ParseExpr`
  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed expression.
  See Also:
    `ParseExpr.parsePrimaryExpression(javafe.parser.Lex)`

### parsePrimarySuffix

    protected Expr parsePrimarySuffix(Lex l,
                                      Expr primary)

  Parse the suffix of a "primary expression" from `l`, given the prefix primary expression `primary`.

  Overrides:
    `parsePrimarySuffix` in class `ParseExpr`
  Parameters:
    `l` - the lexer from which to read and parse.
    `primary` - the primary expression previously parsed.
  Returns:
    the parsed expression.

### parseQuantifierRemainder

    private GCExpr parseQuantifierRemainder(Lex l,
                                            int tag,
                                            Type type,
                                            int loc)

  Parse the balance (everything after the quantifier to the end of the current quantified scope) of a quantifier expression from `l`.

  Parameters:
    `l` - the lexer from which to read and parse.
    `tag` - identifies which kind of quantifier we are parsing.
    `type` - the type of the quantified variable.
    `loc` - the starting location of the quantified expression.
  Returns:
    the parsed quantified expression.

### isPrimitiveKeywordTag

    public boolean isPrimitiveKeywordTag(int tag)

  Is a `tag` a PrimitiveType keyword? Overriden to add type `TYPE`.

  Overrides:
    `isPrimitiveKeywordTag` in class `ParseType`
  Parameters:
    `tag` - the tag to check.
  Returns:
    a flag indicating if the supplied parameter is a primate type.

### parsePrimitiveType

    public PrimitiveType parsePrimitiveType(Lex l)

  Parses a PrimitiveType. Overriden to add type TYPE. Returns `null` on failure.

  PrimitiveType is one of: boolean byte short int long char float double void TYPE.

  Overrides:
    `parsePrimitiveType` in class `ParseType`
  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed primative type.

### isStartOfUnaryExpressionNotPlusMinus

    public boolean isStartOfUnaryExpressionNotPlusMinus(int tag)

  Description copied from class: `ParseExpr`
  Determines whether the tag is the first token of a `UnaryExpressionNotPlusMinus`. For the default Java grammar, this amounts to is tag one of: ~ ! Literal Id this new super LPAREN However, it is expected that grammar extensions may extend this list.

  Overrides:
    `isStartOfUnaryExpressionNotPlusMinus` in class `ParseExpr`
  Parameters:
    `tag` - the tag to check.
  Returns:
    a flag indicating if `tag` is the start of an unary expression other than unary '+' or '-'. Overridded to handle new identifier-like keywords "\result" and "\lockset".

### parseExsuresFormalParaDecl

    public FormalParaDecl parseExsuresFormalParaDecl(EscPragmaLex l)

  Parse the formal parameter declaration (the type and name of the associated exception) of an `exsures` or `signals` pragma. This is a bit complicated because these expressions have an optional identifier name associated with the specified Throwable type.

  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed formal paramater declaration.

### parseExsuresType

    public Type parseExsuresType(EscPragmaLex l)

  Parse the type of the of an `exsures` or `signals` pragma parameter.

  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed type declaration.

### parseExsuresPrimitiveTypeOrTypeName

    public Type parseExsuresPrimitiveTypeOrTypeName(EscPragmaLex l)

  Parse the type associated with an `exsures` or `signals` pragma parameter.

  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed type declaration.

### parseExsuresPrimitiveType

    public PrimitiveType parseExsuresPrimitiveType(EscPragmaLex l)

  Parse the primitive type used in an `exsures` or `signals` pragma.

  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed type declaration, if the type is primative.

### parseExsuresTypeName

    public TypeName parseExsuresTypeName(EscPragmaLex l)

  Parse the type name used in an `exsures` or `signals` pragma.

  Parameters:
    `l` - the lexer from which to read and parse.
  Returns:
    the parsed type declaration.

### parseStoreRef

    public Expr parseStoreRef(EscPragmaLex l)

  Parse a StoreRef

### parseStoreRefExpr

    public Expr parseStoreRefExpr(EscPragmaLex l)

  Parse a StoreRefExpr

### parseJavaModifiers

    public void parseJavaModifiers()

### parseFormalParameterList

    public FormalParaDeclVec parseFormalParameterList(Lex l)

  Description copied from class: `Parse`
  Parse a `FormalParameterList`, which includes enclosing parens. Note: this definition differs from JLS, where it does not include the parens

            FormalParameterList:
              LPAREN FormalParameter (, FormalParameter)* RPAREN

            FormalParameter:
              [Modifiers] Type Identifier BracketPair* ModifierPragma*     [1.1]

  Overrides:
    `parseFormalParameterList` in class `Parse`

### parseDeclaration

    public boolean parseDeclaration(Token dst,
                                    int loc,
                                    int kwtag)

  Parses a declaration that appears in a ghost or model annotation - can be a ghost or model field or a model method or constructor.

  Returns:
    true if a terminating semicolon is expected next

### parseTypeDeclTail

    public boolean parseTypeDeclTail(Token dst,
                                     int loc)

### addStmt

    protected void addStmt(Lex l)

  Description copied from class: `ParseStmt`
  Internal method for parsing a `Stmt`.

  Effects: Parses a single `Stmt` according to the grammar at the top of this file. If no syntax errors are encountered, it adds one or more `Stmt` to `seqStmt`, leaving `l` at the token just after the trailing `}` of the statement. More than one statement is added only in the case of variable declarations that declare more than one variable.

  Overrides:
    `addStmt` in class `ParseStmt`

### parseTypeDeclElemIntoSeqTDE

    protected TypeDeclElem parseTypeDeclElemIntoSeqTDE(Lex l,
                                                       int keyword,
                                                       Identifier containerId,
                                                       boolean specOnly)

  Description copied from class: `Parse`
  Parse a `TypeDeclElem`, which is either a field, method, or constructor declaration, a static block, or a TypeDecl [1.1].

  A field declaration may define many fields. Since returning multiple declared entities is cumbersome, this method simply adds all the declared entities onto the StackVector seqTypeDeclElem. The `keyword` argument is either CLASS or INTERFACE. The argument containerId is the name of the enclosing class, which is necessary for checking constructor declarations.

      TypeDeclElem:
         FieldDeclaration
         MethodDeclaration
         ConstructorDeclaration
         InitBlock
         TypeDeclElemPragma
         TypeDeclaration              [1.1]
         ;

      FieldDeclaration:
         Modifiers Type VariableDeclarator (, VariableDeclarator)* ;

      MethodDeclaration:
         Modifiers Type Identifier FormalParameterList BracketPair*
            [throws TypeNameList]
            ( ; | Block )

      ConstructorDeclaration:
         Modifiers Identifier FormalParameterList Block

      InitBlock:
         Modifiers Block

      VariableDeclarator:
         Identifier BRACKET_PAIR* [ = VariableInitializer ]

  Overrides:
    `parseTypeDeclElemIntoSeqTDE` in class `Parse`
  See Also:
    `TagConstants`

### parseTypeDeclTail

    protected TypeDecl parseTypeDeclTail(Lex l,
                                         boolean specOnly,
                                         int loc,
                                         int modifiers,
                                         ModifierPragmaVec modifierPragmas)

  Description copied from class: `Parse`
  Parse a `TypeDeclTail` (ie a class or interface declaration starting at the keyword 'class' or 'interface').

            TypeDeclTail:
              class Identifier [TypeModifierPragma]* [extends TypeName] [implements TypeNameList]
                { TypeDeclElem* }
              interface Identifier [TypeModifierPragma]* [extends TypeNameList] { TypeDeclElem* }

  Overrides:
    `parseTypeDeclTail` in class `Parse`

### parseFieldDeclTail

    public boolean parseFieldDeclTail(Token dst,
                                      int loc,
                                      int locId,
                                      Type type,
                                      Identifier id,
                                      ModifierPragmaVec modifierPragmas)

### parseConstructorDeclTail

    public boolean parseConstructorDeclTail(Token dst,
                                            int loc,
                                            Type type,
                                            int locType,
                                            ModifierPragmaVec modifierPragmas)

### parseMethodDeclTail

    public boolean parseMethodDeclTail(Token dst,
                                       int loc,
                                       Type type,
                                       int locType,
                                       Identifier id,
                                       int locId,
                                       ModifierPragmaVec modifierPragmas)

### isPragmaDecl

    public FieldDecl isPragmaDecl(Token l)

  Specified by:
    `isPragmaDecl` in interface `PragmaParser`

### parseMapsMemberFieldRef

    public Expr parseMapsMemberFieldRef(Lex scanner)

### parseInPragmas

    private boolean parseInPragmas(int tag,
                                   int loc,
                                   Token dst,
                                   boolean first)

### parseGroupList

    public java.util.LinkedList parseGroupList()

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage