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