JML

org.jmlspecs.checker
Class TokenStreamSelector

java.lang.Object
  extended byantlr.TokenStreamSelector
      extended byorg.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
Constructor Detail

TokenStreamSelector

public TokenStreamSelector()
Method Detail

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


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.