org.jmlspecs.checker
Class TokenStreamSelector

java.lang.Object
  antlr.TokenStreamSelector
      org.jmlspecs.checker.TokenStreamSelector

All Implemented Interfaces:

antlr.TokenStream

public class TokenStreamSelector

extends antlr.TokenStreamSelector

Provides for switching between various lexical analyzers for lexing JML. Extends antlr.TokenStreamSelector by providing some shared state for the lexical analyzers. This shared state tracks whether the IDENTs being lexed appear in a regular Java context, a regular JML annotation context, or within a JML expression. The same IDENT is matched against a different set of keywords in the different contexts.

Version:

$Revision: 1.9 $

Author:

Curtis Clifton

Field Summary
private  boolean	allowUniverseKeywords
private  CToken	HACKED_AFFIRM_LITERAL_TOKEN           This token is returned whenever an assert token is lexed inside a JML annotation.
private static Object	INEXPRESSION
protected  boolean	inJMLExpression           Flag indicates whether we are lexing within a JML expression.
private  boolean	inJMLModelMethodConstructorHeader           Flag indicates whether we are lexing within the header of a model method or constructor declaration.
private  boolean	inJMLModelTypeHeader           Flag indicates whether we are lexing within the header of a model class or interface declaration.
private  boolean	inQuantifier           Flag indicates whether we are lexing within a JML quantifier expression.
private  LinkedList	intstack           This stack keeps track of parenthesis nesting level as we move into inner {} contexts.
private static Object	MODELCONSTRUCTOR
private static Object	MODELTYPE
private static Object	NOTINEXPRESSION
private  int	parenCount           Count of the number of left parens without matching right parens found within a JML expression.
private  LinkedList	rstack           This stack keeps track of the different kinds of {} contexts we are in within what is at the top level a JML expression.

 

Fields inherited from class antlr.TokenStreamSelector

input, inputStreamNames, streamStack

 

Constructor Summary

TokenStreamSelector()

 

Method Summary
void	lexedLCurly()
void	lexedLeftParen()
void	lexedRCurly(antlr.Token tok)
void	lexedRightParen()
void	lexedSemicolon()
CToken	lookupJMLToken(char[] charCache, int start, int tokenLen)           Returns the appropriate token for the JML ident contained in charCache[start]..charCache[start+length], or null if no JML ident is appropriate.
protected  CToken	lookupKeyword(char[] charCache, int start, int tokenLen)           Looks up keywords.
void	setAllowUniverseKeywords(boolean flag)           WMD

 

Methods inherited from class antlr.TokenStreamSelector

addInputStream, getCurrentStream, getStream, nextToken, pop, push, push, retry, select, select

 

Methods inherited from class java.lang.Object

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

 

Field Detail

inJMLExpression

protected boolean inJMLExpression

Flag indicates whether we are lexing within a JML expression. Used to switch between keyword tables for resolving IDENTs.

inJMLModelTypeHeader

private boolean inJMLModelTypeHeader

Flag indicates whether we are lexing within the header of a model class or interface declaration. Used to switch between keyword tables for resolving IDENTs.

inJMLModelMethodConstructorHeader

private boolean inJMLModelMethodConstructorHeader

Flag indicates whether we are lexing within the header of a model method or constructor declaration. Used to switch between keyword tables for resolving IDENTs.

inQuantifier

private boolean inQuantifier

Flag indicates whether we are lexing within a JML quantifier expression. Used to detect whether or not a ';' indicates the end of a JML expression.

parenCount

private int parenCount

Count of the number of left parens without matching right parens found within a JML expression. Used to detect whether or not a ';' indicates the end of a JML expression.

allowUniverseKeywords

private boolean allowUniverseKeywords

HACKED_AFFIRM_LITERAL_TOKEN

private CToken HACKED_AFFIRM_LITERAL_TOKEN

This token is returned whenever an assert token is lexed inside a JML annotation.

intstack

private LinkedList intstack

This stack keeps track of parenthesis nesting level as we move into inner {} contexts.

rstack

private LinkedList rstack

This stack keeps track of the different kinds of {} contexts we are in within what is at the top level a JML expression.

MODELTYPE

private static final Object MODELTYPE

MODELCONSTRUCTOR

private static final Object MODELCONSTRUCTOR

INEXPRESSION

private static final Object INEXPRESSION

NOTINEXPRESSION

private static final Object NOTINEXPRESSION

TokenStreamSelector

public TokenStreamSelector()

lexedLeftParen

public final void lexedLeftParen()

lexedRightParen

public final void lexedRightParen()

lexedSemicolon

public final void lexedSemicolon()

lexedLCurly

public final void lexedLCurly()

lexedRCurly

public final void lexedRCurly(antlr.Token tok)

lookupJMLToken

public final CToken lookupJMLToken(char[] charCache,
                                   int start,
                                   int tokenLen)

Returns the appropriate token for the JML ident contained in charCache[start]..charCache[start+length], or null if no JML ident is appropriate. The token table searched depends on whether or the lexical analyzers are processing a JML expression or just a regular annotation. The result of this method is only valid if the lexical analysis is actually processing an annotation. Note the various logic in this class for keeping track of whether inJMLExpression should be true or false. We have to do this based on the token stream - hence the calls alerting to the processing of various punctuation marks. If we try invoking some information from the parser, we will get in trouble, because the lexer is a few tokens ahead of the parser, because of lookahead (and the amount will vary depending on what lookahead various rules of the grammar need). The essential piece of logic is that a semicolon terminates a JML expression, as long as it is not inside braces or parentheses (as in quantifier expressions). Note that within an expression one can have method calls on anonymous classes that contain method definitions - full-fledged code. So maintaining inJMLExpression is tricky. You are welcome to improve on what is here (but test it well!) - DRCok 7/25/2003

 requires (* token in charCache appears inside a JML annotation *);
 

lookupKeyword

protected CToken lookupKeyword(char[] charCache,
                               int start,
                               int tokenLen)

Looks up keywords. If the current token is not a keyword, null is returned.

setAllowUniverseKeywords

public void setAllowUniverseKeywords(boolean flag)

WMD