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