escjava.parser
Class EscPragmaLex

java.lang.Object
  javafe.parser.Token
      javafe.parser.Lex
          escjava.parser.EscPragmaLex

public final class EscPragmaLex

extends Lex

This lexer overrides Lex.scanJavaExtensions(int) to support "informal predicates". An informal predicate is an embedded comment.

 //@ requires (* this is an informal predicate *);
 //@ requires true &&(*soIsThis*)
 //@ ensures (((((* Here's one inside some parens *)))));
 

Informal predicates can even be more crazy with embedded comments. See the file ESCTools/Escjava/test/escjava/test/test70/C.java for examples.

Informal predicates are parsed as boolean literal expressions with an AST decoration of "informalPredicate". See EscPragmaParser.parsePrimaryExpression(Lex) and EscPragmaParser.informalPredicateDecoration for details.

Field Summary

Fields inherited from class javafe.parser.Lex

inPragma, javakeywords, keywords, lexicalPragmas, lookaheadq, m_in, m_nextchr, onlyjavakeywords, pragmaParser, savedState, text, textlen

Fields inherited from class javafe.parser.Token

auxVal, CLEAR, endingLoc, identifierVal, startingLoc, ttype

Constructor Summary

EscPragmaLex(PragmaParser pragmaParser, boolean isJava)

Method Summary

protected int

scanJavaExtensions(int nextchr) Scans a Java extension.

Methods inherited from class javafe.parser.Lex

addJavaKeywords, addJavaPunctuation, addKeyword, addPunctuation, append, close, getLexicalPragmas, getNextToken, lookahead, lookaheadToken, popLexicalPragma, replaceLookaheadToken, restart, zzz

Methods inherited from class javafe.parser.Token

clear, copyInto, ztoString, zzz

Methods inherited from class java.lang.Object

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

Constructor Detail

EscPragmaLex

public EscPragmaLex(PragmaParser pragmaParser,
                    boolean isJava)

Method Detail

scanJavaExtensions

protected int scanJavaExtensions(int nextchr)

Description copied from class: Lex

Scans a Java extension. If input doesn't match any Java extension, returns TagConstants.NULL. Assumes startingLoc already filled in, and assumes textlen is 0.

The routine may change the mark arbitrarily.

If a Java extension is matched, returns with m_nextchr holding the character just after the token scanned and m_in pointing to the character after that.

Overrides:

scanJavaExtensions in class Lex