    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.parser;
    004
    005    import escjava.Main;
    006    import escjava.ast.*;
    007    // This import is necessary to override javafe.ast.TagConstants.
    008    import escjava.ast.TagConstants;
    009    import escjava.ast.Modifiers;
    010    import escjava.AnnotationHandler;
    011
    012    import java.io.IOException;
    013
    014    import javafe.ast.*;
    015    import javafe.SrcTool;
    016    import javafe.parser.Lex;
    017    import javafe.parser.Parse;
    018    import javafe.parser.PragmaParser;
    019    import javafe.parser.Token;
    020    import javafe.util.Assert;
    021    import javafe.util.CorrelatedReader;
    022    import javafe.util.ErrorSet;
    023    import javafe.util.Info;
    024    import javafe.util.Location;
    025
    026    import java.util.ArrayList;
    027    import java.util.Vector;
    028    import java.util.LinkedList;
    029    import java.util.Iterator;
    030
    031    /**
    032     Grammar:
    033
    034     <pre>
    035     Pragma ::= LexicalPragma | ModifierPragma | TypeDeclElemPragma | StmtPragma
    036
    037     LexicalPragma ::= "nowarn" [ Idn [',' Idn]* ] [';']
    038
    039
    040     StmtPragma ::= SimpleStmtPragma [';']
    041     | ExprStmtPragma SpecExpr [';']
    042     | 'set' PrimaryExpr '=' SpecExpr [';']
    043
    044     SimpleStmtPragma ::= 'unreachable'
    045
    046     ExprStmtPragma ::= 'assume' | 'assume_redundantly'
    047     | 'assert' | 'assert_redundantly'
    048     | 'loop_inv' | 'loop_invariant' | 'loop_invariant_redundantly'
    049     | 'decreases' | 'decreases_redundantly'
    050     | 'loop_predicate'
    051     | 'maintaining' | 'maintaining_redundantly'
    052     | 'decreasing' | 'decreasing_redundantly'
    053
    054     TypeDeclElemPragma ::=
    055     ExprDeclPragma SpecExpr [';']
    056     | 'ghost' Modifiers Type VariableDeclarator [';']
    057     | 'still_deferred' Idn [',' Idn]* [';']
    058
    059     ExprDeclPragma ::= 'axiom' | 'invariant' | 'invariant_redundantly'
    060
    061
    062     ModifierPragma ::=
    063     [PrivacyPragma] [BehaviorPragma] SimpleModifierPragma
    064     [PrivacyPragma] [BehaviorPragma] NonSimpleModifierPragma
    065
    066     NonSimpleModifierPragma ::=
    067     | ['also'] ExprModifierPragma SpecExpr [';']
    068     | ['also'] VarExprModifierPragma '(' Type Idn ')' SpecExpr [';']
    069     | ['also'] 'monitored_by' SpecExpr [',' SpecExpr]* [';']
    070     | ['also'] ModifierPragma SpecDesignator [',' SpecDesignator]* [';']
    071
    072     PrivacyPragma ::= 'public' | 'private' | 'protected'
    073
    074     BehaviorPragma ::= 'behavior' | 'normal_behavior' | 'exceptional_behavior'
    075
    076     SimpleModifierPragma ::= 'uninitialized' | 'monitored'
    077     | 'non_null' | 'instance' | 'pure'
    078     | 'spec_public' | 'writable_deferred' | 'helper'
    079     | 'public' | 'private' | 'protected'
    080     | 'spec_protected' | 'model' | 'transient' | '\peer' | '\readonly' | '\rep'
    081     | 'may_be_null' | 'non_null_ref_by_default' | 'null_ref_by_default' | 'obs_pure'
    082     | 'code_java_math' | 'code_safe_math' | 'code_bigint_math'
    083     | 'spec_java_math' | 'spec_safe_math' | 'spec_bigint_math'
    084
    085     ExprModifierPragma ::= 'readable_if' | 'writable_if'
    086     | 'requires' | 'requires_redundantly' | 'also_requires' (if Main.allowAlsoRequires)
    087     | 'ensures' | 'ensures_redundantly' | 'also_ensures'
    088     | 'pre' | 'pre_redundantly' | 'post' | 'post_redundantly'
    089
    090     VarExprModifierPragma ::= 'exsures' | 'exsures_redundantly' | 'also_exsures"
    091     | 'signals' | 'signals_redundantly'
    092
    093     ModifierPragma ::= 'modifies' | 'modifies_redundantly' | 'also_modifies'
    094     | 'modifiable' | 'modifiable_redundantly'
    095     | 'assignable' | 'assignable_redundantly'
    096
    097
    098     DurationClause ::= DurationKeyword '\not_specified' ';'
    099     | DurationKeyword DurSpecExpr [ 'if' predicate ] ';'
    100
    101     DurSpecExpr ::= SpecExpr (of type long) OpWithLongResult DurSpecExpr
    102     | '\duration' '(' MethodInvOrConstructor ')' LongOp DurSpecExpr;
    103
    104     MethodInvOrConstructorOrNotSpecified ::= MethodInvOrConstructor | '\not_specified';
    105
    106     InvariantForExpr ::= '\invariant_for' '(' SpecExpr ')' ';'
    107
    108     SpaceExpr ::= '\space' '(' SpecExpr ')'
    109
    110     IsInitializedExpr ::= '\is_initialized' '(' Idn ')' ';'
    111
    112     InvariantFor ::= '\invariant_for' '(' SpecExpr ')' ';'
    113
    114     WorkingSpaceClause ::= WorkingSpaceKeyword '\not_specified' ';'
    115     | WorkingSpaceKeyword WorkingSpaceSpecExpr [ 'if' predicate ] ';'
    116
    117     WorkingSpaceSpecExpr ::= SpecExpr (of type int) OpWithIntResult WorkingSpaceSpecExpr
    118     | '\working_space' '(' MethodInvOrConstructor ')' IntOp WorkingSpaceSpecExpr
    119
    120     MethodInvOrConstructor ::= MethodInvocation | ConstructorInvocation
    121
    122     OpWithIntResult ::= STAR | '/' | '%' | PLUS | '-' | '&' | BITOR | '^'
    123
    124     WorkingSpaceKeyword ::= 'working_space' | 'working_space_redundantly'
    125
    126     DurationKeyword ::= 'duration' | 'duration_redundantly'
    127
    128     PrivateDataKeyword ::= '\private_data'
    129
    130     NotModifiedExpr ::= '\not_modified' '(' SpecDesignator [',' SpecDesignator]* ')' ';'
    131
    132     ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';'
    133
    134     FieldsOfExpr ::= '\fields_of' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';'
    135
    136     OtherExpr ::= '\other' [ StoreRefNameSuffix ] ';'
    137
    138     ReachExpr ::= '\reach' '(' SpecExpr [ ',' Idn [ ',' StoreRefExpr ] ] ')' ';'
    139
    140     StoreRefList ::= StoreRef [ ',' StoreRef ] ...
    141
    142     StoreRef ::= StoreRefExpr
    143     | FieldsOfExpr
    144     | InformalDescription
    145     | StoreRefKeyword
    146
    147     StoreRefExpr ::= StoreRefName [ StoreRefNameSuffix ] ...
    148
    149     StoreRefName ::= Idn | 'super' | 'this'
    150
    151     StoreRefNameSuffix ::= '.' Idn | '.' 'this' | '[' SpecArrayRefExpr ']'
    152
    153     SpecArrayRefExpr ::= SpecExpr | SpecExpr '..' SpecExpr | '*'
    154
    155     StoreRefKeyword ::= '\nothing' | '\everything' | '\not_specified' | '\private_data'
    156
    157
    158     ConditionalStoreRefList ::= ConditionalStoreRef [ ',' ConditionalStoreRef ] ...
    159
    160     ConditionalStoreRef ::= StoreRef [ 'if' Predicate ]
    161
    162
    163     InformalDescription ::= '(*' NonStarClose [ NonStarClose ] ... '*)'
    164
    165     NonStarClose ::= NonStar | StarsNonClose
    166
    167     StarsNonClose ::= '*' [ '*' ] ... NonClose
    168
    169     NonClose ::= any character except ')'
    170
    171     </pre>
    172
    173     The grammar of SpecExpr is:
    174
    175     <pre>
    176     SpecExpr:
    177     Name
    178     | \result
    179     | \lockset
    180     | this
    181     | Literal
    182     | SpecExpr '.' Idn
    183     | SpecExpr '[' SpecExpr ']'
    184     | UnOp SpecExpr
    185     | '(' Type ')' SpecExpr
    186     | SpecExpr BinOp SpecExpr
    187     | SpecExpr 'instanceof' Type
    188     | Function '(' [ SpecExpr [ ',' SpecExpr ]* ] ')'
    189     | '\type' '(' Type ')'
    190     | SpecExpr '?' SpecExpr ':' SpecExpr
    191     | '(' {'\forall'|'\exists'} Type Idn [',' Idn]* ';' [[SpecExpr] ';'] SpecExpr ')'
    192     | '(' {'\lblpos'|'\lblneg'} Idn SpecExpr ')'
    193     | '(' SpecExpr ')'
    194     | Name '.' this                         [1.1]
    195     | Name ([])* '.' class                  [1.1]
    196     | JmlSpecExpr
    197
    198     JmlSpecExpr ::= '\nothing' | '\everything' | '\not_specified'
    199
    200     Function ::= '\fresh' | '\nonnullelements' | '\elemtype' | '\max' | '\old'
    201     | '\typeof' | '\not_modified' | '\nowarn' | '\nowarn_op' | '\warn' | '\warn_op'
    202     | '\java_math' | '\safe_math' | \bigint_math
    203
    204     UnOp ::= '+' | '-' | '!' | '~'
    205
    206     BinOp ::= '+' | '-' | '*' | '/' | '%' | '<<' | '>>' | '>>>'
    207     | '<' | '<=' | '==' | '!=' | '>=' | '>'
    208     | '&' | '|' | '^' | '&&' | '||'
    209     </pre>
    210
    211     * <p> Also, the grammar for Type is extended (recursively) with the
    212     * new base type 'TYPE'.
    213     *
    214     * <p> Expressions in redundant specifications (e.g.,
    215     * requires_redundantly ...) are only parsed if
    216     * <code>Main.checkRedundantSpecs</code> is true.
    217     *
    218     * @note 'SC' == Statically Checkable or otherwise useful 'HPT' == Handle at
    219     * Parse-time 'AAST' == 'Augments Abstract Symbol Tree' Final 0-5 indicates
    220     * difficulty of implementation; 0 being easiest.  All estimates and
    221     * implementation/design guesses were made by Joe Kiniry on 29 April 2003.
    222     *
    223     * @note kiniry 24 Jan 2003 - All rules named Jml* added by
    224     * kiniry@cs.kun.nl starting on 24 Jan 2003.
    225     *
    226     * @todo kiniry 24 Jan 2003 - Make semicolon at end of 'nowarn' lexical
    227     * pragma non-optional.  This requires updating spec files &c.
    228     *
    229     * @todo kiniry 24 Jan 2003 - Permit splitting syntactic constructs
    230     * across multiple @code{//@@} comments.
    231     *
    232     * @todo kiniry 19 May 2003 - Need to add grammar expressions above
    233     * for constraints.
    234     *
    235     * @todo kiniry 9 July 2003 - Support for \not_specified is scattered all over the
    236     * code right now---perhaps we can refactor and clean up?  It is sometimes parsed
    237     * and discarded, sometimes recognized and ignored, etc.
    238     *
    239     * @see escjava.Options#checkRedundantSpecs
    240     */
    241
    242    public class EscPragmaParser extends Parse
    243      implements PragmaParser
    244    {
    245      private static final boolean DEBUG = false;
    246
    247      /**
    248       * The informal-predicate decoration is associated with a true-valued boolean
    249       * literal expression, if the concrete syntax of this expression was an informal
    250       * comment.  The value associated with the decoration is the string of the
    251       * informal predicate (i.e., the comment itself).
    252       */
    253      public static final ASTDecoration informalPredicateDecoration = new ASTDecoration(
    254          "informalPredicate");
    255
    256      /**
    257       * The lexer associated with this pragma parser from which we will read tokens.
    258       */
    259      private/*@ non_null @*/EscPragmaLex scanner;
    260
    261      public int NOTHING_ELSE_TO_PROCESS = -2;
    262
    263      public int NEXT_TOKEN_STARTS_NEW_PRAGMA = -1;
    264
    265      /**
    266       * The value NOTHING_ELSE_TO_PROCESS means there is nothing else to process.  The
    267       * value NEXT_TOKEN_STARTS_NEW_PRAGMA means there is something to process and the
    268       * next thing to read begins a new pragma (or ends the pragma-containing
    269       * comment).  The other values indicate that the pragma parser is in the middle
    270       * of parsing some pragma, and is expected to continue this parsing next time it
    271       * gets control.
    272       */
    273      //@ spec_public
    274      private int inProcessTag;
    275
    276      /*@ invariant inProcessTag == NOTHING_ELSE_TO_PROCESS ||
    277       @           inProcessTag == NEXT_TOKEN_STARTS_NEW_PRAGMA ||
    278       @           inProcessTag == TagConstants.STILL_DEFERRED ||
    279       @           inProcessTag == TagConstants.MONITORED_BY ||
    280       @           inProcessTag == TagConstants.MODIFIES ||
    281       @           inProcessTag == TagConstants.ALSO_MODIFIES ||
    282       @           inProcessTag == TagConstants.MODIFIABLE ||
    283       @           inProcessTag == TagConstants.ASSIGNABLE ||
    284       @           inProcessTag == TagConstants.LOOP_PREDICATE ||
    285       @           inProcessTag == TagConstants.ALSO;
    286       @*/
    287
    288      private int inProcessLoc;
    289
    290      private CorrelatedReader pendingJavadocComment;
    291
    292      /**
    293       * Maximum # of levels of nesting of annotation comments allowed.  0 == no
    294       * nesting of annotation comments allowed.
    295       *
    296       * <p> If you change this, change the error message in EscPragmaParser(int) below
    297       * as well.
    298       */
    299      static final int maxAnnotationNestingLevel = 1;
    300
    301      /**
    302       * Constructs a new pragma parser with zero nesting level.
    303       *
    304       * @see #EscPragmaParser(int)
    305       */
    306      public EscPragmaParser() {
    307        this(0);
    308      }
    309
    310      /**
    311       * Constructs a new prama parser at the indicated nesting level.
    312       *
    313       * @param level the nesting level of this instance.
    314       */
    315      //@ requires level >= 0;
    316      public EscPragmaParser(int level) {
    317        PragmaParser pp;
    318        if (level < maxAnnotationNestingLevel)
    319          pp = new EscPragmaParser(level + 1);
    320        else
    321          pp = new ErrorPragmaParser("Annotation comments may be nested "
    322              + "at most 1 time");
    323
    324        scanner = new EscPragmaLex(pp, true);
    325        scanner.addPunctuation("==>", TagConstants.IMPLIES);
    326        scanner.addPunctuation("<==", TagConstants.EXPLIES);
    327        scanner.addPunctuation("<==>", TagConstants.IFF);
    328        scanner.addPunctuation("<=!=>", TagConstants.NIFF);
    329        scanner.addPunctuation("<:", TagConstants.SUBTYPE);
    330        scanner.addPunctuation("..", TagConstants.DOTDOT);
    331        scanner.addPunctuation("<-", TagConstants.LEFTARROW);
    332        scanner.addPunctuation("->", TagConstants.RIGHTARROW);
    333        scanner.addPunctuation("{|", TagConstants.OPENPRAGMA);
    334        scanner.addPunctuation("|}", TagConstants.CLOSEPRAGMA);
    335        addOperator(TagConstants.IMPLIES, 76, false);
    336        addOperator(TagConstants.EXPLIES, 76, true);
    337        addOperator(TagConstants.IFF, 73, true);
    338        addOperator(TagConstants.NIFF, 73, true);
    339        addOperator(TagConstants.SUBTYPE, 140, true);
    340        addOperator(TagConstants.DOTDOT, 1, true);
    341        scanner.addKeyword("\\real", TagConstants.REAL);
    342        scanner.addKeyword("\\bigint", TagConstants.BIGINT);
    343        scanner.addKeyword("\\result", TagConstants.RES);
    344        scanner.addKeyword("\\lockset", TagConstants.LS);
    345        scanner.addKeyword("\\TYPE", TagConstants.TYPETYPE);
    346        scanner.addKeyword("\\everything", TagConstants.EVERYTHING);
    347        scanner.addKeyword("\\nothing", TagConstants.NOTHING);
    348        scanner.addKeyword("\\fields_of", TagConstants.FIELDS_OF);
    349        //scanner.addKeyword("\\reach",TagConstants.REACH);
    350        scanner.addKeyword("\\not_specified", TagConstants.NOT_SPECIFIED);
    351        scanner.addKeyword("\\such_that", TagConstants.SUCH_THAT);
    352        inProcessTag = NOTHING_ELSE_TO_PROCESS;
    353      }
    354
    355      /**
    356       * @param tag the comment tag character to check.
    357       * @return true iff tag is an '@' or an '*' character.
    358       */
    359      public boolean checkTag(int tag) {
    360        if (Main.options().parsePlus && tag == '+') return true;
    361        return tag == '@' || tag == '*' || tag == '-';
    362      }
    363
    364      /**
    365       * Restart a pragma parser on a new input stream.  If <code>this</code> is
    366       * already opened on another {@link CorrelatedReader}, close the old reader.
    367       *
    368       * @param in the reader from which to read.
    369       * @param eolComment a flag that indicates we are parsing an EOL
    370       * comment (a comment that starts with "//").
    371       */
    372      public void restart(/*@ non_null @*/CorrelatedReader in, boolean eolComment) {
    373        try {
    374          int c = in.read();
    375          //System.out.println("restart: c = '"+(char)c+"'");
    376
    377          if (Main.options().parsePlus && c == '+') {
    378            c = in.read();
    379            if (c != '@') {
    380              //Not an annotation or doc comment after all - skip to end
    381              while (in.read() != -1) {
    382              }
    383              return;
    384            }
    385          }
    386
    387          if (c == '-') {
    388            c = in.read();
    389            if (c != '@') {
    390              //Not an annotation or doc comment after all - skip to end
    391              while (in.read() != -1) {
    392              }
    393              return;
    394            }
    395          }
    396
    397          switch (c) {
    398            case '@':
    399              /* Normal escjava annotation: */
    400
    401              eatAts(in);
    402              eatWizardComment(in);
    403              in = new JmlCorrelatedReader(in,
    404                  eolComment ? JmlCorrelatedReader.EOL_COMMENT
    405                      : JmlCorrelatedReader.C_COMMENT);
    406              /*
    407               * At this point, <code>in</code> has been
    408               * trimmed/replaced as needed to represent the
    409               * annotation part of the comment (if any -- it may be
    410               * empty).
    411               */
    412              scanner.restart(in);
    413              inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    414              break;
    415
    416            case '*':
    417              if (eolComment) {
    418                // This is not a Javadoc comment, so ignore
    419                inProcessTag = NOTHING_ELSE_TO_PROCESS;
    420              } else {
    421                // Javadoc comment -- look for <esc> ... </esc> inside
    422
    423                if (pendingJavadocComment != null) {
    424                  pendingJavadocComment.close();
    425                }
    426                pendingJavadocComment = in;
    427                processJavadocComment();
    428              }
    429              break;
    430
    431            default:
    432              fail(in.getLocation(), "Bad starting character on comment:" + c + " "
    433                  + (char)c);
    434          }
    435        } catch (IOException e) {
    436          ErrorSet.fatal(in.getLocation(), e.toString());
    437        }
    438      }
    439
    440      /**
    441       * Parse embedded <esc&gr; ... </esc> in Javadoc comments.
    442       *
    443       * @return a flag indicating if an embedded comment was recognized.
    444       * @exception IOException if something goes wrong during reading.
    445       */
    446      private boolean processJavadocComment() throws IOException {
    447        if (pendingJavadocComment == null) { return false; }
    448        int startLoc = scanForOpeningTag(pendingJavadocComment); // sets the value of endTag
    449        if (startLoc == Location.NULL) {
    450          pendingJavadocComment = null;
    451          inProcessTag = NOTHING_ELSE_TO_PROCESS;
    452          return false;
    453        }
    454
    455        // Mark the current character, the first character inside the enclosed
    456        // pragma:
    457        pendingJavadocComment.mark();
    458
    459        if (scanFor(pendingJavadocComment, endTag) != Location.NULL) {
    460          // Restrict "pendingJavadocComment" to just before endEnclosedPragma
    461          CorrelatedReader nu = pendingJavadocComment.createReaderFromMark(endTag
    462              .length());
    463          nu = new JmlCorrelatedReader(nu, JmlCorrelatedReader.JAVADOC_COMMENT);
    464          scanner.restart(nu);
    465          inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    466          return true;
    467        } else {
    468          ErrorSet.error(startLoc, "Pragma in javadoc comment is not correctly "
    469              + "terminated (missing " + endTag + ")");
    470          pendingJavadocComment = null;
    471          inProcessTag = NOTHING_ELSE_TO_PROCESS;
    472          return false;
    473        }
    474      } //@ nowarn Exception; // IndexOutOfBoundsException
    475
    476      /** Eats any extra @ symbols.
    477       */
    478      private void eatAts(/*@ non_null @*/CorrelatedReader in) throws IOException {
    479        do {
    480          in.mark();
    481        } while (in.read() == '@');
    482        in.reset();
    483      }
    484
    485      /**
    486       * Eat any wizard inserted comment at the start of an escjava annotation.
    487       *
    488       * <p> May side-effect the mark of <code>in</code>.
    489       *
    490       * <p> Eats "([^)]*)", if present, from <code>in</code>.
    491       *
    492       * @param in the stream from which to read.
    493       */
    494      private void eatWizardComment(/*@ non_null @*/CorrelatedReader in)
    495          throws IOException {
    496        in.mark();
    497        int cc = in.read();
    498        if (cc != '(') {
    499          in.reset();
    500          return;
    501        }
    502
    503        // Handle (...) comment:
    504        // Skip up to and including the next close paren:
    505        do {
    506          cc = in.read();
    507          if (cc == -1 || cc == '\n') {
    508            // At end-of-comment or end-of-line but still no close paren:
    509            ErrorSet.error(in.getLocation(),
    510                "Badly formed wizard comment (missing `)')");
    511            return;
    512          }
    513        } while (cc != ')');
    514      }
    515
    516      /**
    517       * Scans input stream for a string matching the parameter
    518       * <code>match</code>. Only works if the first character is not repeated in the
    519       * string.
    520       *
    521       * <p> If present, the location of the match is returned.  If not present,
    522       * <code>Location.NULL</code> is returned.
    523       *
    524       * <p> Requires that <code>in</code> is not closed.
    525       *
    526       * @param in the stream from which to read.
    527       * @param match the string to match against the input stream.
    528       * @return the location of the match, or
    529       * <code>Location.NULL</code> if there is no match.
    530       */
    531      private int scanFor(/*@ non_null @*/CorrelatedReader in,
    532      /*@ non_null @*/String match) throws IOException {
    533
    534        int start = match.charAt(0);
    535        int c = in.read();
    536
    537        mainLoop: while (true) {
    538          while (c != -1 && c != start)
    539            c = in.read();
    540
    541          if (c == -1) return Location.NULL;
    542          int startLoc = in.getLocation();
    543          Assert.notFalse(startLoc != Location.NULL);
    544
    545          // Have a match for the first character in the string
    546
    547          for (int i = 1; i < match.length(); i++) {
    548            c = in.read();
    549            if (c != match.charAt(i)) continue mainLoop;
    550          }
    551
    552          // Have a match
    553          return startLoc;
    554        }
    555      }
    556
    557      private String endTag;
    558
    559      /**
    560       * Scans for one of <esc> <jml> <ESC> <JML>.  This is
    561       * hard-coded to simplify the code.  Also sets the variable endTag to the
    562       * corresponding tag that closes the opening tag that was found (null if none
    563       * was found).
    564       */
    565      //@ modifies endTag;
    566      private int scanForOpeningTag(/*@ non_null @*/CorrelatedReader in)
    567          throws IOException {
    568        endTag = null;
    569
    570        int start = '<'; // first character of all tags
    571        int c = in.read();
    572        while (c != -1) {
    573
    574          while (c != -1 && c != start)
    575            c = in.read();
    576
    577          if (c == -1) return Location.NULL;
    578          int startLoc = in.getLocation();
    579          Assert.notFalse(startLoc != Location.NULL);
    580
    581          // Have a match for the first character in the string
    582
    583          c = in.read();
    584          if (c == -1) return Location.NULL;
    585          if (c == 'e') {
    586            c = in.read();
    587            if (c != 's') continue;
    588            c = in.read();
    589            if (c != 'c') continue;
    590            c = in.read();
    591            if (c != '>') continue;
    592            endTag = "</esc>";
    593          } else if (c == 'E') {
    594            c = in.read();
    595            if (c != 'S') continue;
    596            c = in.read();
    597            if (c != 'C') continue;
    598            c = in.read();
    599            if (c != '>') continue;
    600            endTag = "</ESC>";
    601          } else if (c == 'j') { // && Main.options().parsePlus) {
    602            c = in.read();
    603            if (c != 'm') continue;
    604            c = in.read();
    605            if (c != 'l') continue;
    606            c = in.read();
    607            if (c != '>') continue;
    608            endTag = "</jml>";
    609          } else if (c == 'J') { // && Main.options().parsePlus) {
    610            c = in.read();
    611            if (c != 'M') continue;
    612            c = in.read();
    613            if (c != 'L') continue;
    614            c = in.read();
    615            if (c != '>') continue;
    616            endTag = "</JML>";
    617          } else {
    618            continue;
    619          }
    620          // Have a match
    621          return startLoc;
    622        }
    623        return Location.NULL;
    624      }
    625
    626      /**
    627       * Closes this pragma parser including its scanner and pending Javadoc comment.
    628       */
    629      public void close() {
    630        scanner.close();
    631        if (pendingJavadocComment != null) {
    632          pendingJavadocComment.close();
    633          pendingJavadocComment = null;
    634        }
    635      }
    636
    637      //private FieldDecl previousDecl;
    638
    639      /*
    640       A bit of refactoring of the old Esc/java design.  This method returns
    641       a pragma and is called repeatedly to get a series of pragmas until there
    642       are no more (prior to a non-pragma token).  Sometimes a given
    643       grammatical context produces more than one pragma.  An example is a
    644       ghost declaration with more than one identifier.  The previous design
    645       required the EscPragmaParser object to keep enough context to resume
    646       the parsing in the middle, via continuePragma().
    647
    648       I've improved (I hope) on this by instituting a queue in this object.
    649       Pragmas are returned from the queue if there are any, until the queue
    650       is empty.  If the queue is empty, then the regular parsing occurs.
    651       If the input naturally produces a bunch of pragmas, then all but the
    652       first is put in the queue, and the first one is returned.  This way
    653       we can consistently parse either (a) simple keywords, (b) up to a
    654       semicolon, or (c) up to the EOF marking the end of the pragma.
    655
    656       This will simplify the handling of multiple annotations in one pragma
    657       comment and will simplify the logic overall as well.
    658       -- DRCok 7/23/2003
    659       */
    660
    661      private java.util.LinkedList pragmaQueue = new java.util.LinkedList();
    662
    663      // element type is SavedPragma
    664      protected class SavedPragma {
    665
    666        public int loc;
    667
    668        public int ttype;
    669
    670        public Object auxval;
    671
    672        public SavedPragma(int l, int t, Object o) {
    673          loc = l;
    674          ttype = t;
    675          auxval = o;
    676        }
    677      }
    678
    679      public void savePragma(int l, int t, Object o) {
    680        pragmaQueue.addLast(new SavedPragma(l, t, o));
    681      }
    682
    683      public void savePragma(Token d) {
    684        pragmaQueue.addLast(new SavedPragma(d.startingLoc, d.ttype, d.auxVal));
    685      }
    686
    687      public boolean getPragma(Token dst) {
    688        if (pragmaQueue.isEmpty()) return false;
    689        SavedPragma p = (SavedPragma)pragmaQueue.removeFirst();
    690        dst.startingLoc = p.loc;
    691        dst.ttype = p.ttype;
    692        dst.auxVal = p.auxval;
    693        return true;
    694      }
    695
    696      ModifierPragma savedGhostModelPragma = null;
    697
    698      /**
    699       * Parse the next pragma, putting information about it in the provided token
    700       * <code>dst</code>, and return a flag indicating if there are further pragmas to
    701       * be parsed.
    702       *
    703       *
    704       * Note: All worrying about 'also' is now done during the desugaring of specs.
    705       * JML style of using also is preferred.
    706       *
    707       * @param dst the token in which to store information about the current pragma.
    708       * @return a flag indicating if further pragmas need to be parsed.
    709       * @see Lex
    710       */
    711      public boolean getNextPragma(/*@ non_null @*/Token dst) {
    712        try {
    713          if (getPragma(dst)) return true;
    714          boolean b;
    715          b = getNextPragmaHelper(dst);
    716          if (!b) return b;
    717          if (dst.ttype == TagConstants.NULL) return getPragma(dst);
    718          return true;
    719        } finally {
    720          //System.out.println("GNP " + TagConstants.toString(dst.ttype) + " " + dst.auxVal);
    721        }
    722      }
    723
    724      public boolean getNextPragmaHelper(/*@ non_null @*/Token dst) {
    725        //  System.out.println("CALLING HELPER " + TagConstants.toString(dst.ttype));
    726        try {
    727          if (inProcessTag == NOTHING_ELSE_TO_PROCESS) {
    728            if (DEBUG) Info.out("getNextPragma: Nothing else to process.");
    729            return false;
    730          }
    731
    732          // See if we need to continue a previous pragma, for example
    733          // "monitored_by", which can take multiple SpecExprs
    734          if (inProcessTag != NEXT_TOKEN_STARTS_NEW_PRAGMA) {
    735            continuePragma(dst);
    736            return true;
    737          }
    738
    739          // FIXME -- explain this - what circumstances need it?
    740          // Eventually the scanner comes to an EOF as the next character (the one the lexer is
    741          // looking at.  Then we proceed into this block for clean up.
    742          if (scanner.ttype == TagConstants.EOF) {
    743            if (savedGhostModelPragma != null) {
    744              // Came to the end of an annotation without finding a declaration after having
    745              // seen a ghost or model keyword.
    746              ErrorSet.error(savedGhostModelPragma.getStartLoc(),
    747                  "Expected a declaration within the annotation following the "
    748                      + TagConstants.toString(savedGhostModelPragma.getTag())
    749                      + " keyword");
    750              savedGhostModelPragma = null;
    751            }
    752            LexicalPragma PP = scanner.popLexicalPragma();
    753            if (PP != null) {
    754              // FIXME - check if this actually ever occurs - perhaps it was a case without a terminating semicolon
    755              dst.ttype = TagConstants.LEXICALPRAGMA;
    756              dst.auxVal = PP;
    757              if (DEBUG)
    758                  Info.out("getNextPragma: parsed final lexical pragma " + PP
    759                      + " at EOF.");
    760              return true;
    761            }
    762
    763            if (pendingJavadocComment != null) {
    764              // In this case, we were processing an annotation embedded in a
    765              // javadoc comment.  So we go back to process more of the
    766              // javadoc comment.
    767              scanner.close();
    768              if (!processJavadocComment()) {
    769                close();
    770                return false;
    771              }
    772              if (DEBUG)
    773                  Info.out("getNextPragma: processed javadoc comment at EOF.");
    774            } else {
    775              close();
    776              if (DEBUG)
    777                  Info.out("getNextPragma: hit EOF, so finishing pragma parsing.");
    778              return false;
    779            }
    780          }
    781          //@ assume scanner.m_in != null;  // TBW: is this right??  --KRML
    782          dst.ttype = TagConstants.NULL;
    783          dst.auxVal = null;
    784
    785          // FIXME - not everything allows modifiers
    786          // These are Java modifiers that are
    787          // parsed within an annotation, up until a non-modifier
    788          // is encountered or the end of the annotation.
    789          parseJavaModifiers(); // adds to the 'modifiers' field
    790
    791          // Start a new pragma
    792          // Need a better explanation - FIXME
    793          int loc = scanner.startingLoc;
    794          if (Main.options().parsePlus &&
    795          // Check for a closing + as in @+*/ - but might it be confused with a //+@ .... +  FIXME!
    796              scanner.ttype == TagConstants.ADD
    797              && scanner.lookahead(1) == TagConstants.EOF) { return false; }
    798
    799          int tag = scanner.ttype;
    800          Identifier kw = null;
    801          if (tag == TagConstants.IDENT) {
    802            kw = scanner.identifierVal;
    803            // Looks up JML keywords
    804            tag = TagConstants.fromIdentifier(kw);
    805            // Note: if we are parsing a ghost or model declaration
    806            // then we have already parsed all modifiers and
    807            // pragma modifiers and we start getNextPragma looking
    808            // at the type name that begins the actual field or
    809            // model declaration - then the IDENT is not a
    810            // may or may not be a keyword, but is the beginning
    811            // of the type
    812            if (tag != TagConstants.NULL) scanner.getNextToken(); // advance the scanner
    813            // For an IDENT that is not a JML keyword, the tag is
    814            // NULL and the switch statment below falls into the default
    815            // case - all pragmas begin with a keyword, so this must be
    816            // the start of a declaration of some sort.
    817          } else if (tag == TagConstants.MODIFIERPRAGMA) {
    818            // This can happen if there is an embedded annotation within
    819            // an annotation, such as
    820            //      //@ ghost public /*@ non_null */ Object o;
    821            // We'll just copy the pragma into the output and return.
    822            scanner.copyInto(dst);
    823            scanner.getNextToken();
    824            return true;
    825          }
    826          // Note: If the tag is not obtained from the identifier (e.g. if it
    827          // is also a Java keyword, such as assert) and is not already a
    828          // MODIFIERPRAGMA, then the scanner is
    829          // not advanced here and will need to be in the appropriate case
    830          // within the switch statement.
    831
    832          boolean semicolonExpected = false;
    833
    834          if (DEBUG) Info.out("next tag is: " + TagConstants.toString(tag));
    835
    836          switch (tag) {
    837            case TagConstants.CODE_CONTRACT:
    838            case TagConstants.BEHAVIOR:
    839            case TagConstants.EXCEPTIONAL_BEHAVIOR:
    840            case TagConstants.NORMAL_BEHAVIOR:
    841            case TagConstants.EXAMPLE:
    842            case TagConstants.NORMAL_EXAMPLE:
    843            case TagConstants.EXCEPTIONAL_EXAMPLE:
    844              dst.ttype = TagConstants.MODIFIERPRAGMA;
    845              dst.auxVal = SimpleModifierPragma.make(tag, loc);
    846              // We need to capture the modifiers ??? FIXME
    847              modifiers = Modifiers.NONE;
    848              break;
    849
    850            case TagConstants.FOR_EXAMPLE:
    851            case TagConstants.IMPLIES_THAT:
    852            case TagConstants.SUBCLASSING_CONTRACT:
    853            case TagConstants.ALSO:
    854              checkNoModifiers(tag, loc);
    855              // SUPPORT COMPLETE (cok/kiniry)
    856              // All desugaring of method specifications
    857              // is now performed in the desugaring
    858              // step in AnnotationHandler.
    859              dst.ttype = TagConstants.MODIFIERPRAGMA;
    860              dst.auxVal = SimpleModifierPragma.make(tag, loc);
    861              break;
    862
    863            case TagConstants.NOWARN:
    864              checkNoModifiers(tag, loc);
    865              dst.ttype = TagConstants.LEXICALPRAGMA;
    866              seqIdentifier.push();
    867              if (scanner.ttype == TagConstants.IDENT) {
    868                semicolonExpected = true;
    869                while (true) {
    870                  seqIdentifier.addElement(parseIdentifier(scanner));
    871                  if (scanner.ttype != TagConstants.COMMA) break;
    872                  scanner.getNextToken(); // Discard COMMA
    873                }
    874              } else if (scanner.ttype == TagConstants.EOF) {
    875                semicolonExpected = false;
    876              } else if (scanner.ttype == TagConstants.SEMICOLON) {
    877                semicolonExpected = true;
    878              } else {
    879                ErrorSet.error(loc, "Syntax error in nowarn pragma");
    880                eatThroughSemiColon();
    881                inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    882                semicolonExpected = false;
    883                break;
    884              }
    885              IdentifierVec checks = IdentifierVec
    886                  .popFromStackVector(seqIdentifier);
    887              dst.auxVal = NowarnPragma.make(checks, loc);
    888              break;
    889
    890            case TagConstants.ALSO_MODIFIES:
    891              tag = TagConstants.MODIFIES;
    892              ErrorSet.error(loc,
    893                             "Original ESC/Java keywords beginning with also_ are " +
    894                             "obsolete; they have been replaced with the " +
    895                             "corresponding JML keywords and the use of 'also' - " +
    896                             "note that the semantics has also changed.");
    897            // fall through
    898            case TagConstants.ASSIGNABLE: // SUPPORT COMPLETE (kiniry)
    899            case TagConstants.ASSIGNABLE_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    900            case TagConstants.MODIFIABLE: // SUPPORT COMPLETE (kiniry)
    901            case TagConstants.MODIFIABLE_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    902            case TagConstants.MODIFIES_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    903            case TagConstants.MODIFIES:
    904            {
    905              checkNoModifiers(tag, loc);
    906              ModifiesGroupPragma group = ModifiesGroupPragma.make(tag, loc);
    907              if (TagConstants.isRedundant(tag)) group.setRedundant(true);
    908              do {
    909                Expr e = parseStoreRef(scanner);
    910                // deal with optional conditional ('if' <predicate>)
    911                int t = scanner.ttype;
    912                if (t == TagConstants.IF) {
    913                  ErrorSet.caution(scanner.startingLoc,
    914                      "Conditional assignable clauses are"
    915                          + " no longer supported and are ignored");
    916                  scanner.getNextToken();
    917                  parseExpression(scanner);
    918                }
    919                // A CondExprModifierPragma is still used
    920                // even though we no longer have conditional
    921                // assignable clauses.  The cond part is always null
    922                if (e != null) {
    923                  CondExprModifierPragma pragma = CondExprModifierPragma.make(
    924                      TagConstants.unRedundant(tag), e, e.getStartLoc(), null);
    925                  if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    926                  group.addElement(pragma);
    927                }
    928                if (scanner.ttype != TagConstants.COMMA) break;
    929                scanner.getNextToken(); // skip comma
    930              } while (true);
    931              semicolonExpected = true;
    932              if (DEBUG)
    933                  Info.out("getNextPragma: parsed a frame axiom: "
    934                      + dst.ztoString());
    935              dst.startingLoc = loc;
    936              dst.ttype = TagConstants.MODIFIERPRAGMA;
    937              dst.auxVal = group;
    938              break;
    939            }
    940
    941            case TagConstants.STILL_DEFERRED:
    942            {
    943              checkNoModifiers(tag, loc);
    944              inProcessTag = tag;
    945              inProcessLoc = loc;
    946              continuePragma(dst);
    947              if (DEBUG)
    948                  Info.out("getNextPragma: parsed a frame axiom: "
    949                      + dst.ztoString());
    950              return true;
    951            }
    952
    953            case TagConstants.MONITORED_BY:
    954            {
    955              checkNoModifiers(tag, loc);
    956              semicolonExpected = true;
    957              int t = scanner.lookahead(0);
    958              Expr e = parseExpression(scanner);
    959              dst.auxVal = ExprModifierPragma.make(tag, e, loc);
    960              dst.ttype = TagConstants.MODIFIERPRAGMA;
    961              if (scanner.ttype == TagConstants.COMMA) {
    962                savePragma(dst);
    963                while (scanner.ttype == TagConstants.COMMA) {
    964                  scanner.getNextToken(); // skip comma
    965                  e = parseExpression(scanner);
    966                  savePragma(loc, TagConstants.MODIFIERPRAGMA, ExprModifierPragma
    967                      .make(tag, e, loc));
    968                }
    969                dst.ttype = TagConstants.NULL;
    970              }
    971              break;
    972            }
    973
    974            case TagConstants.WRITABLE:
    975            case TagConstants.READABLE:
    976            {
    977              checkNoModifiers(tag, loc);
    978              do {
    979                Expr e = parseStoreRef(scanner);
    980                // deal with optional conditional ('if' <predicate>)
    981                int t = scanner.ttype;
    982                Expr cond = null;
    983                if (t != TagConstants.IF) {
    984                  ErrorSet.error(scanner.startingLoc, "A "
    985                      + TagConstants.toString(tag)
    986                      + " clause requires an if predicate");
    987                  e = null;
    988                } else {
    989                  scanner.getNextToken();
    990                  cond = parseExpression(scanner);
    991                }
    992                if (e != null) {
    993                  NamedExprDeclPragma pragma = NamedExprDeclPragma.make(
    994                      TagConstants.unRedundant(tag), cond, e, modifiers, loc);
    995                  if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    996                  savePragma(loc, TagConstants.TYPEDECLELEMPRAGMA, pragma);
    997                }
    998                if (scanner.ttype != TagConstants.COMMA) break;
    999                scanner.getNextToken(); // skip comma
    1000              } while (true);
    1001              semicolonExpected = true;
    1002              break;
    1003            }
    1004
    1005            case TagConstants.MONITORS_FOR:
    1006            {
    1007              //checkNoModifiers(tag,loc);
    1008              int locId = scanner.startingLoc;
    1009              Identifier target = parseIdentifier(scanner);
    1010              if (scanner.ttype != TagConstants.ASSIGN
    1011                  && scanner.ttype != TagConstants.LEFTARROW) {
    1012                ErrorSet.error(scanner.startingLoc,
    1013                    "Expected a = or <- character in a monitors_for clause");
    1014                eatThroughSemiColon();
    1015                return getNextPragmaHelper(dst);
    1016              } else {
    1017                scanner.getNextToken(); // eat =
    1018                Expr e = parseExpression(scanner);
    1019                savePragma(loc, TagConstants.TYPEDECLELEMPRAGMA, IdExprDeclPragma
    1020                    .make(tag, target, e, modifiers, loc, locId));
    1021                while (scanner.ttype == TagConstants.COMMA) {
    1022                  scanner.getNextToken(); // skip comma
    1023                  e = parseExpression(scanner);
    1024                  savePragma(loc, TagConstants.TYPEDECLELEMPRAGMA, IdExprDeclPragma
    1025                      .make(tag, target, e, modifiers, loc, locId));
    1026                }
    1027                dst.ttype = TagConstants.NULL;
    1028                semicolonExpected = true;
    1029              }
    1030              break;
    1031            }
    1032
    1033            case TagConstants.DEPENDS:
    1034            case TagConstants.DEPENDS_REDUNDANTLY:
    1035            {
    1036              ErrorSet.caution(loc,
    1037                               "The depends clause is obsolete; it has been " +
    1038                               "replaced by the in and maps clauses");
    1039              int tempTag = TagConstants.unRedundant(tag);
    1040              dst.ttype = TagConstants.TYPEDECLELEMPRAGMA;
    1041              // FIXME - should this be a primary expression
    1042              // or maybe even a simple name?
    1043              Expr target = parseExpression(scanner);
    1044              int locOp = scanner.startingLoc;
    1045              expect(scanner, TagConstants.LEFTARROW);
    1046              Vector list = new Vector();
    1047              while (true) {
    1048                Expr value = parseExpression(scanner);
    1049                list.add(value);
    1050                if (scanner.ttype != TagConstants.COMMA) break;
    1051                scanner.getNextToken();
    1052              }
    1053              eatThroughSemiColon();
    1054              return getNextPragmaHelper(dst);
    1055            }
    1056
    1057            case TagConstants.UNREACHABLE:
    1058              checkNoModifiers(tag, loc);
    1059              dst.ttype = TagConstants.STMTPRAGMA;
    1060              dst.auxVal = SimpleStmtPragma.make(tag, loc).setOriginalTag(tag);
    1061              if (scanner.ttype == TagConstants.SEMICOLON) scanner.getNextToken();
    1062              break;
    1063
    1064            case TagConstants.ASSERT:
    1065              // The ASSERT token is not obtained from an identifier
    1066              // so the scanner was not advanced.
    1067              scanner.getNextToken();
    1068            case TagConstants.ASSERT_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1069            {
    1070              checkNoModifiers(tag, loc);
    1071              dst.ttype = TagConstants.STMTPRAGMA;
    1072              Expr assertion = parseExpression(scanner);
    1073              Expr label = null;
    1074              if (scanner.ttype == TagConstants.COLON) {
    1075                scanner.getNextToken();
    1076                label = parseExpression(scanner);
    1077              }
    1078              ExprStmtPragma pragma = ExprStmtPragma.make(TagConstants
    1079                  .unRedundant(tag), assertion, label, loc);
    1080              if (TagConstants.isRedundant(tag))
    1081                pragma.setRedundant(true);
    1082              pragma.setOriginalTag(tag);
    1083              dst.auxVal = pragma;
    1084              semicolonExpected = true;
    1085              break;
    1086            }
    1087
    1088            case TagConstants.HENCE_BY_REDUNDANTLY:
    1089            case TagConstants.HENCE_BY:
    1090            case TagConstants.ASSUME:
    1091            case TagConstants.DECREASES:
    1092            case TagConstants.ASSUME_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1093            case TagConstants.DECREASES_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1094            case TagConstants.DECREASING: // SUPPORT COMPLETE (kiniry)
    1095            case TagConstants.DECREASING_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1096            case TagConstants.LOOP_INVARIANT_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1097            case TagConstants.MAINTAINING: // SUPPORT COMPLETE (kiniry)
    1098            case TagConstants.MAINTAINING_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1099            case TagConstants.LOOP_INVARIANT:
    1100            {
    1101              checkNoModifiers(tag, loc);
    1102              dst.ttype = TagConstants.STMTPRAGMA;
    1103              ExprStmtPragma pragma = ExprStmtPragma.make(TagConstants
    1104                  .unRedundant(tag), parseExpression(scanner), null, loc);
    1105              if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1106              pragma.setOriginalTag(tag);
    1107              dst.auxVal = pragma;
    1108              semicolonExpected = true;
    1109              break;
    1110            }
    1111
    1112            case TagConstants.LOOP_PREDICATE:
    1113              checkNoModifiers(tag, loc);
    1114              inProcessTag = tag;
    1115              inProcessLoc = loc;
    1116              continuePragma(dst);
    1117              semicolonExpected = true;
    1118              if (DEBUG)
    1119                  Info.out("getNextPragma: parsed a loop predicate: "
    1120                      + dst.ztoString());
    1121              return true;
    1122
    1123            case TagConstants.SET:
    1124            {
    1125              checkNoModifiers(tag, loc);
    1126              dst.ttype = TagConstants.STMTPRAGMA;
    1127              Expr target = parsePrimaryExpression(scanner);
    1128              int locOp = scanner.startingLoc;
    1129              expect(scanner, TagConstants.ASSIGN);
    1130              Expr value = parseExpression(scanner);
    1131              dst.auxVal = SetStmtPragma.make(target, locOp, value, loc)
    1132                                                    .setOriginalTag(tag);
    1133              semicolonExpected = true;
    1134              break;
    1135            }
    1136
    1137            case TagConstants.REPRESENTS: // SC HPT AAST 4 SUPPORT COMPLETE (cok)
    1138            case TagConstants.REPRESENTS_REDUNDANTLY: // SC HPT AAST 4 (cok)
    1139            {
    1140              // FIXME - need to utilize modifiers
    1141              dst.ttype = TagConstants.TYPEDECLELEMPRAGMA;
    1142              // FIXME - the grammar wants a StoreRefExpr here ???
    1143              int locId = scanner.startingLoc;
    1144              Identifier id = parseIdentifier(scanner);
    1145              Expr target = AmbiguousVariableAccess
    1146                  .make(SimpleName.make(id, locId));
    1147              NamedExprDeclPragma e;
    1148              int locOp = scanner.startingLoc;
    1149              if (scanner.ttype == TagConstants.LEFTARROW
    1150                  || scanner.ttype == TagConstants.ASSIGN) {
    1151                scanner.getNextToken();
    1152                Expr value = parseExpression(scanner);
    1153                Expr target2 = AmbiguousVariableAccess.make(SimpleName.make(id,
    1154                    locId));
    1155                e = NamedExprDeclPragma.make(TagConstants.unRedundant(tag),
    1156                    BinaryExpr.make(TagConstants.EQ, target, value, locOp),
    1157                    target2, modifiers, loc);
    1158              } else if (scanner.ttype == TagConstants.SUCH_THAT) {
    1159                expect(scanner, TagConstants.SUCH_THAT);
    1160                Expr value = parseExpression(scanner);
    1161                e = NamedExprDeclPragma.make(TagConstants.unRedundant(tag), value,
    1162                    target, modifiers, loc);
    1163              } else {
    1164                ErrorSet.error(locOp, "Invalid syntax for a represents clause.");
    1165                // Skip this invalid clause
    1166                eatThroughSemiColon();
    1167                return getNextPragmaHelper(dst);
    1168              }
    1169              e.setRedundant(TagConstants.isRedundant(tag));
    1170              dst.auxVal = e;
    1171              semicolonExpected = true;
    1172              break;
    1173            }
    1174
    1175            case TagConstants.CONSTRAINT_REDUNDANTLY: // SC AAST 4
    1176            case TagConstants.CONSTRAINT: // SC AAST 4
    1177            {
    1178              // FIXME - need to utilize modifiers
    1179              dst.ttype = TagConstants.TYPEDECLELEMPRAGMA;
    1180              ExprDeclPragma pragma = ExprDeclPragma.make(TagConstants
    1181                  .unRedundant(tag), parseExpression(scanner), modifiers, loc);
    1182              if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1183              dst.auxVal = pragma;
    1184              semicolonExpected = true;
    1185              if (scanner.ttype != TagConstants.SEMICOLON) {
    1186                // FIXME - for clause of constraint needs implementing
    1187                eatThroughSemiColon();
    1188                semicolonExpected = false;
    1189              }
    1190              break;
    1191            }
    1192
    1193            case TagConstants.AXIOM:
    1194              checkNoModifiers(tag, loc);
    1195            // fall-through
    1196            case TagConstants.INVARIANT:
    1197            case TagConstants.INITIALLY: // SC AAST 4 parsed (cok)
    1198            case TagConstants.INVARIANT_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1199            {
    1200              // Need to utilize modifiers -- FIXME
    1201              dst.ttype = TagConstants.TYPEDECLELEMPRAGMA;
    1202              ExprDeclPragma pragma = ExprDeclPragma.make(TagConstants
    1203                  .unRedundant(tag), parseExpression(scanner), modifiers, loc);
    1204              if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1205              dst.auxVal = pragma;
    1206              semicolonExpected = true;
    1207              break;
    1208            }
    1209
    1210            case TagConstants.IMPORT:
    1211              checkNoModifiers(tag, loc);
    1212              // SUPPORT COMPLETE (cok)
    1213              ErrorSet.caution(loc, "An import statement in an annotation "
    1214                  + "should begin with 'model import'");
    1215              scanner.lexicalPragmas.addElement(ImportPragma.make(
    1216                  parseImportDeclaration(scanner), loc));
    1217              // parseImportDeclaration parses the semicolon
    1218              return getNextPragmaHelper(dst);
    1219              // no fall-through
    1220
    1221            case TagConstants.GHOST:
    1222              // modifiers are used later when we get to the declaration
    1223              // let them accumulate
    1224              if (savedGhostModelPragma != null) {
    1225                ErrorSet.caution(loc, "Duplicate " + TagConstants.toString(tag)
    1226                    + " tag", savedGhostModelPragma.getStartLoc());
    1227              } else {
    1228                savedGhostModelPragma = SimpleModifierPragma.make(tag, loc);
    1229              }
    1230              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1231              dst.auxVal = SimpleModifierPragma.make(tag, loc);
    1232              break;
    1233
    1234            case TagConstants.MODEL:
    1235              // modifiers are used later when we get to the declaration
    1236              // let them accumulate
    1237              // SUPPORT COMPLETE (cok)
    1238              if (scanner.lookahead(0) == TagConstants.IMPORT) {
    1239                scanner.lexicalPragmas.addElement(ImportPragma.make(
    1240                    parseImportDeclaration(scanner), loc));
    1241                // parseImportDeclaration parses the semicolon
    1242
    1243                return getNextPragmaHelper(dst);
    1244              }
    1245              if (savedGhostModelPragma != null) {
    1246                ErrorSet.caution(loc, "Duplicate " + TagConstants.toString(tag)
    1247                    + " tag", savedGhostModelPragma.getStartLoc());
    1248              } else {
    1249                savedGhostModelPragma = SimpleModifierPragma.make(tag, loc);
    1250              }
    1251              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1252              dst.auxVal = SimpleModifierPragma.make(tag, loc);
    1253              break;
    1254
    1255            case TagConstants.SKOLEM_CONSTANT:
    1256            {
    1257              checkNoModifiers(tag, loc);
    1258              dst.ttype = TagConstants.STMTPRAGMA;
    1259
    1260              int locType = scanner.startingLoc;
    1261              Type type = parseType(scanner);
    1262
    1263              LocalVarDeclVec v = LocalVarDeclVec.make();
    1264              int nextTtype;
    1265
    1266              loop: while (true) {
    1267                int locId = scanner.startingLoc;
    1268                Identifier id = parseIdentifier(scanner);
    1269                Type vartype = parseBracketPairs(scanner, type);
    1270
    1271                LocalVarDecl decl = LocalVarDecl.make(Modifiers.NONE, null, id,
    1272                    vartype, locId, null, Location.NULL);
    1273                v.addElement(decl);
    1274
    1275                switch (scanner.ttype) {
    1276                  case TagConstants.COMMA:
    1277                    scanner.getNextToken();
    1278                    continue loop;
    1279
    1280                  default:
    1281                    fail(scanner.startingLoc,
    1282                        "Expected comma or semicolon in skolem_constant decl");
    1283
    1284                  case TagConstants.SEMICOLON:
    1285                    break loop;
    1286
    1287                }
    1288              }
    1289
    1290              dst.auxVal = SkolemConstantPragma.make(v, locType,
    1291                  scanner.startingLoc);
    1292              semicolonExpected = true;
    1293              break;
    1294            }
    1295
    1296            case TagConstants.NO_WACK_FORALL:
    1297            // this is 'forall', *NOT* '\forall'
    1298            {
    1299              Type type = parseType(scanner);
    1300              while (true) {
    1301                int locId = scanner.startingLoc;
    1302                Identifier id = parseIdentifier(scanner);
    1303                Type vartype = parseBracketPairs(scanner, type);
    1304                if (scanner.ttype == TagConstants.ASSIGN) {
    1305                  ErrorSet.error(scanner.startingLoc,
    1306                      "forall annotations may not have initializers");
    1307                  eatUpToCommaOrSemiColon();
    1308                }
    1309                LocalVarDecl decl = LocalVarDecl.make(Modifiers.NONE, null, id,
    1310                    vartype, locId, null, Location.NULL);
    1311                dst.ttype = TagConstants.MODIFIERPRAGMA;
    1312                dst.auxVal = VarDeclModifierPragma.make(tag, decl, loc, locId);
    1313                savePragma(locId, TagConstants.MODIFIERPRAGMA, dst.auxVal);
    1314                if (scanner.ttype != TagConstants.COMMA) break;
    1315                scanner.getNextToken(); // eat comma
    1316              }
    1317              //if (!getPragma(dst)) return getNextPragmaHelper(dst);
    1318              dst.ttype = TagConstants.NULL;
    1319              semicolonExpected = true;
    1320              break;
    1321            }
    1322
    1323            case TagConstants.OLD:
    1324            {
    1325              Type type = parseType(scanner);
    1326              if (scanner.ttype == TagConstants.ASSIGN) {
    1327                ErrorSet.error(scanner.startingLoc, "Missing type or id");
    1328                eatThroughSemiColon();
    1329                semicolonExpected = false;
    1330                return getNextPragmaHelper(dst);
    1331              }
    1332              semicolonExpected = true;
    1333              while (true) {
    1334
    1335                int locId = scanner.startingLoc;
    1336                Identifier id = parseIdentifier(scanner);
    1337                Type vartype = parseBracketPairs(scanner, type);
    1338                if (scanner.ttype != TagConstants.ASSIGN) {
    1339                  ErrorSet.error(locId, "old annotations must be initialized");
    1340                  if (scanner.ttype == TagConstants.COMMA) {
    1341                    scanner.getNextToken();
    1342                    continue;
    1343                  }
    1344                  eatThroughSemiColon();
    1345                  semicolonExpected = false;
    1346                  break;
    1347                } else {
    1348                  int locAssignOp = scanner.startingLoc;
    1349                  scanner.getNextToken();
    1350                  VarInit init = parseVariableInitializer(scanner, false);
    1351                  if (init instanceof Expr) {
    1352                    ExprVec args = ExprVec.make();
    1353                    args.addElement((Expr)init);
    1354                    init = NaryExpr.make(loc, locAssignOp, TagConstants.PRE, null,
    1355                        args);
    1356                  } else {
    1357                    ErrorSet.error(locAssignOp,
    1358                        "Array initializers in old statements are not implemented");
    1359                    if (scanner.ttype == TagConstants.COMMA) {
    1360                      scanner.getNextToken();
    1361                      continue;
    1362                    }
    1363                    break;
    1364                  }
    1365                  OldVarDecl decl = OldVarDecl.make(id, vartype, locId, init,
    1366                      locAssignOp);
    1367
    1368                  savePragma(loc, TagConstants.MODIFIERPRAGMA,
    1369                      VarDeclModifierPragma.make(tag, decl, loc, locId));
    1370
    1371                  if (scanner.ttype != TagConstants.COMMA) break;
    1372                  scanner.getNextToken(); // eats comma
    1373                }
    1374
    1375              }
    1376              dst.ttype = TagConstants.NULL;
    1377              break;
    1378            }
    1379
    1380            case TagConstants.OPENPRAGMA: // complete (ok)
    1381            case TagConstants.CLOSEPRAGMA: // complete (cok)
    1382              scanner.getNextToken();
    1383            // punctuation does not look like an identifier so it
    1384            // does not get advanced up at the top
    1385            // fall-through
    1386            case TagConstants.CODE_BIGINT_MATH:
    1387            case TagConstants.CODE_JAVA_MATH:
    1388            case TagConstants.CODE_SAFE_MATH:
    1389            case TagConstants.FUNCTION:
    1390            case TagConstants.HELPER:
    1391            case TagConstants.IMMUTABLE:
    1392            case TagConstants.INSTANCE: // complete (cok)
    1393            case TagConstants.MAY_BE_NULL: // incomplete (chalin/kiniry)
    1394            case TagConstants.MONITORED: // incomplete
    1395            case TagConstants.NON_NULL: // incomplete
    1396            case TagConstants.NON_NULL_REF_BY_DEFAULT: // incomplete (chalin/kiniry)
    1397            case TagConstants.NULL_REF_BY_DEFAULT: // incomplete (chalin/kiniry)
    1398            case TagConstants.OBS_PURE: // incomplete (chalin/kiniry)
    1399            case TagConstants.PEER: // parsed but not typechecked - Universe type annotation (cjbooms)
    1400            case TagConstants.PURE:
    1401            case TagConstants.READONLY: // parsed but not typechecked - Universe type annotation (cjbooms)
    1402            case TagConstants.REP: // parsed but not typechecked - Universe type annotation (cjbooms)
    1403            case TagConstants.SPEC_BIGINT_MATH:
    1404            case TagConstants.SPEC_JAVA_MATH:
    1405            case TagConstants.SPEC_PROTECTED: // SC HPT AAST 3, SUPPORT COMPLETE (cok)
    1406            case TagConstants.SPEC_PUBLIC: // incomplete
    1407            case TagConstants.SPEC_SAFE_MATH:
    1408            case TagConstants.UNINITIALIZED: // incomplete
    1409            case TagConstants.WRITABLE_DEFERRED: // incomplete
    1410              // let modifiers accumulate
    1411              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1412              dst.auxVal = SimpleModifierPragma.make(tag, loc);
    1413              break;
    1414
    1415            case TagConstants.ALSO_ENSURES:
    1416            case TagConstants.ALSO_REQUIRES:
    1417              int oldtag = tag;
    1418              if (tag == TagConstants.ALSO_ENSURES)
    1419                tag = TagConstants.ENSURES;
    1420              else if (tag == TagConstants.ALSO_REQUIRES)
    1421                  tag = TagConstants.REQUIRES;
    1422              ErrorSet.error(loc,
    1423                             "Original ESC/Java keywords beginning with also_ are " +
    1424                             "obsolete; they have been replaced with the corresponding " +
    1425                             "JML keywords and the use of 'also' - note that the " +
    1426                             "semantics has also changed.");
    1427            // fall through
    1428            case TagConstants.ENSURES:
    1429            case TagConstants.DIVERGES: // parsed (cok)
    1430            case TagConstants.DIVERGES_REDUNDANTLY: // parsed (cok)
    1431            case TagConstants.ENSURES_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1432            case TagConstants.POSTCONDITION: // SUPPORT COMPLETE (kiniry)
    1433            case TagConstants.POSTCONDITION_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1434            case TagConstants.PRECONDITION: // SUPPORT COMPLETE (kiniry)
    1435            case TagConstants.PRECONDITION_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1436            case TagConstants.REQUIRES_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1437            case TagConstants.WHEN: // NOT SC, parsed but concurrent only (cok)
    1438            case TagConstants.WHEN_REDUNDANTLY: // ditto
    1439            case TagConstants.READABLE_IF:
    1440            case TagConstants.REQUIRES:
    1441            case TagConstants.WRITABLE_IF:
    1442            {
    1443              checkNoModifiers(tag, loc);
    1444              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1445              ExprModifierPragma pragma;
    1446              if (scanner.ttype == TagConstants.NOT_SPECIFIED) {
    1447                pragma = ExprModifierPragma.make(TagConstants.unRedundant(tag),
    1448                    NotSpecifiedExpr.make(scanner.startingLoc), loc);
    1449                scanner.getNextToken();
    1450              } else {
    1451                // SpecExpr [';']
    1452                pragma = ExprModifierPragma.make(TagConstants.unRedundant(tag),
    1453                    parseExpression(scanner), loc);
    1454              }
    1455              if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1456              dst.auxVal = pragma;
    1457              semicolonExpected = true;
    1458              break;
    1459            }
    1460
    1461    //         case TagConstants.WACK_JAVA_MATH:
    1462    //         case TagConstants.WACK_SAFE_MATH:
    1463    //         case TagConstants.WACK_BIGINT_MATH: {
    1464    //           // @todo check that token consumed is '(' and if not emit a warning
    1465    //           // and try to unparse token and parse next expr to build ExprModifierPragma
    1466    //           l.getNextToken();
    1467    //           Expr e = parseExpression(l);
    1468    //           dst.ttype = TagConstants.MODIFIERPRAGMA;
    1469    //           ExprModifierPragma pragma = ExprModifierPragma.make(tag, e, loc);
    1470    //           // make sure token is closing ')' and if not emit warning that it is
    1471    //           // mandatory, pop, and continue
    1472    //           l.getNextToken();
    1473    //           dst.auxVal = pragma;
    1474    //           break;
    1475    //         }
    1476
    1477            case TagConstants.MEASURED_BY: // parsed, unclear semantics (cok)
    1478            case TagConstants.MEASURED_BY_REDUNDANTLY: // parsed, unclear semantics (cok)
    1479            case TagConstants.DURATION: // SC HPT 2
    1480            case TagConstants.DURATION_REDUNDANTLY: // SC HPT 2
    1481            case TagConstants.WORKING_SPACE: // SC HPT 2
    1482            case TagConstants.WORKING_SPACE_REDUNDANTLY:// SC HPT 2
    1483            // parsed and returned (cok)
    1484            {
    1485              checkNoModifiers(tag, loc);
    1486              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1487              CondExprModifierPragma pragma;
    1488              if (scanner.ttype == TagConstants.NOT_SPECIFIED) {
    1489                // \not_specified ;
    1490                pragma = CondExprModifierPragma.make(TagConstants.unRedundant(tag),
    1491                    NotSpecifiedExpr.make(scanner.startingLoc), loc, null);
    1492                scanner.getNextToken(); // reads semicolon
    1493              } else {
    1494                // SpecExpr [';']
    1495                pragma = CondExprModifierPragma.make(TagConstants.unRedundant(tag),
    1496                    parseExpression(scanner), loc, null);
    1497              }
    1498              if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1499              dst.auxVal = pragma;
    1500              semicolonExpected = true;
    1501              if (scanner.ttype == TagConstants.IF) {
    1502                scanner.getNextToken(); // read the if
    1503                pragma.cond = parseExpression(scanner);
    1504              }
    1505              break;
    1506            }
    1507
    1508            case TagConstants.ALSO_EXSURES:
    1509              tag = TagConstants.EXSURES;
    1510              ErrorSet.error(loc,
    1511                             "Original ESC/Java keywords beginning with also_ are " +
    1512                             "obsolete; they have been replaced with the " +
    1513                             "corresponding JML keywords and the use of 'also' - " +
    1514                             "note that the semantics has also changed.");
    1515            // fall through
    1516            case TagConstants.EXSURES:
    1517            case TagConstants.EXSURES_REDUNDANTLY: // SUPPORT COMPLETE (kiniry)
    1518            case TagConstants.SIGNALS: // SUPPORT COMPLETE (kiniry)
    1519            case TagConstants.SIGNALS_REDUNDANTLY:
    1520            {
    1521              checkNoModifiers(tag, loc);
    1522              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1523              expect(scanner, TagConstants.LPAREN);
    1524              FormalParaDecl arg = parseExsuresFormalParaDecl(scanner);
    1525              expect(scanner, TagConstants.RPAREN);
    1526              Expr expr = null;
    1527              // FIXME - test the semicolon and the not specified alternatives
    1528              // do we need a getNextToken()?
    1529              if (scanner.ttype == TagConstants.SEMICOLON)
    1530                expr = LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.TRUE,
    1531                    scanner.startingLoc);
    1532              else if (scanner.ttype == TagConstants.NOT_SPECIFIED) {
    1533                expr = NotSpecifiedExpr.make(scanner.startingLoc);
    1534                scanner.getNextToken();
    1535              } else
    1536                expr = parseExpression(scanner);
    1537              VarExprModifierPragma pragma = VarExprModifierPragma.make(
    1538                  TagConstants.SIGNALS, arg, expr, loc);
    1539              if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1540              pragma.setOriginalTag(tag);
    1541              dst.auxVal = pragma;
    1542              semicolonExpected = true;
    1543              break;
    1544            }
    1545
    1546            case TagConstants.SIGNALS_ONLY:
    1547            {
    1548              checkNoModifiers(tag, loc);
    1549              int ploc = loc;
    1550              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1551              Name name;
    1552              semicolonExpected = true;
    1553              Expr expr = LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.FALSE, loc);
    1554              Identifier id = TagConstants.ExsuresIdnName;
    1555              FormalParaDecl arg = FormalParaDecl.make(0,null,
    1556                  id, Main.options().useThrowable ?
    1557                       javafe.tc.Types.javaLangThrowable():
    1558                       javafe.tc.Types.javaLangException(),
    1559                  ploc);
    1560              if (scanner.ttype == TagConstants.SEMICOLON) {
    1561                ErrorSet.caution(scanner.startingLoc,
    1562                  "Use either \\nothing or a comma-separated list of type names " +
    1563                  "after a signals_only keyword");
    1564                // skip - expression is false
    1565              } else if (scanner.ttype == TagConstants.NOTHING) {
    1566                scanner.getNextToken();
    1567                // skip - expression is false
    1568              } else while (true) {
    1569                if (scanner.ttype == TagConstants.IDENT) {
    1570                  name = parseName(scanner);
    1571                  int thisloc = name.getStartLoc();
    1572                  Expr e = InstanceOfExpr.make(
    1573                          VariableAccess.make(id,thisloc,arg),
    1574                          TypeName.make(null,name),
    1575                          thisloc);
    1576                  expr = BinaryExpr.make(TagConstants.OR,
    1577                          expr, e, thisloc);
    1578                } else {
    1579                  ErrorSet.error(scanner.startingLoc,
    1580                      "Expected a type name");
    1581                  eatThroughSemiColon();
    1582                  semicolonExpected = false;
    1583                  break;
    1584                }
    1585                if (scanner.ttype != TagConstants.COMMA) break;
    1586                scanner.getNextToken();
    1587              }
    1588              VarExprModifierPragma pragma = VarExprModifierPragma.make(
    1589                  TagConstants.SIGNALS,
    1590                  arg, expr, ploc);
    1591              pragma.setOriginalTag(TagConstants.SIGNALS_ONLY);
    1592              dst.auxVal = pragma;
    1593              break;
    1594            }
    1595
    1596            case TagConstants.REFINE:
    1597            {
    1598              checkNoModifiers(tag, loc);
    1599              int sloc = scanner.startingLoc;
    1600              Expr e = parsePrimaryExpression(scanner);
    1601              if (!(e instanceof LiteralExpr)
    1602                  || e.getTag() != TagConstants.STRINGLIT) {
    1603                ErrorSet.error(sloc, "Expected a string literal after 'refine'");
    1604                eatThroughSemiColon();
    1605              } else {
    1606                expect(scanner, TagConstants.SEMICOLON);
    1607                scanner.lexicalPragmas.addElement(RefinePragma.make(
    1608                    (String)((LiteralExpr)e).value, loc));
    1609              }
    1610              return getNextPragmaHelper(dst);
    1611            }
    1612
    1613            // The following clauses must be followed by a semi-colon.
    1614            case TagConstants.IN:
    1615            case TagConstants.IN_REDUNDANTLY:
    1616            {
    1617              boolean first = true;
    1618              do {
    1619                boolean more = parseInPragmas(tag, loc, dst, first);
    1620                if (more)
    1621                  savePragma(dst);
    1622                else if (first)
    1623                  return getNextPragmaHelper(dst);
    1624                else
    1625                  break;
    1626                first = false;
    1627              } while (true);
    1628              dst.ttype = TagConstants.NULL;
    1629              semicolonExpected = true;
    1630              break;
    1631            }
    1632
    1633            case TagConstants.MAPS:
    1634            case TagConstants.MAPS_REDUNDANTLY:
    1635            {
    1636              // Already parsed something - should be an identifier
    1637              //System.out.println("MAPPING " + scanner.identifierVal.toString());
    1638              Identifier id = scanner.identifierVal;
    1639              Expr mapsod = parseMapsMemberFieldRef(scanner);
    1640              if (mapsod == null) {
    1641                // already wrote an error message
    1642                eatThroughSemiColon();
    1643                semicolonExpected = false;
    1644              } else if (scanner.identifierVal == null
    1645                  || !scanner.identifierVal.toString().equals("\\into")) {
    1646                ErrorSet.error(scanner.startingLoc,
    1647                    "Expected \\into in the maps clause here");
    1648                eatThroughSemiColon();
    1649                semicolonExpected = false;
    1650              } else {
    1651                scanner.getNextToken(); // skip \into
    1652                LinkedList groups = parseGroupList();
    1653                Iterator ig = groups.iterator();
    1654                while (ig.hasNext()) {
    1655                  Expr e = (Expr)ig.next();
    1656                  MapsExprModifierPragma pragma = MapsExprModifierPragma.make(
    1657                      TagConstants.unRedundant(tag), id, mapsod, loc, e);
    1658                  if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    1659                  dst.startingLoc = loc;
    1660                  dst.auxVal = pragma;
    1661                  dst.ttype = TagConstants.POSTMODIFIERPRAGMA;
    1662                  savePragma(dst);
    1663                }
    1664                dst.ttype = TagConstants.NULL;
    1665                semicolonExpected = false;
    1666                break;
    1667              }
    1668            }
    1669
    1670            // Unsupported JML clauses/keywords.
    1671
    1672            case TagConstants.ACCESSIBLE_REDUNDANTLY:
    1673            // SC HPT AAST 2 unclear syntax and semantics (kiniry)
    1674            case TagConstants.ACCESSIBLE:
    1675            // SC HPT AAST 2 unclear syntax and semantics (kiniry)
    1676            case TagConstants.BREAKS_REDUNDANTLY:
    1677            // unclear syntax and semantics (kiniry)
    1678            case TagConstants.BREAKS:
    1679            // unclear syntax and semantics (kiniry)
    1680            case TagConstants.CALLABLE_REDUNDANTLY:
    1681            // unclear syntax and semantics (kiniry)
    1682            case TagConstants.CALLABLE:
    1683            // unclear semantics (kiniry)
    1684            case TagConstants.CONTINUES_REDUNDANTLY:
    1685            // unclear syntax and semantics (kiniry)
    1686            case TagConstants.CONTINUES:
    1687            // unclear syntax and semantics (kiniry)
    1688            case TagConstants.RETURNS_REDUNDANTLY:
    1689            // unclear syntax and semantics (kiniry)
    1690            case TagConstants.RETURNS:
    1691              // unclear syntax and semantics (kiniry)
    1692              checkNoModifiers(tag, loc);
    1693              eatThroughSemiColon();
    1694              noteUnsupportedCheckableJmlPragma(loc, tag);
    1695              return getNextPragmaHelper(dst);
    1696
    1697            // The following clauses are block oriented, thus everything
    1698            // after them up to the next new block must be skipped.
    1699            case TagConstants.ABRUPT_BEHAVIOR:
    1700              // unclear syntax and semantics (kiniry)
    1701              ErrorSet.fatal(loc, "Encountered a keyword we recognize, "
    1702                  + "but do not know how to handle: " + tag + " "
    1703                  + TagConstants.toString(tag));
    1704              break;
    1705
    1706            // The following clauses are isolated keywords and can be skipped
    1707            // trivially.
    1708            case TagConstants.WEAKLY:
    1709              // unclear syntax and semantics (kiniry)
    1710              noteUnsupportedCheckableJmlPragma(loc, tag);
    1711              return getNextPragmaHelper(dst);
    1712
    1713            case TagConstants.MODEL_PROGRAM:
    1714            {
    1715              // unclear syntax and semantics (cok/kiniry)
    1716              // SKIP the compound statement
    1717              //checkNoModifiers(tag,loc);
    1718              // FIXME - allow but ignore modifiers for now
    1719              modifiers = Modifiers.NONE;
    1720              expect(scanner, TagConstants.LBRACE);
    1721              int braceCount = 1;
    1722              while (true) {
    1723                if (scanner.ttype == TagConstants.LBRACE) {
    1724                  ++braceCount;
    1725                } else if (scanner.ttype == TagConstants.RBRACE) {
    1726                  --braceCount;
    1727                  if (braceCount == 0) {
    1728                    scanner.getNextToken();
    1729                    break;
    1730                  }
    1731                }
    1732                scanner.getNextToken();
    1733              }
    1734              // FIXME - parse the compound statement and add it to
    1735              // the pragma
    1736              dst.ttype = TagConstants.MODIFIERPRAGMA;
    1737              dst.auxVal = ModelProgamModifierPragma.make(tag, loc);
    1738              inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    1739              // NO SEMICOLON
    1740              break;
    1741            }
    1742
    1743            // The following clauses have an unknown syntax, so if they are
    1744            // seen then the ESC/Java parser will fail.
    1745            case TagConstants.CHOOSE_IF:
    1746            // unclear semantics (kiniry)
    1747            case TagConstants.CHOOSE:
    1748            // unclear semantics (kiniry)
    1749            case TagConstants.INITIALIZER:
    1750            // SC AAST 4 unclear syntax and semantics (kiniry)
    1751            case TagConstants.OR:
    1752            // unclear semantics (kiniry)
    1753            case TagConstants.STATIC_INITIALIZER:
    1754              // SC AAST 4, unclear syntax and semantics (kiniry)
    1755              checkNoModifiers(tag, loc);
    1756              ErrorSet.fatal(loc, "Encountered a keyword we recognize, "
    1757                  + "but do not know how to parse: " + tag + " "
    1758                  + TagConstants.toString(tag));
    1759              break;
    1760
    1761            case TagConstants.CONSTRUCTOR:
    1762            case TagConstants.METHOD:
    1763              if (savedGhostModelPragma == null) {
    1764                ErrorSet.error(loc, "A " + TagConstants.toString(tag)
    1765                    + " keyword may only be used in a model method declaration");
    1766              }
    1767            // fall-through
    1768            case TagConstants.FIELDKW:
    1769              if (savedGhostModelPragma == null && tag == TagConstants.FIELDKW) {
    1770                ErrorSet.error(loc, "A " + TagConstants.toString(tag)
    1771                    + " keyword may only be used in a ghost or model declaration");
    1772              }
    1773              if (savedGhostModelPragma != null) {
    1774                semicolonExpected = parseDeclaration(dst, loc, tag);
    1775              }
    1776              break;
    1777
    1778            default:
    1779              if (savedGhostModelPragma != null) {
    1780                // model is special because it can be placed in any
    1781                // order like a simple modifier, but it signals that
    1782                // there is a regular field declaration within the
    1783                // annotation that follows (though there might be
    1784                // more modifiers and simple pragmas before the
    1785                // field declaration begins).  So we have gotten all
    1786                // of the modifiers above, and we see that one of them
    1787                // is ghost, so we go off to parse the field declaration
    1788                // Same for model.
    1789                semicolonExpected = parseDeclaration(dst, loc, 0);
    1790              } else {
    1791                ErrorSet.error(loc, "Unrecognized pragma: " + tag + " "
    1792                    + TagConstants.toString(tag));
    1793                // Skip to end
    1794                while (scanner.ttype != TagConstants.EOF)
    1795                  scanner.getNextToken();
    1796                modifiers = Modifiers.NONE;
    1797                return false;
    1798              }
    1799          }
    1800
    1801          if (semicolonExpected) {
    1802            modifiers = Modifiers.NONE;
    1803            eatSemiColon(kw);
    1804            if (savedGhostModelPragma != null) {
    1805              ErrorSet.error(savedGhostModelPragma.getStartLoc(),
    1806                  "Expected a declaration within the annotation following the "
    1807                      + TagConstants.toString(savedGhostModelPragma.getTag())
    1808                      + " keyword");
    1809              savedGhostModelPragma = null;
    1810            }
    1811            inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    1812          }
    1813          if (DEBUG) Info.out("getNextPragma: parsed : " + dst.ztoString());
    1814          return true;
    1815        } catch (javafe.util.FatalError e) {
    1816          modifiers = Modifiers.NONE;
    1817          savedGhostModelPragma = null;
    1818          eatThroughSemiColon();
    1819          return false;
    1820        } catch (IOException e) {
    1821          modifiers = Modifiers.NONE;
    1822          savedGhostModelPragma = null;
    1823          return false;
    1824        } finally {
    1825          //System.out.println("HELPER " + TagConstants.toString(scanner.ttype) + " " + TagConstants.toString(dst.ttype) + " " + dst.auxVal);
    1826        }
    1827      }
    1828
    1829      /**
    1830       * Issues an error if any Java modifiers have accumulated, and resets the
    1831       * accumulated modifiers to NONE.
    1832       */
    1833      //@ private normal_behavior
    1834      //@   requires modifiers == 0;
    1835      //@   modifies \nothing;
    1836      //@ also private behavior
    1837      //@   requires modifiers != 0;
    1838      //@   modifies modifiers, ErrorSet.cautions;
    1839      //@   ensures true;
    1840      //@   signals (Exception e) false;
    1841      //@
    1842      private void checkNoModifiers(int tag, int loc) {
    1843        if (modifiers != 0) {
    1844          ErrorSet.caution(loc, "Access modifiers are not allowed prior to "
    1845                           + TagConstants.toString(tag));
    1846          modifiers = Modifiers.NONE;
    1847        }
    1848      }
    1849
    1850      /**
    1851       * Emit an error message to the user that support for the supplied
    1852       * tag at the specified location is underway by a particular
    1853       * developer.
    1854       */
    1855      /* UNUSED
    1856       private void notePragmaUnderway(int loc, int tag, String username) {
    1857       ErrorSet.fatal(loc, "Unsupported pragma: " +
    1858       TagConstants.toString(tag) +
    1859       "; " + username + "@users.sf.net is working on it.");
    1860       }
    1861       */
    1862
    1863      /**
    1864       * Emit a caution to the user if verbosity is enabled that the
    1865       * supplied tag at the specified location is unsupported by the
    1866       * current version of ESC/Java but is statically checkable.
    1867       */
    1868      private void noteUnsupportedCheckableJmlPragma(int loc, int tag) {
    1869        if (Info.on)
    1870            ErrorSet.caution(loc, "Unsupported pragma '"
    1871                + TagConstants.toString(tag)
    1872                + "'; ESC/Java will not statically check this spec.");
    1873      }
    1874
    1875      /**
    1876       * Emit a caution to the user if verbosity is enabled that the
    1877       * supplied tag at the specified location is unsupported by the
    1878       * current version of ESC/Java and is statically uncheckable.
    1879       */
    1880      /* UNUNSED
    1881       private void noteUnsupportedUncheckableJmlPragma(int loc, int tag) {
    1882       if (Info.on)
    1883       ErrorSet.caution(loc, "Unsupported uncheckable pragma '" +
    1884       TagConstants.toString(tag) +
    1885       "' ignored.");
    1886       }
    1887       */
    1888
    1889      /**
    1890       * Eat tokens up through and including terminating semi-colon.
    1891       * This method is used to pretend like we are parsing
    1892       * semi-colon-terminated expressions in pragmas that we do not yet
    1893       * really parse or handle.
    1894       *
    1895       */
    1896      private void eatThroughSemiColon() {
    1897        while (scanner.ttype != TagConstants.SEMICOLON) {
    1898          if (scanner.ttype == TagConstants.EOF) return;
    1899          scanner.getNextToken();
    1900        }
    1901        // throw away final semi-colon
    1902        scanner.getNextToken();
    1903      }
    1904
    1905      private void eatUpToCommaOrSemiColon() {
    1906        while (scanner.ttype != TagConstants.SEMICOLON
    1907            && scanner.ttype != TagConstants.COMMA) {
    1908          if (scanner.ttype == TagConstants.EOF) return;
    1909          scanner.getNextToken();
    1910        }
    1911      }
    1912
    1913      /**
    1914       * Eat the next token if it is a semi-colon and, if the next
    1915       * token is a pragma (not EOF, thus not the end of the pragma)
    1916       * then issue an error message indicating that the specified
    1917       * identifier must be semi-colon terminated if it is followed by
    1918       * more pragmas.
    1919       */
    1920      private void eatSemiColon(Identifier kw) {
    1921        if (scanner.ttype == TagConstants.SEMICOLON) {
    1922
    1923          scanner.getNextToken();
    1924
    1925        } else if (scanner.ttype != TagConstants.EOF) {
    1926
    1927          if (kw != null)
    1928            ErrorSet.fatal(scanner.startingLoc, "Semicolon required when a "
    1929                + kw.toString() + " pragma is followed by another pragma (found "
    1930                + TagConstants.toString(scanner.ttype) + " instead).");
    1931          else
    1932            ErrorSet.fatal(scanner.startingLoc, "Semicolon required when a"
    1933                + " pragma is followed by another pragma (found "
    1934                + TagConstants.toString(scanner.ttype) + " instead).");
    1935
    1936        } else if (!Main.options().noSemicolonWarnings) {
    1937
    1938          ErrorSet.caution(scanner.startingLoc,
    1939              "JML requires annotations to be terminated with a semicolon");
    1940        }
    1941      }
    1942
    1943      // FIXME - should get rid of this method, along with inProcessTag
    1944      /*@ requires inProcessTag == TagConstants.LOOP_PREDICATE ||
    1945       @          inProcessTag == TagConstants.STILL_DEFERRED;
    1946       @*/
    1947      //@ requires scanner.startingLoc != Location.NULL;
    1948      //@ requires scanner.m_in != null;
    1949      private void continuePragma(/*@ non_null @*/Token dst) throws IOException {
    1950        if (inProcessTag == TagConstants.STILL_DEFERRED) {
    1951          int locId = scanner.startingLoc;
    1952          Identifier idn = parseIdentifier(scanner);
    1953          dst.ttype = TagConstants.TYPEDECLELEMPRAGMA;
    1954          dst.auxVal = StillDeferredDeclPragma.make(idn, inProcessLoc, locId);
    1955        } else if (inProcessTag == TagConstants.LOOP_PREDICATE) {
    1956          dst.startingLoc = inProcessLoc;
    1957          Expr e = parseExpression(scanner);
    1958          dst.auxVal = ExprStmtPragma.make(inProcessTag, e, null, inProcessLoc)
    1959                                                   .setOriginalTag(inProcessTag);
    1960          dst.ttype = TagConstants.STMTPRAGMA;
    1961          //        } else if (inProcessTag == TagConstants.DEPENDS) {
    1962          // FIXME - not sure why we end up here or what we are supposed to do
    1963        } else {
    1964          System.out.println("UNSUPPORTED TAG "
    1965              + TagConstants.toString(inProcessTag));
    1966          Assert.precondition(false);
    1967        }
    1968
    1969        switch (scanner.ttype) {
    1970          case TagConstants.SEMICOLON:
    1971            scanner.getNextToken();
    1972          case TagConstants.EOF:
    1973            inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    1974            break;
    1975
    1976          case TagConstants.COMMA:
    1977            scanner.getNextToken();
    1978            break;
    1979
    1980          default:
    1981            ErrorSet.fatal(scanner.startingLoc, "Unexpected token '"
    1982                + TagConstants.toString(scanner.ttype)
    1983                + "', expected ',', ';' or end-of-file");
    1984        }
    1985      }
    1986
    1987      // Special parsing methods for handling quantified expressions.
    1988
    1989      /**
    1990       * Parse a "primary expression" from <code>l</code>.  A primary
    1991       * expression is an expression of the form:
    1992       * <pre>
    1993       * \result
    1994       * \lockset
    1995       * (*...*)
    1996       * Function '('
    1997       * '\type' '('
    1998       * '(' {'\forall'|'\exists'} Type
    1999       * '(' {'\lblpos'|'\lblneg'} Idn
    2000       * </pre>
    2001       * or is a "normal" primary expression parsed with
    2002       * <code>ParseExpr.parsePrimaryExpression()</code>.
    2003       *
    2004       * @param l the lexer from which to read and parse.
    2005       * @return the parsed expression.
    2006       * @see javafe.parser.ParseExpr#parsePrimaryExpression(javafe.parser.Lex)
    2007       */
    2008      protected Expr parsePrimaryExpression(Lex l) {
    2009        /* Lookahead for:
    2010         *  \result
    2011         *  \lockset
    2012         *  (*...*)
    2013         *  Function '('
    2014         * '\type' '('
    2015         * '(' {'\forall'|'\exists'} Type
    2016         * '(' {'\lblpos'|'\lblneg'} Idn
    2017         */
    2018
    2019        //-@ uninitialized
    2020        Expr primary = null;
    2021
    2022        // First parse PrimaryCore into variable primary
    2023        switch (l.ttype) {
    2024          case TagConstants.RES:
    2025            primary = ResExpr.make(l.startingLoc);
    2026            l.getNextToken();
    2027            break;
    2028
    2029          case TagConstants.LS:
    2030            primary = LockSetExpr.make(l.startingLoc);
    2031            l.getNextToken();
    2032            break;
    2033
    2034          case TagConstants.INFORMALPRED_TOKEN:
    2035            primary = LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.TRUE,
    2036                l.startingLoc);
    2037            informalPredicateDecoration.set(primary, l.auxVal);
    2038            l.getNextToken();
    2039            break;
    2040
    2041          case TagConstants.IDENT:
    2042          {
    2043            // First comes a Name...
    2044            int loc = l.startingLoc;
    2045            Name n = parseName(l);
    2046
    2047            // May be followed by ( ArgumentListopt ) :
    2048            if (l.ttype == TagConstants.LPAREN) {
    2049              int locOpenParen = l.startingLoc;
    2050
    2051              Identifier kw = n.identifierAt(0);
    2052              int tag = TagConstants.fromIdentifier(kw);
    2053
    2054              if (n.size() != 1) {
    2055                ExprVec args = parseArgumentList(l);
    2056                primary = AmbiguousMethodInvocation.make(n, null, locOpenParen,
    2057                    args);
    2058                // fail(loc, "Annotations may not contain method calls");
    2059              } else {
    2060                switch (tag) {
    2061                  case TagConstants.IS_INITIALIZED:
    2062                  {
    2063                    l.getNextToken();
    2064                    Type subexpr = parseType(l);
    2065                    primary = TypeExpr.make(loc, l.startingLoc, subexpr);
    2066                    expect(l, TagConstants.RPAREN);
    2067                    ExprVec args = ExprVec.make(1);
    2068                    args.addElement(primary);
    2069                    primary = NaryExpr.make(loc, l.startingLoc, tag, null, args);
    2070                    break;
    2071                  }
    2072
    2073                  case TagConstants.TYPE:
    2074                  {
    2075                    l.getNextToken();
    2076                    Type subexpr = parseType(l);
    2077                    primary = TypeExpr.make(loc, l.startingLoc, subexpr);
    2078                    expect(l, TagConstants.RPAREN);
    2079                    break;
    2080                  }
    2081
    2082                  case TagConstants.DTTFSA:
    2083                  {
    2084                    l.getNextToken();
    2085                    Type t = parseType(l);
    2086                    TypeExpr te = TypeExpr.make(loc, l.startingLoc, t);
    2087                    expect(l, TagConstants.COMMA);
    2088                    ExprVec args = parseExpressionList(l, TagConstants.RPAREN);
    2089                    args.insertElementAt(te, 0);
    2090                    primary = NaryExpr.make(loc, l.startingLoc, tag, null, args);
    2091                    break;
    2092                  }
    2093
    2094                  case TagConstants.NOT_MODIFIED:
    2095                  {
    2096                    int sloc = l.startingLoc;
    2097                    l.getNextToken(); // parse (
    2098                    primary = NotModifiedExpr.make(sloc, parseExpression(l));
    2099                    while (l.ttype == TagConstants.COMMA) {
    2100                      l.getNextToken(); // skip comma
    2101                      Expr arg = NotModifiedExpr.make(l.startingLoc,
    2102                          parseExpression(l));
    2103                      primary = BinaryExpr.make(TagConstants.AND, primary, arg, arg
    2104                          .getStartLoc());
    2105                    }
    2106                    /*
    2107                     primary = null;
    2108                     int num = 0;
    2109                     while (true) {
    2110                     ++num;
    2111                     int exprLoc = l.startingLoc;
    2112                     Expr arg = parseExpression(l);
    2113                     ExprVec args = ExprVec.make(2);
    2114                     ExprVec args2 = ExprVec.make(1);
    2115                     args.addElement(arg);
    2116                     args2.addElement((Expr)arg.clone());
    2117                     Expr oldex =
    2118                     NaryExpr.make(exprLoc, l.startingLoc,
    2119                     TagConstants.PRE, null, args2);
    2120
    2121                     args.addElement(oldex);
    2122                     Expr p = NaryExpr.make(exprLoc, l.startingLoc,
    2123                     TagConstants.EQ, null, args);
    2124                     p = BinaryExpr.make(
    2125                     TagConstants.EQ, arg, oldex, exprLoc);
    2126                     p = LabelExpr.make(exprLoc,l.startingLoc,
    2127                     false,
    2128                     Identifier.intern("Modified-arg-"+
    2129                     num),
    2130                     p);
    2131                     if (primary == null) primary = p;
    2132                     else {
    2133                     primary = BinaryExpr.make(
    2134                     TagConstants.AND,
    2135                     primary, p, exprLoc);
    2136                     }
    2137                     if (l.ttype != TagConstants.COMMA) break;
    2138                     l.getNextToken(); // parse comma
    2139                     }
    2140                     */
    2141                    expect(l, TagConstants.RPAREN);
    2142                    break;
    2143                  }
    2144
    2145                  case TagConstants.WACK_NOWARN:
    2146                  case TagConstants.NOWARN_OP:
    2147                  case TagConstants.WARN:
    2148                  case TagConstants.WARN_OP:
    2149                  case TagConstants.FRESH:
    2150                  case TagConstants.REACH:
    2151                  case TagConstants.INVARIANT_FOR:
    2152                  case TagConstants.ELEMSNONNULL:
    2153                  case TagConstants.ELEMTYPE:
    2154                  case TagConstants.MAX:
    2155                  case TagConstants.PRE: // \\old
    2156                  case TagConstants.TYPEOF:
    2157                  case TagConstants.WACK_JAVA_MATH:
    2158                  case TagConstants.WACK_SAFE_MATH:
    2159                  case TagConstants.WACK_BIGINT_MATH:
    2160                  {
    2161                    l.getNextToken();
    2162                    ExprVec args = parseExpressionList(l, TagConstants.RPAREN);
    2163                    primary = NaryExpr.make(loc, l.startingLoc, tag, null, args);
    2164                    //primary = UnaryExpr.make(tag, args.elementAt(0), loc);
    2165                    break;
    2166                  }
    2167
    2168                  case TagConstants.WACK_DURATION:
    2169                  case TagConstants.WACK_WORKING_SPACE:
    2170                  case TagConstants.SPACE:
    2171                  {
    2172                    l.getNextToken();
    2173                    ExprVec args = parseExpressionList(l, TagConstants.RPAREN);
    2174                    primary = NaryExpr.make(loc, l.startingLoc, tag, null, args);
    2175                    //primary = UnaryExpr.make(tag, args.elementAt(0), loc);
    2176                    // FIXME why Nary instead of Unary?
    2177                    break;
    2178
    2179                  }
    2180
    2181                  default:
    2182                    // parseArgumentList requires that the scanner (l) must
    2183                    // be at the LPAREN, so we can't read the LPAREN token
    2184                    ExprVec args = parseArgumentList(l);
    2185                    primary = AmbiguousMethodInvocation.make(n, null, locOpenParen,
    2186                        args);
    2187                }
    2188              }
    2189              break;
    2190            }
    2191
    2192            // Look for 'TypeName . this'
    2193            if (l.lookahead(0) == TagConstants.FIELD
    2194                && l.lookahead(1) == TagConstants.THIS) {
    2195              expect(l, TagConstants.FIELD);
    2196              int locThis = l.startingLoc;
    2197              expect(l, TagConstants.THIS);
    2198              primary = ThisExpr.make(TypeName.make(n), locThis);
    2199              break;
    2200            }
    2201
    2202            // Or ([])* . class:
    2203            // (need to look ahead fully because of "<type>[] x;" declarations)
    2204            int i = 0;
    2205            while ((l.lookahead(i) == TagConstants.LSQBRACKET)
    2206                && (l.lookahead(i + 1) == TagConstants.RSQBRACKET))
    2207              i += 2;
    2208            if ((l.lookahead(i) == TagConstants.FIELD)
    2209                && (l.lookahead(i + 1) == TagConstants.CLASS)) {
    2210              Type t = TypeName.make(n);
    2211              t = parseBracketPairs(l, t);
    2212              primary = parseClassLiteralSuffix(l, t);
    2213              break;
    2214            }
    2215
    2216            // Ok, it must have just been a naked Name:
    2217            primary = AmbiguousVariableAccess.make(n);
    2218            break;
    2219          }
    2220
    2221          case TagConstants.LPAREN:
    2222          {
    2223            // LPAREN Expression RPAREN
    2224            int locOpenParen = l.startingLoc;
    2225            l.getNextToken();
    2226            boolean regularParenExpr = true;
    2227
    2228
    2229            while (l.ttype == TagConstants.IDENT) {
    2230              Identifier kw = l.identifierVal;
    2231              int tag = TagConstants.fromIdentifier(kw);
    2232              if (tag != TagConstants.PEER) break;
    2233                 // skip these for now - FIXME
    2234              l.getNextToken();
    2235            }
    2236
    2237            // First see if we have a (LBLxxx ...) or (quantifier ...)
    2238            if (l.ttype == TagConstants.IDENT) {
    2239              Identifier kw = l.identifierVal;
    2240              int tag = TagConstants.fromIdentifier(kw);
    2241              // If \max is followed by a ( then it is a function,
    2242              // otherwise it is a quantifier and we change the tag.
    2243              if (tag == TagConstants.MAX && l.lookahead(1) != TagConstants.LPAREN)
    2244                  tag = TagConstants.MAXQUANT;
    2245              if ((tag == TagConstants.LBLPOS || tag == TagConstants.LBLNEG)
    2246                  && l.lookahead(1) == TagConstants.IDENT) {
    2247                regularParenExpr = false;
    2248                boolean pos = (tag == TagConstants.LBLPOS);
    2249                l.getNextToken(); // Discard LBLxxx
    2250                Identifier label = l.identifierVal;
    2251                l.getNextToken();
    2252                Expr e = parseExpression(l);
    2253                primary = LabelExpr
    2254                    .make(locOpenParen, l.startingLoc, pos, label, e);
    2255                expect(l, TagConstants.RPAREN);
    2256              } else if (tag == TagConstants.FORALL || tag == TagConstants.MIN
    2257                  || tag == TagConstants.MAXQUANT || tag == TagConstants.NUM_OF
    2258                  || tag == TagConstants.SUM || tag == TagConstants.PRODUCT
    2259                  || tag == TagConstants.EXISTS) {
    2260                int lookahead = l.lookahead(1);
    2261                if (lookahead == TagConstants.IDENT
    2262                    || isPrimitiveKeywordTag(lookahead)) {
    2263                  regularParenExpr = false;
    2264                  l.getNextToken(); // Discard quantifier
    2265                  Type type = parseType(l);
    2266                  primary = parseQuantifierRemainder(l, tag, type, locOpenParen);
    2267                }
    2268              }
    2269            }
    2270            if (regularParenExpr) {
    2271              Expr e = parseExpression(l);
    2272              int locCloseParen = l.startingLoc;
    2273              expect(l, TagConstants.RPAREN);
    2274              primary = ParenExpr.make(e, locOpenParen, locCloseParen);
    2275            }
    2276            break;
    2277          }
    2278
    2279          case TagConstants.NEW:
    2280          {
    2281            int locNew = l.startingLoc;
    2282            l.getNextToken();
    2283
    2284            Type type = parsePrimitiveTypeOrTypeName(l);
    2285            if (l.ttype != TagConstants.LBRACE) {
    2286              // usual new expression
    2287              primary = parseNewExpressionTail(l, type, locNew);
    2288              break;
    2289            }
    2290            l.getNextToken();
    2291            // set comprehension
    2292            FormalParaDecl fp = parseFormalParaDecl(l);
    2293            expect(l, TagConstants.BITOR);
    2294            Expr e = parseExpression(l);
    2295            expect(l, TagConstants.RBRACE);
    2296            primary = SetCompExpr.make(type, fp, e);
    2297            // No suffix
    2298            return primary;
    2299          }
    2300          default:
    2301            primary = super.parsePrimaryExpression(l);
    2302        }
    2303
    2304        // Ok, parsed a PrimaryCore expression into primary.
    2305        // Now handle PrimarySuffix*
    2306
    2307        return parsePrimarySuffix(l, primary);
    2308      }
    2309
    2310      /**
    2311       * Parse the suffix of a "primary expression" from <code>l</code>,
    2312       * given the prefix primary expression <code>primary</code>.
    2313       *
    2314       * @param l the lexer from which to read and parse.
    2315       * @param primary the primary expression previously parsed.
    2316       * @return the parsed expression.
    2317       */
    2318
    2319      protected Expr parsePrimarySuffix(Lex l, Expr primary) {
    2320        while (true) {
    2321
    2322          if (l.ttype == TagConstants.FIELD && l.lookahead(1) == TagConstants.STAR) {
    2323            l.getNextToken();
    2324            int loc = l.startingLoc;
    2325            l.getNextToken();
    2326            primary = WildRefExpr.make(primary, null);
    2327
    2328          } else if ((l.ttype == TagConstants.LSQBRACKET)
    2329              && (l.lookahead(1) == TagConstants.STAR)
    2330              && (l.lookahead(2) == TagConstants.RSQBRACKET)) {
    2331            int locOpen = l.startingLoc;
    2332            l.getNextToken();
    2333            l.getNextToken();
    2334            int locClose = l.startingLoc;
    2335            l.getNextToken();
    2336            primary = ArrayRangeRefExpr.make(locOpen, primary, null, null);
    2337            // and go around again
    2338          } else if (l.ttype == TagConstants.LSQBRACKET) {
    2339            int locOpen = l.startingLoc;
    2340            l.getNextToken();
    2341            Expr e1 = parseExpression(l);
    2342            if (l.ttype == TagConstants.RSQBRACKET) {
    2343              int locClose = l.startingLoc;
    2344              expect(l, TagConstants.RSQBRACKET);
    2345              if (e1 instanceof BinaryExpr
    2346                  && ((BinaryExpr)e1).op == TagConstants.DOTDOT) {
    2347
    2348                primary = ArrayRangeRefExpr.make(locOpen, primary,
    2349                    ((BinaryExpr)e1).left, ((BinaryExpr)e1).right);
    2350              } else {
    2351                primary = ArrayRefExpr.make(primary, e1, locOpen, locClose);
    2352              }
    2353            } else {
    2354              // PROBLEM
    2355              ErrorSet.error(l.startingLoc,
    2356                  "Expected either .. or ] after an index expression");
    2357              return null;
    2358            }
    2359          } else {
    2360            Expr nprimary = super.parsePrimarySuffix(l, primary);
    2361            if (nprimary == primary) return primary;
    2362            primary = nprimary;
    2363          }
    2364        }
    2365      }
    2366
    2367      /**
    2368       * Parse the balance (everything after the quantifier to the end
    2369       * of the current quantified scope) of a quantifier expression
    2370       * from <code>l</code>.
    2371       *
    2372       * @param l the lexer from which to read and parse.
    2373       * @param tag identifies which kind of quantifier we are parsing.
    2374       * @param type the type of the quantified variable.
    2375       * @param loc the starting location of the quantified expression.
    2376       * @return the parsed quantified expression.
    2377       */
    2378      //@ requires l.m_in != null;
    2379      //@ requires type.syntax;
    2380      /*@ requires tag == TagConstants.FORALL || tag == TagConstants.EXISTS ||
    2381       @          tag == TagConstants.MAX || tag == TagConstants.MIN ||
    2382       @          tag == TagConstants.PRODUCT || tag == TagConstants.SUM ||
    2383       @          tag == TagConstants.NUM_OF;
    2384       @*/
    2385      private/*@ non_null */GCExpr parseQuantifierRemainder(
    2386      /*@ non_null @*/Lex l, int tag,
    2387      /*@ non_null @*/Type type, int loc) {
    2388        int idLoc = l.startingLoc;
    2389        Identifier idn = parseIdentifier(l);
    2390        LocalVarDecl v = LocalVarDecl.make(0, null, idn, type, idLoc, null,
    2391            Location.NULL);
    2392
    2393        GenericVarDeclVec vs = GenericVarDeclVec.make();
    2394        vs.addElement(v);
    2395
    2396        while (l.ttype == TagConstants.COMMA) {
    2397          l.getNextToken(); // skip comma
    2398          idLoc = l.startingLoc;
    2399          idn = parseIdentifier(l);
    2400          v = LocalVarDecl.make(0, null, idn, type, idLoc, null, Location.NULL);
    2401          vs.addElement(v);
    2402        }
    2403
    2404        int locSemi = Location.NULL;
    2405        /*-@ uninitialized */int endLoc = 0;
    2406        Expr rangeExpr = null;
    2407        /*-@ uninitialized */Expr rest = null;
    2408
    2409        if (l.ttype == TagConstants.SEMICOLON) {
    2410          l.getNextToken();
    2411          locSemi = l.startingLoc;
    2412          boolean emptyRange = false;
    2413          if (l.ttype == TagConstants.SEMICOLON) {
    2414            l.getNextToken(); // eat the semicolon
    2415            emptyRange = true;
    2416          }
    2417          rest = parseExpression(l);
    2418          if (!emptyRange && l.ttype == TagConstants.SEMICOLON) {
    2419            // there is a nonempty range expression
    2420            locSemi = l.startingLoc;
    2421            l.getNextToken(); // eat the semicolon
    2422            rangeExpr = rest;
    2423            rest = parseExpression(l);
    2424          }
    2425          endLoc = l.startingLoc;
    2426          expect(l, TagConstants.RPAREN);
    2427        } else
    2428          ErrorSet.fatal(l.startingLoc, "Syntax error in quantified expression.");
    2429        GCExpr returnExpr = null;
    2430        if (tag == TagConstants.FORALL) {
    2431          //if (rangeExpr != null) rest = BinaryExpr.make(TagConstants.IMPLIES,
    2432          //rangeExpr, rest, locSemi);
    2433          returnExpr = QuantifiedExpr.make(loc, endLoc, tag, vs, rangeExpr, rest,
    2434              null, null);
    2435        } else if (tag == TagConstants.EXISTS) {
    2436          //if (rangeExpr != null) rest = BinaryExpr.make(TagConstants.AND,
    2437          //rangeExpr, rest, locSemi);
    2438          returnExpr = QuantifiedExpr.make(loc, endLoc, tag, vs, rangeExpr, rest,
    2439              null, null);
    2440        } else if (tag == TagConstants.MAXQUANT || tag == TagConstants.MIN
    2441            || tag == TagConstants.PRODUCT || tag == TagConstants.SUM) {
    2442          if (rangeExpr == null) {
    2443            rangeExpr = LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.TRUE,
    2444                Location.NULL);
    2445          }
    2446          returnExpr = GeneralizedQuantifiedExpr.make(loc, endLoc, tag, vs, rest,
    2447              rangeExpr, null);
    2448        } else if (tag == TagConstants.NUM_OF) {
    2449          if (rangeExpr != null)
    2450              rest = BinaryExpr.make(TagConstants.AND, rangeExpr, rest, locSemi);
    2451          returnExpr = NumericalQuantifiedExpr.make(loc, endLoc, tag, vs,
    2452              rangeExpr, rest, null);
    2453        } else {
    2454          Assert.fail("Illegal quantifier seen at location " + loc);
    2455        }
    2456
    2457        return returnExpr;
    2458      }
    2459
    2460      // Overridden methods to handle new keywords and types specific
    2461      // to this parser.
    2462
    2463      /**
    2464       * Is a <code>tag</code> a PrimitiveType keyword?  Overriden to
    2465       * add type <code>TYPE</code>.
    2466       *
    2467       * @param tag the tag to check.
    2468       * @return a flag indicating if the supplied parameter is a
    2469       * primate type.
    2470       */
    2471      public boolean isPrimitiveKeywordTag(int tag) {
    2472        switch (tag) {
    2473          case TagConstants.TYPETYPE:
    2474          case TagConstants.REAL:
    2475          case TagConstants.BIGINT:
    2476            return true;
    2477
    2478          default:
    2479            return super.isPrimitiveKeywordTag(tag);
    2480        }
    2481      }
    2482
    2483      /**
    2484       * Parses a PrimitiveType.  Overriden to add type TYPE.  Returns
    2485       * <code>null</code> on failure.
    2486       *
    2487       * <p> PrimitiveType is one of: boolean byte short int long char
    2488       * float double void TYPE.
    2489       *
    2490       * @param l the lexer from which to read and parse.
    2491       * @return the parsed primative type.
    2492       */
    2493      public PrimitiveType parsePrimitiveType(Lex l) {
    2494        int tag;
    2495
    2496        switch (l.ttype) {
    2497          case TagConstants.TYPETYPE:
    2498            tag = TagConstants.TYPECODE;
    2499            break;
    2500          case TagConstants.REAL:
    2501            tag = TagConstants.REALTYPE;
    2502            break;
    2503          case TagConstants.BIGINT:
    2504            tag = TagConstants.BIGINTTYPE;
    2505            break;
    2506
    2507          default:
    2508            return super.parsePrimitiveType(l);
    2509        }
    2510        // get here => tag is defined
    2511
    2512        int loc = l.startingLoc;
    2513        l.getNextToken();
    2514        return PrimitiveType.make(tag, loc);
    2515      }
    2516
    2517      /**
    2518       * @param tag the tag to check.
    2519       * @return a flag indicating if <code>tag</code> is the start of
    2520       * an unary expression other than unary '+' or '-'.  Overridded
    2521       * to handle new identifier-like keywords "\result" and "\lockset".
    2522       */
    2523      public boolean isStartOfUnaryExpressionNotPlusMinus(int tag) {
    2524        // All previous cases apply...
    2525        if (super.isStartOfUnaryExpressionNotPlusMinus(tag)) return true;
    2526
    2527        // New Identifier-like keywords:
    2528        if (tag == TagConstants.RES || tag == TagConstants.LS) return true;
    2529
    2530        return false;
    2531      }
    2532
    2533      // Special handling for parsing exsures/signals clauses.
    2534
    2535      /**
    2536       * Parse the formal parameter declaration (the type and name of
    2537       * the associated exception) of an <code>exsures</code> or
    2538       * <code>signals</code> pragma.  This is a bit complicated because
    2539       * these expressions have an optional identifier name associated
    2540       * with the specified Throwable type.
    2541       *
    2542       * @param l the lexer from which to read and parse.
    2543       * @return the parsed formal paramater declaration.
    2544       */
    2545      //@ requires l.m_in != null;
    2546      // FIXME - do we really allow modifier pragmas in here?
    2547      public FormalParaDecl parseExsuresFormalParaDecl(
    2548      /*@ non_null @*/EscPragmaLex l) {
    2549        int modifiers = parseModifiers(l);
    2550        ModifierPragmaVec modifierPragmas = this.modifierPragmas;
    2551        Type paratype = parseExsuresType(l);
    2552        Identifier idn;
    2553        int locId = l.startingLoc;
    2554
    2555        if (l.ttype == TagConstants.IDENT) {
    2556          idn = l.identifierVal;
    2557          l.getNextToken();
    2558        } else {
    2559          idn = TagConstants.ExsuresIdnName;
    2560        }
    2561
    2562        // allow more modifier pragmas
    2563        modifierPragmas = parseMoreModifierPragmas(l, modifierPragmas);
    2564        return FormalParaDecl
    2565            .make(modifiers, modifierPragmas, idn, paratype, locId);
    2566      }
    2567
    2568      /**
    2569       * Parse the type of the of an <code>exsures</code> or
    2570       * <code>signals</code> pragma parameter.
    2571       *
    2572       * @param l the lexer from which to read and parse.
    2573       * @return the parsed type declaration.
    2574       */
    2575      //@ requires l.m_in != null;
    2576      //@ ensures \result.syntax;
    2577      public/*@ non_null */Type parseExsuresType(/*@ non_null @*/EscPragmaLex l) {
    2578        Type type = parseExsuresPrimitiveTypeOrTypeName(l);
    2579        return parseBracketPairs(l, type);
    2580      }
    2581
    2582      /**
    2583       * Parse the type associated with an <code>exsures</code> or
    2584       * <code>signals</code> pragma parameter.
    2585       *
    2586       * @param l the lexer from which to read and parse.
    2587       * @return the parsed type declaration.
    2588       */
    2589      //@ requires l.m_in != null;
    2590      //@ ensures \result.syntax;
    2591      public/*@ non_null */Type parseExsuresPrimitiveTypeOrTypeName(
    2592      /*@ non_null @*/EscPragmaLex l) {
    2593        Type type = parseExsuresPrimitiveType(l);
    2594        if (type != null)
    2595          return type;
    2596        else
    2597          return parseExsuresTypeName(l);
    2598      }
    2599
    2600      /**
    2601       * Parse the primitive type used in an <code>exsures</code> or
    2602       * <code>signals</code> pragma.
    2603       *
    2604       * @param l the lexer from which to read and parse.
    2605       * @return the parsed type declaration, if the type is primative.
    2606       */
    2607      //@ requires l.m_in != null;
    2608      //@ ensures \result != null ==> \result.syntax;
    2609      public PrimitiveType parseExsuresPrimitiveType(/*@ non_null @*/EscPragmaLex l) {
    2610        int tag;
    2611        switch (l.ttype) {
    2612          case TagConstants.TYPETYPE:
    2613            tag = TagConstants.TYPECODE;
    2614            break;
    2615          case TagConstants.REAL:
    2616            tag = TagConstants.REALTYPE;
    2617            break;
    2618          case TagConstants.BIGINT:
    2619            tag = TagConstants.BIGINTTYPE;
    2620            break;
    2621          case TagConstants.BOOLEAN:
    2622            tag = TagConstants.BOOLEANTYPE;
    2623            break;
    2624          case TagConstants.BYTE:
    2625            tag = TagConstants.BYTETYPE;
    2626            break;
    2627          case TagConstants.SHORT:
    2628            tag = TagConstants.SHORTTYPE;
    2629            break;
    2630          case TagConstants.INT:
    2631            tag = TagConstants.INTTYPE;
    2632            break;
    2633          case TagConstants.LONG:
    2634            tag = TagConstants.LONGTYPE;
    2635            break;
    2636          case TagConstants.CHAR:
    2637            tag = TagConstants.CHARTYPE;
    2638            break;
    2639          case TagConstants.FLOAT:
    2640            tag = TagConstants.FLOATTYPE;
    2641            break;
    2642          case TagConstants.DOUBLE:
    2643            tag = TagConstants.DOUBLETYPE;
    2644            break;
    2645          case TagConstants.VOID:
    2646            tag = TagConstants.VOIDTYPE;
    2647            break;
    2648          default:
    2649            return null; // Fail!
    2650        }
    2651        // get here => tag is defined
    2652        int loc = l.startingLoc;
    2653        l.getNextToken();
    2654        return PrimitiveType.make(tag, loc);
    2655      }
    2656
    2657      /**
    2658       * Parse the type name used in an <code>exsures</code> or
    2659       * <code>signals</code> pragma.
    2660       *
    2661       * @param l the lexer from which to read and parse.
    2662       * @return the parsed type declaration.
    2663       */
    2664      //@ requires l.m_in != null;
    2665      //@ ensures \result.syntax;
    2666      public/*@ non_null */TypeName parseExsuresTypeName(
    2667      /*@ non_null @*/EscPragmaLex l) {
    2668        return parseTypeName(l);
    2669      }
    2670
    2671      /**
    2672       * Parse a StoreRef
    2673       */
    2674      //@ requires l.m_in != null;
    2675      public Expr parseStoreRef(/*@ non_null @*/EscPragmaLex l) {
    2676        // StoreRefKeyword
    2677        int loc = l.startingLoc;
    2678        int t = l.ttype;
    2679        if (t == TagConstants.NOTHING) {
    2680          scanner.getNextToken();
    2681          return NothingExpr.make(loc);
    2682        } else if (t == TagConstants.NOT_SPECIFIED) {
    2683          scanner.getNextToken();
    2684          return NotSpecifiedExpr.make(loc);
    2685        } else if (t == TagConstants.EVERYTHING) {
    2686          scanner.getNextToken();
    2687          return EverythingExpr.make(loc);
    2688        } else if (t == TagConstants.PRIVATE_DATA) {
    2689          // PRIVATE_DATA recognized and discarded, unclear semantics (kiniry)
    2690          // FIXME
    2691          l.getNextToken();
    2692          return null; // FIXME
    2693        } else if (t == TagConstants.INFORMALPRED_TOKEN) {
    2694          // InformalDescription
    2695          l.getNextToken();
    2696          return null; // FIXME
    2697        }
    2698        // StoreRefExpr
    2699        return parseExpression(l);
    2700        //return parseStoreRefExpr(l);
    2701      }
    2702
    2703      /**
    2704       * Parse a StoreRefExpr
    2705       */
    2706      //@ requires l.m_in != null;
    2707      public Expr parseStoreRefExpr(/*@ non_null @*/EscPragmaLex l) {
    2708        int loc = l.startingLoc;
    2709        Name n = null;
    2710        Expr e = null;
    2711        ObjectDesignator od = null;
    2712        Expr result = null;
    2713        if (l.ttype == TagConstants.IDENT) {
    2714          if (l.lookahead(1) == TagConstants.LPAREN) {
    2715            result = parsePrimaryExpression(l);
    2716          } else if (l.lookahead(1) != TagConstants.FIELD) {
    2717            result = parseExpression(l);
    2718          } else {
    2719            n = parseName(l);
    2720            result = AmbiguousVariableAccess.make(n);
    2721          }
    2722        } else if (l.ttype == TagConstants.THIS) {
    2723          if (l.lookahead(1) != TagConstants.FIELD) {
    2724            result = parseExpression(l);
    2725          } else {
    2726            result = ThisExpr.make(null, loc);
    2727            l.getNextToken();
    2728          }
    2729        } else if (l.ttype == TagConstants.SUPER) {
    2730          l.getNextToken();
    2731          od = SuperObjectDesignator.make(l.startingLoc, loc);
    2732        } else {
    2733          ErrorSet.error(l.startingLoc,
    2734              "Expected an identifier, this or super here");
    2735          return null;
    2736        }
    2737        while (true) {
    2738          // StoreRefNameSuffix ::= '.' Idn | '.' 'this' | '.' '*' | '[' SpecArrayRefExpr ']'
    2739          if (l.ttype == TagConstants.FIELD) {
    2740            int locDot = l.startingLoc;
    2741            l.getNextToken();
    2742            if (l.ttype == TagConstants.IDENT) {
    2743              if (od == null) {
    2744                od = ExprObjectDesignator.make(locDot, result);
    2745              }
    2746              result = FieldAccess.make(od, l.identifierVal, l.startingLoc);
    2747              od = null;
    2748            } else if (l.ttype == TagConstants.THIS) {
    2749              // Will we ever get here?
    2750              ErrorSet.error(l.startingLoc, "Syntax not yet supported - StoreRefB");
    2751              // FIXME
    2752              return null;
    2753            } else if (l.ttype == TagConstants.STAR) {
    2754              result = WildRefExpr.make(result, od);
    2755              od = null;
    2756              // FIXME - no more after this
    2757            } else {
    2758              ErrorSet.error(scanner.startingLoc,
    2759                  "storage reference name suffix must be an "
    2760                      + "identifier or 'this' or '*' ");
    2761              return null;
    2762            }
    2763            l.getNextToken();
    2764          } else if (l.ttype == TagConstants.LSQBRACKET) {
    2765            int locOpenBracket = l.startingLoc;
    2766            l.getNextToken();
    2767            // SpecArrayRefExpr
    2768            if (l.ttype == TagConstants.STAR) {
    2769              l.getNextToken();
    2770              result = ArrayRangeRefExpr.make(locOpenBracket, result, null, null);
    2771            } else {
    2772              Expr firstExpr = parsePrimaryExpression(l);
    2773              if (l.ttype == TagConstants.DOTDOT) {
    2774                l.getNextToken();
    2775                Expr secondExpr = parsePrimaryExpression(l);
    2776                result = ArrayRangeRefExpr.make(locOpenBracket, result, firstExpr,
    2777                    secondExpr);
    2778              } else {
    2779                // Simple array reference
    2780                int locCloseBracket = l.startingLoc;
    2781                result = ArrayRefExpr.make(result, firstExpr, locOpenBracket,
    2782                    locCloseBracket);
    2783              }
    2784            }
    2785            if (l.ttype != TagConstants.RSQBRACKET) {
    2786              ErrorSet.error(l.startingLoc, "Expected a ]");
    2787              return null;
    2788            }
    2789            l.getNextToken(); // skip the [
    2790          } else {
    2791            break;
    2792          }
    2793        }
    2794        return result;
    2795      }
    2796
    2797      //@ spec_public
    2798      protected int modifiers = Modifiers.NONE;
    2799
    2800      // Adds any Java modifiers found into the 'modifiers' field
    2801      public void parseJavaModifiers() {
    2802        int i;
    2803        do {
    2804          i = getJavaModifier(scanner, modifiers);
    2805          modifiers |= i;
    2806        } while (i != 0);
    2807      }
    2808
    2809      private boolean argListInAnnotation = false;
    2810
    2811      public FormalParaDeclVec parseFormalParameterList(Lex l) {
    2812        /* Should be on LPAREN */
    2813        if (l.ttype != TagConstants.LPAREN)
    2814            fail(l.startingLoc, "Expected open paren");
    2815        if (l.lookahead(1) == TagConstants.RPAREN) {
    2816          // Empty parameter list
    2817          expect(l, TagConstants.LPAREN);
    2818          expect(l, TagConstants.RPAREN);
    2819          return FormalParaDeclVec.make();
    2820        } else {
    2821          seqFormalParaDecl.push();
    2822          while (l.ttype != TagConstants.RPAREN) {
    2823            l.getNextToken(); // swallow COMMA
    2824            int modifiers = parseModifiers(l);
    2825            ModifierPragmaVec modifierPragmas = this.modifierPragmas;
    2826            int typeLoc = l.startingLoc;
    2827            Type type = parseType(l);
    2828            Identifier id = null;
    2829            if (argListInAnnotation
    2830                && type instanceof TypeName
    2831                && ((TypeName)type).name.printName().equals("non_null")
    2832                && !(l.ttype == TagConstants.IDENT && (l.lookahead(1) == TagConstants.COMMA || l
    2833                    .lookahead(1) == TagConstants.RPAREN))) {
    2834              // The non_null is a modifier, not a type
    2835              // [ A model method or constructor does not need to
    2836              //   enclose the 'non_null' in annotation markers; hence
    2837              //   we can have either 'non_null i' in which non_null
    2838              //   is a type or 'non_null int i' in which non_null is
    2839              //   a modifier.]
    2840              type = parseType(l);
    2841              if (modifierPragmas == null)
    2842                  modifierPragmas = ModifierPragmaVec.make();
    2843              modifierPragmas.addElement(SimpleModifierPragma.make(
    2844                  TagConstants.NON_NULL, typeLoc));
    2845            }
    2846            int locId = l.startingLoc;
    2847            id = parseIdentifier(l);
    2848            type = parseBracketPairs(l, type);
    2849            modifierPragmas = parseMoreModifierPragmas(l, modifierPragmas);
    2850            seqFormalParaDecl.addElement(FormalParaDecl.make(modifiers,
    2851                modifierPragmas, id, type, locId));
    2852            if (l.ttype != TagConstants.RPAREN && l.ttype != TagConstants.COMMA)
    2853                fail(l.startingLoc, "Exprected comma or close paren");
    2854          }
    2855          expect(l, TagConstants.RPAREN);
    2856          return FormalParaDeclVec.popFromStackVector(seqFormalParaDecl);
    2857        }
    2858      }
    2859
    2860      /* This routine is the beginning of parsing model and ghost
    2861       declarations.  Model types declarations are in particular problematic.
    2862       The implementation here uses the Java parsing infrastructure to
    2863       parse a type declaration, but within a model class ESC keywords are
    2864       not enclosed in annotation comment symbols.  Hence the parsing does
    2865       not work the same.  Plus the ESC design in which annotation pragmas
    2866       are returned as tokens from the lexer (including a complete model
    2867       class), without any context, make the implementation of handling
    2868       model types rather messy.  However, I'm not about to start a complete
    2869       refactoring of the way that ESC designed pragmas into Java right now.
    2870       */
    2871
    2872      /** Parses a declaration that appears in a ghost or model annotation -
    2873       can be a ghost or model field or a model method or constructor.
    2874       @return true if a terminating semicolon is expected next
    2875       */
    2876      public boolean parseDeclaration(Token dst, int loc, int kwtag) {
    2877        try {
    2878
    2879          int tag = savedGhostModelPragma.getTag();
    2880          dst.ttype = TagConstants.TYPEDECLELEMPRAGMA;
    2881
    2882          // Get any modifier pragmas already declared
    2883          ModifierPragmaVec modifierPragmas = ModifierPragmaVec.make();
    2884
    2885          // Parse the type name and brackets associated with it
    2886          int locType = scanner.startingLoc;
    2887          if (scanner.ttype == TagConstants.CLASS
    2888              || scanner.ttype == TagConstants.INTERFACE) {
    2889
    2890            savedGhostModelPragma = null;
    2891            return parseTypeDeclTail(dst, locType);
    2892          }
    2893          Type type = parseType(scanner);
    2894
    2895          if (scanner.ttype == TagConstants.LPAREN) {
    2896            if (!(kwtag == 0 || kwtag == TagConstants.CONSTRUCTOR)) {
    2897              ErrorSet.caution("A constructor declaration is encountered after a "
    2898                  + TagConstants.toString(kwtag) + " keyword");
    2899            }
    2900            if (tag == TagConstants.GHOST) {
    2901              ErrorSet.error(savedGhostModelPragma.getStartLoc(),
    2902                  "A constructor may not be declared ghost");
    2903            }
    2904            return parseConstructorDeclTail(dst, loc, type, locType,
    2905                modifierPragmas);
    2906            // Note the finally block
    2907          }
    2908
    2909          // Parse the id
    2910          int locId = scanner.startingLoc;
    2911          Identifier id = parseIdentifier(scanner);
    2912
    2913          // Now we decide whether this is a field or method.
    2914          // A field will have either an = or ; or , at this point
    2915          // A method will have a (
    2916
    2917          if (scanner.ttype == TagConstants.LPAREN) {
    2918            if (!(kwtag == 0 || kwtag == TagConstants.METHOD)) {
    2919              ErrorSet.caution("A method declaration is encountered after a "
    2920                  + TagConstants.toString(kwtag) + " keyword");
    2921            }
    2922            if (tag == TagConstants.GHOST) {
    2923              ErrorSet.error(savedGhostModelPragma.getStartLoc(),
    2924                  "A method may not be declared ghost");
    2925            }
    2926            return parseMethodDeclTail(dst, loc, type, locType, id, locId,
    2927                modifierPragmas);
    2928            // Note the finally block
    2929          } else {
    2930            if (!(kwtag == 0 || kwtag == TagConstants.FIELDKW)) {
    2931              ErrorSet.caution("A field declaration is encountered after a "
    2932                  + TagConstants.toString(kwtag) + " keyword");
    2933            }
    2934            return parseFieldDeclTail(dst, loc, locId, type, id, modifierPragmas);
    2935            // Note the finally block
    2936          }
    2937        } finally {
    2938          inProcessTag = NEXT_TOKEN_STARTS_NEW_PRAGMA;
    2939          savedGhostModelPragma = null;
    2940          modifiers = Modifiers.NONE;
    2941        }
    2942      }
    2943
    2944      // These do not nest properly - there may well be problems with a routine in a model class within a routine - FIXME - really need a complete overhaul of the parsing design to accommodate model methods and classes.
    2945      boolean inModelType = false;
    2946
    2947      boolean inModelRoutine = false;
    2948
    2949      public boolean parseTypeDeclTail(Token dst, int loc) {
    2950        inModelType = true;
    2951        try {
    2952          int modifiers = this.modifiers;
    2953          TypeDecl td = parseTypeDeclaration(scanner, false);
    2954          // Should use false for specOnly only if already
    2955          // parsing a file for which specOnly=false FIXME
    2956          dst.auxVal = ModelTypePragma.make(td, loc);
    2957        } finally {
    2958          inModelType = false;
    2959        }
    2960        return false; // No semicolon after a type declaration
    2961      }
    2962
    2963      protected void addStmt(Lex l) {
    2964        ModifierPragmaVec mpv = null;
    2965        if (inModelType || inModelRoutine) { // FIXME also in model routine?
    2966          // FIXME what about modifiers and pmodifiers (e.g. non_null) on ghost decls
    2967          OUTER: while (true) {
    2968            if (l.ttype == TagConstants.IDENT || l.ttype == TagConstants.ASSERT) {
    2969              int tag = l.ttype == TagConstants.IDENT ? TagConstants
    2970                  .fromIdentifier(l.identifierVal) : l.ttype;
    2971              if (tag != TagConstants.NULL) {
    2972                Token dst = new Token();
    2973                if (getNextPragmaHelper(dst))
    2974                    do {
    2975                      if (dst.ttype != TagConstants.NULL) {
    2976                        if (dst.ttype == TagConstants.STMTPRAGMA) {
    2977                          seqStmt.addElement((Stmt)dst.auxVal);
    2978                        } else if (dst.ttype == TagConstants.TYPEDECLELEMPRAGMA) {
    2979                          FieldDecl fd = isPragmaDecl(dst);
    2980                          if (fd != null) {
    2981                            LocalVarDecl d = LocalVarDecl.make(fd.modifiers,
    2982                                fd.pmodifiers, fd.id, fd.type, fd.locId, fd.init,
    2983                                fd.locAssignOp);
    2984                            seqStmt.addElement(VarDeclStmt.make(d));
    2985                          }
    2986                        } else if (dst.ttype == TagConstants.MODIFIERPRAGMA) {
    2987                          if (mpv == null) mpv = ModifierPragmaVec.make(1);
    2988                          mpv.addElement((ModifierPragma)dst.auxVal);
    2989                          continue OUTER;
    2990                        } else {
    2991                          System.out.println("UNKOWN PRAGMA TYPE"); // FIXME
    2992                        }
    2993                      }
    2994                    } while (getPragma(dst));
    2995                return;
    2996              }
    2997            }
    2998            break;
    2999          }
    3000        }
    3001        super.addStmt(l);
    3002        if (mpv != null) {
    3003          Object o = seqStmt.elementAt(seqStmt.size() - 1);
    3004          if (o instanceof VarDeclStmt) {
    3005            ((VarDeclStmt)o).decl.pmodifiers = mpv; // FIXME ? append
    3006          } else {
    3007            System.out.println("MPV " + o.getClass());
    3008          }
    3009        }
    3010      }
    3011
    3012      protected TypeDeclElem parseTypeDeclElemIntoSeqTDE(Lex l, int keyword,
    3013          Identifier containerId, boolean specOnly) {
    3014
    3015        ModifierPragmaVec mpv = ModifierPragmaVec.make();
    3016        ModifierPragma ghostModel = null;
    3017        if (inModelType) {
    3018          OUTER: while (true) {
    3019            if (l.ttype == TagConstants.RBRACE) return null;
    3020            if (l.ttype == TagConstants.EOF) return null;
    3021            modifiers = Modifiers.NONE;
    3022            int k = -1;
    3023            while (true) {
    3024              ++k;
    3025              int t = l.lookahead(k);
    3026              if (isJavaModifier(t)) continue;
    3027              if (t == TagConstants.OPENPRAGMA || t == TagConstants.CLOSEPRAGMA) {
    3028                // skip
    3029              } else if (t == TagConstants.EOF) {
    3030                break OUTER;
    3031              } else {
    3032                if (t != TagConstants.IDENT) break OUTER;
    3033                Token tok = l.lookaheadToken(k);
    3034                int tag = TagConstants.fromIdentifier(tok.identifierVal);
    3035                if (tag == TagConstants.NULL) break OUTER;
    3036                if (AnnotationHandler.NestedPragmaParser.isRoutineModifier(tag)) {
    3037                  tok.ttype = TagConstants.MODIFIERPRAGMA;
    3038                  tok.auxVal = SimpleModifierPragma.make(tag, tok.startingLoc);
    3039                  if (tag == TagConstants.GHOST || tag == TagConstants.MODEL)
    3040                      ghostModel = (ModifierPragma)tok.auxVal;
    3041                  continue;
    3042                }
    3043              }
    3044              // Have decided that we have a pragma coming
    3045              // so we parse it.  Otherwise we have already
    3046              // broken out of the loop to parse the next sequence
    3047              // of tokens using the code in the super class.
    3048              Token dst = new Token();
    3049              if (getNextPragmaHelper(dst))
    3050                  do {
    3051                    if (dst.ttype == TagConstants.TYPEDECLELEMPRAGMA) {
    3052                      seqTypeDeclElem.addElement(dst.auxVal);
    3053                    } else if (dst.ttype == TagConstants.MODIFIERPRAGMA) {
    3054                      mpv.addElement((ModifierPragma)dst.auxVal);
    3055                    } else if (dst.ttype == TagConstants.LEXICALPRAGMA) {
    3056                      l.lexicalPragmas.addElement((LexicalPragma)dst.auxVal);
    3057                    } else if (dst.ttype == TagConstants.EOF
    3058                        || dst.ttype == TagConstants.NULL) {
    3059                      // skip
    3060                    } else {
    3061                      System.out.println("UNEXPECTED PRAGMA "
    3062                          + TagConstants.toString(dst.ttype));
    3063                    }
    3064                  } while (getPragma(dst));
    3065              break;
    3066            }
    3067          }
    3068        }
    3069
    3070        TypeDeclElem result = super.parseTypeDeclElemIntoSeqTDE(l, keyword,
    3071            containerId, specOnly);
    3072        if (mpv.size() != 0) {
    3073          if (result instanceof TypeDeclElemPragma) {
    3074            ((TypeDeclElemPragma)result).decorate(mpv);
    3075          } else if (result instanceof MethodDecl) {
    3076            MethodDecl rd =(MethodDecl)result;
    3077            if (rd.pmodifiers != null) mpv.append(rd.pmodifiers);
    3078            rd.pmodifiers = mpv;
    3079          } else if (result instanceof ConstructorDecl) {
    3080            ConstructorDecl rd =(ConstructorDecl)result;
    3081            if (rd.pmodifiers != null) mpv.append(rd.pmodifiers);
    3082            rd.pmodifiers = mpv;
    3083          } else {
    3084            // FIXME
    3085            System.out.println("MODS FOR " + result.getClass());
    3086          }
    3087        }
    3088        if (ghostModel != null) {
    3089          int p = seqTypeDeclElem.size();
    3090          while (--p >= 0) {
    3091            Object o = seqTypeDeclElem.elementAt(p);
    3092            if (o instanceof FieldDecl) {
    3093              FieldDecl f = (FieldDecl)o;
    3094              if (Utils.findModifierPragma(f.pmodifiers, TagConstants.GHOST) != null) {
    3095                seqTypeDeclElem.setElementAt(GhostDeclPragma.make(f, ghostModel
    3096                    .getStartLoc()), p);
    3097              } else if (Utils.findModifierPragma(f.pmodifiers, TagConstants.MODEL) != null) {
    3098                seqTypeDeclElem.setElementAt(ModelDeclPragma.make(f, ghostModel
    3099                    .getStartLoc()), p);
    3100              } else {
    3101                break;
    3102              }
    3103            } else
    3104              break;
    3105          }
    3106        }
    3107        return result;
    3108      }
    3109
    3110      protected TypeDecl parseTypeDeclTail(Lex l, boolean specOnly, int loc,
    3111          int modifiers, ModifierPragmaVec modifierPragmas) {
    3112        int keyword = l.ttype;
    3113        if (keyword == TagConstants.CLASS || keyword == TagConstants.INTERFACE)
    3114            return super.parseTypeDeclTail(l, specOnly, loc, modifiers,
    3115                modifierPragmas);
    3116        if (l.ttype == TagConstants.TYPEDECLELEMPRAGMA) {
    3117          TypeDeclElemPragma tde = (TypeDeclElemPragma)l.auxVal;
    3118          System.out.println("MC " + TagConstants.toString(tde.getTag()));
    3119        }
    3120        fail(l.startingLoc, "expected 'class' or 'interface'");
    3121        return null;
    3122      }
    3123
    3124      public boolean parseFieldDeclTail(Token dst, int loc, int locId, Type type,
    3125          Identifier id, ModifierPragmaVec modifierPragmas) {
    3126        int tag = savedGhostModelPragma.getTag();
    3127
    3128        // Parse any additional brackets and add them to the type
    3129        Type vartype = parseBracketPairs(scanner, type);
    3130
    3131        // Get the initializer if there is one
    3132        VarInit init = null;
    3133        int locAssignOp = Location.NULL;
    3134        if (scanner.ttype == TagConstants.ASSIGN) {
    3135          locAssignOp = scanner.startingLoc;
    3136          scanner.getNextToken();
    3137          init = parseVariableInitializer(scanner, false);
    3138          if (tag == TagConstants.MODEL) {
    3139            ErrorSet.error(locAssignOp, "Model fields may not be initialized");
    3140            init = null;
    3141          }
    3142        }
    3143        ModifierPragmaVec allModifierPragmas;
    3144        if (scanner.ttype == TagConstants.MODIFIERPRAGMA) {
    3145          // FIXME - only need this for old ESC/Java pragmas
    3146          // but some old tests rely on it
    3147          allModifierPragmas = modifierPragmas.copy();
    3148          allModifierPragmas = parseMoreModifierPragmas(scanner, allModifierPragmas);
    3149        } else {
    3150          allModifierPragmas = modifierPragmas;
    3151        }
    3152
    3153        FieldDecl decl = FieldDecl.make(modifiers, allModifierPragmas, id, vartype,
    3154            locId, init, locAssignOp);
    3155        Object pragma = null;
    3156        if (tag == TagConstants.GHOST) {
    3157          pragma = GhostDeclPragma.make(decl, loc);
    3158        } else if (tag == TagConstants.MODEL) {
    3159          pragma = ModelDeclPragma.make(decl, loc);
    3160        }
    3161        dst.ttype = TagConstants.NULL;
    3162        savePragma(loc, TagConstants.TYPEDECLELEMPRAGMA, pragma);
    3163
    3164        while (scanner.ttype == TagConstants.COMMA) {
    3165          scanner.getNextToken(); // skip comma
    3166          locId = scanner.startingLoc;
    3167          id = parseIdentifier(scanner);
    3168          Type vartype2 = parseBracketPairs(scanner, type);
    3169
    3170          init = null;
    3171          locAssignOp = Location.NULL;
    3172          if (scanner.ttype == TagConstants.ASSIGN) {
    3173            locAssignOp = scanner.startingLoc;
    3174            scanner.getNextToken();
    3175            init = parseVariableInitializer(scanner, false);
    3176          }
    3177          if (scanner.ttype == TagConstants.MODIFIERPRAGMA) {
    3178            // FIXME - only need this for old ESC/Java pragmas
    3179            // but some old tests rely on it
    3180            allModifierPragmas = modifierPragmas.copy();
    3181            allModifierPragmas = parseMoreModifierPragmas(scanner,
    3182                allModifierPragmas);
    3183          } else {
    3184            allModifierPragmas = modifierPragmas;
    3185          }
    3186          decl = FieldDecl.make(modifiers, allModifierPragmas, id, vartype2, locId,
    3187              init, locAssignOp);
    3188          if (tag == TagConstants.GHOST) {
    3189            pragma = GhostDeclPragma.make(decl, locId);
    3190          } else if (tag == TagConstants.MODEL) {
    3191            pragma = ModelDeclPragma.make(decl, locId);
    3192          }
    3193          savePragma(loc, TagConstants.TYPEDECLELEMPRAGMA, pragma);
    3194
    3195        }
    3196        if (scanner.ttype == TagConstants.SEMICOLON) {
    3197          // The following is an unfortunate hack to the overall
    3198          // design caused by the fact that the in and maps clauses
    3199          // *follow* the field declarations to which they belong.
    3200          // All other modifiers precede the declaration.  The
    3201          // Javafe parser does not like this, so we have to do
    3202          // some special lookahead here to make the right associations.
    3203          savedGhostModelPragma = null; // Need this so the calls of
    3204          // getNextPragma below do not fail
    3205          Token temp = new Token();
    3206          scanner.getNextToken();
    3207          while (true) {
    3208            // FIXME - when there are multiple FieldDecls in one declaration,
    3209            // an in pragma applies to them all and a maps pragma applies to
    3210            // the ones with a matching leading identifier.  This is not implemented
    3211            // here.
    3212            // FIXME - the following code is another reason why the handling of pragmas
    3213            // should be totally refactored here and within javafe.
    3214            if (scanner.ttype == TagConstants.IDENT
    3215                && (scanner.identifierVal.toString().equals("in") || scanner.identifierVal
    3216                    .toString().equals("in_redundantly"))) {
    3217              boolean isRed = !scanner.identifierVal.toString().equals("in");
    3218              scanner.getNextToken(); // skip the in token
    3219
    3220              boolean first = true;
    3221              boolean more;
    3222              do {
    3223                more = parseInPragmas(TagConstants.IN, scanner.startingLoc, temp,
    3224                    first);
    3225                if (more) {
    3226                  if (decl.pmodifiers == null)
    3227                      decl.pmodifiers = ModifierPragmaVec.make();
    3228                  decl.pmodifiers.addElement((ModifierPragma)temp.auxVal);
    3229                }
    3230                first = false;
    3231              } while (more);
    3232              expect(scanner, TagConstants.SEMICOLON);
    3233              continue;
    3234            }
    3235            if (scanner.ttype == TagConstants.IDENT
    3236                && (scanner.identifierVal.toString().equals("maps") || scanner.identifierVal
    3237                    .toString().equals("maps_redundantly"))) {
    3238              boolean isRed = !scanner.identifierVal.toString().equals("maps");
    3239              scanner.getNextToken(); // skip the maps token
    3240              // Already parsed something - should be an identifier
    3241              //System.out.println("MAPPING " + scanner.identifierVal.toString());
    3242              Identifier idd = scanner.identifierVal;
    3243              Expr mapsod = parseMapsMemberFieldRef(scanner);
    3244              if (mapsod == null) {
    3245                // already wrote an error message
    3246                eatThroughSemiColon();
    3247              } else if (scanner.identifierVal == null
    3248                  || !scanner.identifierVal.toString().equals("\\into")) {
    3249                ErrorSet.error(scanner.startingLoc,
    3250                    "Expected \\into in the maps clause here");
    3251                eatThroughSemiColon();
    3252              } else {
    3253                scanner.getNextToken(); // skip \into
    3254                LinkedList groups = parseGroupList(); // parses through the semicolon
    3255                Iterator ig = groups.iterator();
    3256                while (ig.hasNext()) {
    3257                  Expr e = (Expr)ig.next();
    3258                  MapsExprModifierPragma ppragma = MapsExprModifierPragma.make(
    3259                      TagConstants.MAPS, idd, mapsod, loc, e);
    3260                  if (isRed) ppragma.setRedundant(true);
    3261                  if (decl.pmodifiers == null)
    3262                      decl.pmodifiers = ModifierPragmaVec.make();
    3263                  decl.pmodifiers.addElement(ppragma);
    3264                }
    3265                continue;
    3266              }
    3267            }
    3268            if (scanner.ttype == TagConstants.POSTMODIFIERPRAGMA) {
    3269              decl.pmodifiers.addElement((ModifierPragma)temp.auxVal);
    3270              continue;
    3271            }
    3272            break;
    3273          }
    3274          return false; // already ate the semicolon
    3275        }
    3276        return true; // semicolon still to eat
    3277      }
    3278
    3279      public boolean parseConstructorDeclTail(Token dst, int loc, Type type,
    3280          int locType, ModifierPragmaVec modifierPragmas) {
    3281        // Must be a model constructor
    3282        inModelRoutine = true;
    3283        savedGhostModelPragma = null;
    3284        try {
    3285          SimpleName id = null;
    3286          if (!(type instanceof TypeName)) {
    3287            ErrorSet
    3288                .error(
    3289                    type.getStartLoc(),
    3290                    "The type name in a constructor declaration may not be a primitive or array type");
    3291          } else {
    3292            Name name = ((TypeName)type).name;
    3293            if (!(name instanceof SimpleName)) {
    3294              ErrorSet
    3295                  .error(
    3296                      name.getStartLoc(),
    3297                      "The type name in a constructor must be a simple name that matches the name of the enclosing type");
    3298            } else {
    3299              id = (SimpleName)name;
    3300            }
    3301          }
    3302          FormalParaDeclVec args;
    3303          argListInAnnotation = true;
    3304          try {
    3305            args = parseFormalParameterList(scanner);
    3306          } finally {
    3307            argListInAnnotation = false;
    3308          }
    3309          int locThrowsKeyword;
    3310          if (scanner.ttype == TagConstants.THROWS) {
    3311            locThrowsKeyword = scanner.startingLoc;
    3312          } else {
    3313            locThrowsKeyword = Location.NULL;
    3314          }
    3315          TypeNameVec raises = parseTypeNames(scanner, TagConstants.THROWS);
    3316          modifierPragmas = parseMoreModifierPragmas(scanner, modifierPragmas);
    3317          int locOpenBrace = Location.NULL;
    3318          BlockStmt body = null;
    3319          if (scanner.ttype == TagConstants.SEMICOLON) {
    3320            scanner.getNextToken(); // eats semicolon
    3321          } else if (scanner.ttype == TagConstants.LBRACE) {
    3322            locOpenBrace = scanner.startingLoc;
    3323            body = parseBlock(scanner, false);
    3324            // To skip the body, use true in the call above.
    3325            // body will be non-null but have 0 statements
    3326          } else {
    3327            ErrorSet.fatal(scanner.startingLoc, "Invalid syntax - expected a "
    3328                + "semicolon or the start of a constructor body, " + "encountered "
    3329                + TagConstants.toString(scanner.ttype));
    3330          }
    3331          ConstructorDecl md = ConstructorDecl.make(modifiers, modifierPragmas,
    3332              null, args, raises, body, locOpenBrace, loc, locType,
    3333              locThrowsKeyword);
    3334          ModelConstructorDeclPragma mcd = ModelConstructorDeclPragma.make(md, loc,
    3335              id);
    3336          dst.auxVal = mcd;
    3337          // Semantic checks in AnnotationHandler verify that the
    3338          // id matches the enclosing type, since the enclosing type
    3339          // is not available here.
    3340          if (id == null) {
    3341            savedGhostModelPragma = null;
    3342            modifiers = Modifiers.NONE;
    3343            return getNextPragmaHelper(dst);
    3344          }
    3345        } finally {
    3346          inModelRoutine = false;
    3347        }
    3348        return false; // No semicolon, or it is already eaten
    3349      }
    3350
    3351      public boolean parseMethodDeclTail(Token dst, int loc, Type type,
    3352          int locType, Identifier id, int locId, ModifierPragmaVec modifierPragmas) {
    3353
    3354        // Must be a model method
    3355        inModelRoutine = true;
    3356        savedGhostModelPragma = null;
    3357        try {
    3358          FormalParaDeclVec args;
    3359          argListInAnnotation = true;
    3360          try {
    3361            args = parseFormalParameterList(scanner);
    3362          } finally {
    3363            argListInAnnotation = false;
    3364          }
    3365
    3366          int locThrowsKeyword;
    3367          if (scanner.ttype == TagConstants.THROWS) {
    3368            locThrowsKeyword = scanner.startingLoc;
    3369          } else {
    3370            locThrowsKeyword = Location.NULL;
    3371          }
    3372          TypeNameVec raises = parseTypeNames(scanner, TagConstants.THROWS);
    3373
    3374          modifierPragmas = parseMoreModifierPragmas(scanner, modifierPragmas);
    3375          int locOpenBrace = Location.NULL;
    3376          BlockStmt body = null;
    3377          int modifiers = this.modifiers;
    3378          this.modifiers = Modifiers.NONE;
    3379          if (scanner.ttype == TagConstants.SEMICOLON) {
    3380            scanner.getNextToken(); // eats semicolon
    3381          } else if (scanner.ttype == TagConstants.LBRACE) {
    3382            locOpenBrace = scanner.startingLoc;
    3383            body = parseBlock(scanner, false);
    3384            // To skip the body, use true in the call above.
    3385            // body will be non-null but have 0 statements
    3386            // FIXME - set in accordance with specOnly; constructor also
    3387          } else {
    3388            ErrorSet.fatal(scanner.startingLoc, "Invalid syntax - expected a "
    3389                + "semicolon or the start of a method body, " + "encountered "
    3390                + TagConstants.toString(scanner.ttype));
    3391          }
    3392          MethodDecl md = MethodDecl.make(modifiers, modifierPragmas, null, args,
    3393              raises, body, locOpenBrace, loc, locId, locThrowsKeyword, id, type,
    3394              locType);
    3395          dst.auxVal = ModelMethodDeclPragma.make(md, loc);
    3396        } finally {
    3397          inModelRoutine = false;
    3398        }
    3399        return false; // No semicolon, or it is already eaten
    3400      }
    3401
    3402      public FieldDecl isPragmaDecl(Token l) {
    3403        if (l.auxVal == null) return null;
    3404        TypeDeclElemPragma smp = (TypeDeclElemPragma)l.auxVal;
    3405        int loc = smp.getStartLoc();
    3406        int tag = smp.getTag();
    3407        if (tag == TagConstants.MODELDECLPRAGMA) {
    3408          ModelDeclPragma mdp = (ModelDeclPragma)smp;
    3409          ModifierPragma mp = Utils.findModifierPragma(mdp.decl.pmodifiers,
    3410              TagConstants.MODEL);
    3411          ErrorSet.error(mp != null ? mp.getStartLoc() : loc,
    3412              "Model variables are not allowed here");
    3413          return null;
    3414        }
    3415        if (tag != TagConstants.GHOSTDECLPRAGMA) {
    3416          ErrorSet.error(loc, "Expected a local ghost declaration here");
    3417          return null;
    3418        }
    3419
    3420        GhostDeclPragma gd = (GhostDeclPragma)l.auxVal;
    3421        return gd.decl;
    3422      }
    3423
    3424      // Starting state is looking at the initial identifier
    3425      public Expr parseMapsMemberFieldRef(Lex scanner) {
    3426        Identifier startid = scanner.identifierVal;
    3427        Expr expr = AmbiguousVariableAccess.make(SimpleName.make(startid,
    3428            scanner.startingLoc));
    3429        scanner.getNextToken();
    3430        boolean foundSomething = false;
    3431        while (scanner.ttype == TagConstants.LSQBRACKET) {
    3432          int openLoc = scanner.startingLoc;
    3433          scanner.getNextToken();
    3434          if (scanner.ttype == TagConstants.STAR) {
    3435            scanner.getNextToken();
    3436            expr = ArrayRangeRefExpr.make(openLoc, expr, null, null);
    3437          } else {
    3438            Expr lo = parseExpression(scanner);
    3439            Expr hi = null;
    3440            if (scanner.ttype == TagConstants.DOTDOT) {
    3441              scanner.getNextToken();
    3442              hi = parseExpression(scanner);
    3443              expr = ArrayRangeRefExpr.make(openLoc, expr, lo, hi);
    3444            } else {
    3445              expr = ArrayRefExpr.make(expr, lo, openLoc, scanner.startingLoc);
    3446            }
    3447          }
    3448          if (scanner.ttype != TagConstants.RSQBRACKET) {
    3449            ErrorSet.error(scanner.startingLoc,
    3450                "Expected a ] here, matching the opening bracket", openLoc);
    3451          }
    3452          foundSomething = true;
    3453          scanner.getNextToken();
    3454        }
    3455
    3456        if (scanner.ttype == TagConstants.FIELD) { // the dot
    3457          int locDot = scanner.startingLoc;
    3458          scanner.getNextToken();
    3459          if (scanner.ttype == TagConstants.IDENT) {
    3460            expr = FieldAccess.make(ExprObjectDesignator.make(locDot, expr),
    3461                scanner.identifierVal, scanner.startingLoc);
    3462            scanner.getNextToken();
    3463          } else if (scanner.ttype == TagConstants.STAR) {
    3464            expr = WildRefExpr.make(expr, null);
    3465            scanner.getNextToken();
    3466          } else {
    3467            ErrorSet.error(scanner.startingLoc,
    3468                "Expected either a * or an identifier here");
    3469          }
    3470          foundSomething = true;
    3471
    3472        }
    3473        if (!foundSomething) {
    3474          ErrorSet.error(scanner.startingLoc,
    3475              "Expected either a . or a [ in the maps field reference here");
    3476          return null;
    3477        }
    3478        return expr;
    3479      }
    3480
    3481      private boolean parseInPragmas(int tag, int loc, Token dst, boolean first) {
    3482        if (!first) {
    3483          if (scanner.ttype == TagConstants.SEMICOLON) return false;
    3484          if (scanner.ttype == TagConstants.COMMA) scanner.getNextToken(); // skip comma
    3485        }
    3486        int n = 0;
    3487        if (scanner.ttype == TagConstants.SUPER
    3488            || scanner.ttype == TagConstants.THIS) {
    3489          if (scanner.lookahead(1) != TagConstants.FIELD) {
    3490            ErrorSet.error(scanner.lookaheadToken(1).startingLoc,
    3491                "Expected a . after super");
    3492            eatThroughSemiColon();
    3493            return false;
    3494          }
    3495          n = 2;
    3496        }
    3497        if (scanner.lookahead(n) != TagConstants.IDENT) {
    3498          ErrorSet.error(scanner.lookaheadToken(n).startingLoc,
    3499              "Expected an identifier here");
    3500          eatThroughSemiColon();
    3501          return false;
    3502        }
    3503        int t = scanner.lookahead(n + 1);
    3504        if (t != TagConstants.COMMA && t != TagConstants.SEMICOLON) {
    3505          ErrorSet.error(scanner.lookaheadToken(n + 1).startingLoc,
    3506              "Expected a comma or semicolon here");
    3507          eatThroughSemiColon();
    3508          return false;
    3509        }
    3510        Expr e = parseExpression(scanner);
    3511        MapsExprModifierPragma pragma = MapsExprModifierPragma.make(TagConstants
    3512            .unRedundant(tag), null, null, loc, e);
    3513        if (TagConstants.isRedundant(tag)) pragma.setRedundant(true);
    3514        dst.startingLoc = loc;
    3515        dst.auxVal = pragma;
    3516        dst.ttype = TagConstants.POSTMODIFIERPRAGMA;
    3517        return true;
    3518      }
    3519
    3520      public LinkedList parseGroupList() {
    3521        LinkedList res = new LinkedList();
    3522        while (true) {
    3523          int n = 0;
    3524          if (scanner.ttype == TagConstants.SUPER
    3525              || scanner.ttype == TagConstants.THIS) {
    3526            if (scanner.lookahead(1) != TagConstants.FIELD) {
    3527              ErrorSet.error(scanner.lookaheadToken(1).startingLoc,
    3528                  "Expected a . after super");
    3529              eatThroughSemiColon();
    3530              return res;
    3531            }
    3532            n = 2;
    3533          }
    3534          if (scanner.lookahead(n) != TagConstants.IDENT) {
    3535            ErrorSet.error(scanner.lookaheadToken(n).startingLoc,
    3536                "Expected an identifier here");
    3537            eatThroughSemiColon();
    3538            return res;
    3539          }
    3540          int t = scanner.lookahead(n + 1);
    3541          if (t != TagConstants.COMMA && t != TagConstants.SEMICOLON) {
    3542            ErrorSet.error(scanner.lookaheadToken(n + 1).startingLoc,
    3543                "Expected a comma or semicolon here");
    3544            eatThroughSemiColon();
    3545            return res;
    3546          }
    3547          Expr e = parseExpression(scanner);
    3548          res.add(e);
    3549          if (scanner.ttype != TagConstants.COMMA) break;
    3550          scanner.getNextToken(); // skip comma
    3551        }
    3552        // skip semicolon
    3553        if (scanner.ttype == TagConstants.SEMICOLON) scanner.getNextToken();
    3554        return res;
    3555      }
    3556
    3557    } // end of class EscPragmaParser
    3558
    3559    /*
    3560     * Local Variables:
    3561     * Mode: Java
    3562     * fill-column: 85
    3563     * End:
    3564     */