escjava.parser
Class JmlCorrelatedReader

java.lang.Object
  javafe.util.CorrelatedReader
      javafe.util.FilterCorrelatedReader
          escjava.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