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     */