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 JmlCorrelatedReader

java.lang.Object
  extended byjavafe.util.CorrelatedReader
      extended byjavafe.util.FilterCorrelatedReader
          extended byescjava.parser.JmlCorrelatedReader

public class JmlCorrelatedReader
extends FilterCorrelatedReader

This FilterCorrelatedReader creates the illusion that the additional \@-signs, etc. allowed in the JML annotation syntax are really just whitespace.

Author:
Rustan Leino
See Also:
FilterCorrelatedReader

Field Summary
private  boolean allowSpecialSuffix
          Indicates whether or not a sequence of consecutive special characters at the end of the comment are to be treated as white space.
static int C_COMMENT
           
static int COMMENTS_KINDS
           
static int EOL_COMMENT
           
static int JAVADOC_COMMENT
           
private  int lastUnreturnedChar
          If there are unreturned characters, lastUnreturnedChar indicates the last of these characters.
private  int lastUnreturnedCharAtMark
           
private  int prefixMode
          The lines of the input consist of (0) a number of whitespace characters, (1) a number of special characters ('@' in ordinary comments and '*' inside Javadoc comments), and followed by (2) the "real meat".
private  int prefixModeAtMark
           
private  int specialCharacter
          Indicates the special character.
private  int unreturnedChars
          This variable is included so that @-signs at the end of a pragma-containing comment can be ignored.
private  int unreturnedCharsAtMark
           
 
Fields inherited from class javafe.util.FilterCorrelatedReader
child
 
Fields inherited from class javafe.util.CorrelatedReader
marked
 
Constructor Summary
protected JmlCorrelatedReader(CorrelatedReader child, int commentKind)
          Constructs a JmlCorrelatedReader with child as the underlying CorrelatedReader.
 
Method Summary
 int getLocation()
          Returns the location of the last character read.
 void mark()
          See documentation in superclass.
 int read()
          Reads the next character from this input stream.
 void reset()
          See documentation in superclass.
 
Methods inherited from class javafe.util.FilterCorrelatedReader
clearMark, close, createReaderFromMark, getFile
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

EOL_COMMENT

public static final int EOL_COMMENT
See Also:
Constant Field Values

C_COMMENT

public static final int C_COMMENT
See Also:
Constant Field Values

JAVADOC_COMMENT

public static final int JAVADOC_COMMENT
See Also:
Constant Field Values

COMMENTS_KINDS

public static final int COMMENTS_KINDS
See Also:
Constant Field Values

prefixMode

private int prefixMode
The lines of the input consist of (0) a number of whitespace characters, (1) a number of special characters ('@' in ordinary comments and '*' inside Javadoc comments), and followed by (2) the "real meat". The variable prefixMode indicates which of these three segments are currently being scanned.


specialCharacter

private final int specialCharacter
Indicates the special character.


unreturnedChars

private int unreturnedChars
This variable is included so that @-signs at the end of a pragma-containing comment can be ignored. In particular, it counts the number of characters read but not reported. These characters will be a number of @-signs followed by one more character (or -1, if at end-of-pragma). @-signs that immediately follow the first whitespace characters on a line are always "reported" (since these are actually reported as spaces anyway). In the steady state of this correlated reader, unreturnedChars is non-zero only when lastUnreturnedChar is not an @-sign.

unreturnedChars is not used (actually, is 0) when scanning Javadoc comments.


lastUnreturnedChar

private int lastUnreturnedChar
If there are unreturned characters, lastUnreturnedChar indicates the last of these characters.


allowSpecialSuffix

private final boolean allowSpecialSuffix
Indicates whether or not a sequence of consecutive special characters at the end of the comment are to be treated as white space. This is only done for the special character '@'.


prefixModeAtMark

private int prefixModeAtMark

unreturnedCharsAtMark

private int unreturnedCharsAtMark

lastUnreturnedCharAtMark

private int lastUnreturnedCharAtMark
Constructor Detail

JmlCorrelatedReader

protected JmlCorrelatedReader(CorrelatedReader child,
                              int commentKind)
Constructs a JmlCorrelatedReader with child as the underlying CorrelatedReader. After calling this constructor, the caller should no longer use child directly.

commentKind is EOL_COMMENT to indicate a slash-slash comment, C_COMMENT to indicate an ordinary slash-star comment, and JAVADOC_COMMENT to indicate that the portion to be read resides inside a (pair of tags in a) Javadoc comment.

Method Detail

read

public int read()
         throws java.io.IOException
Reads the next character from this input stream. Performs Unicode conversion and JML filtering. Requires that the stream is open.

Overrides:
read in class FilterCorrelatedReader
Returns:
A Unicode character, or -1.
Throws:
java.io.IOException

getLocation

public int getLocation()
Description copied from class: FilterCorrelatedReader
Returns the location of the last character read. If no character has been read yet, returns a whole-file location for this file.

Overrides:
getLocation in class FilterCorrelatedReader

mark

public void mark()
Description copied from class: FilterCorrelatedReader
See documentation in superclass.

Overrides:
mark in class FilterCorrelatedReader

reset

public void reset()
           throws java.io.IOException
Description copied from class: FilterCorrelatedReader
See documentation in superclass.

Overrides:
reset in class FilterCorrelatedReader
Throws:
java.io.IOException

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