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

escjava.parser
Class EscPragmaParser

java.lang.Object
  extended byjavafe.parser.ParseUtil
      extended byjavafe.parser.ParseType
          extended byjavafe.parser.ParseExpr
              extended byjavafe.parser.ParseStmt
                  extended byjavafe.parser.Parse
                      extended byescjava.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()

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

The ESC/Java2 Project Homepage