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_by_default' | 'nullable_by_default' 
 | 'non_null' | 'nullable' 
 | 'instance' 
 | 'pure' | 'obs_pure'
 | 'spec_public' | 'writable_deferred' | 'helper' 
 | 'public' | 'private' | 'protected' 
 | 'spec_protected' | 'model' | 'transient' | '\peer' | '\readonly' | '\rep'
 | '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, universeArray, universeLevel, useUniverses

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, getElementUniverse, getJavaModifier, getUniverse, isJavaModifier, parseModifierPragmas, parseModifiers, parseMoreModifierPragmas, parseUniverses, setElementUniverse, setUniverse, setUniverse, setUniverse

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()