001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 /* IF THIS IS A JAVA FILE, DO NOT EDIT IT! 004 005 Most Java files in this directory which are part of the Javafe AST 006 are automatically generated using the astgen comment (see 007 ESCTools/Javafe/astgen) from the input file 'hierarchy.h'. If you 008 wish to modify AST classes or introduce new ones, modify 009 'hierarchy.j.' 010 */ 011 012 package javafe.ast; 013 014 import javafe.util.Assert; 015 import javafe.util.Location; 016 import javafe.util.ErrorSet; 017 018 // Convention: unless otherwise noted, integer fields named "loc" refer 019 // to the location of the first character of the syntactic unit 020 021 022 /** Represents a ForStatement. 023 * 024 * The ForInit part of a ForStatement is either a StatementExpressionList 025 * or a LocalVariableDeclaration. Both alternatives are represented here 026 * by a Stmt sequence. 027 * Note that our Stmt class corresponds to a BlockStatement syntactic unit, 028 * so <code>forInit</code> can contain variable declarations. 029 */ 030 031 public class ForStmt extends Stmt 032 { 033 public /*@ non_null @*/ StmtVec forInit; 034 035 public /*@ non_null @*/ Expr test; 036 037 public /*@ non_null @*/ ExprVec forUpdate; 038 039 public /*@ non_null @*/ Stmt body; 040 041 //@ invariant loc != javafe.util.Location.NULL; 042 public int loc; 043 044 //@ invariant locFirstSemi != javafe.util.Location.NULL; 045 public int locFirstSemi; 046 047 048 private void postCheck() { 049 for(int i = 0; i < forInit.size(); i++) { 050 int t = forInit.elementAt(i).getTag(); 051 Assert.notFalse(t != TagConstants.SWITCHLABEL //@ nowarn Pre; 052 && t != TagConstants.CONSTRUCTORINVOCATION); 053 // Could have a stronger invariant here... 054 } 055 // Invariants on forUpdate??... 056 int t = body.getTag(); 057 Assert.notFalse(t != TagConstants.SWITCHLABEL //@ nowarn Pre; 058 && t != TagConstants.CONSTRUCTORINVOCATION 059 && t != TagConstants.VARDECLSTMT); 060 } 061 public int getStartLoc() { return loc; } 062 public int getEndLoc() { return body.getEndLoc(); } 063 064 065 // Generated boilerplate constructors: 066 067 /** 068 * Construct a raw ForStmt whose class invariant(s) have not 069 * yet been established. It is the caller's job to 070 * initialize the returned node's fields so that any 071 * class invariants hold. 072 */ 073 //@ requires I_will_establish_invariants_afterwards; 074 protected ForStmt() {} //@ nowarn Invariant,NonNullInit; 075 076 077 // Generated boilerplate methods: 078 079 public final int childCount() { 080 int sz = 0; 081 if (this.forInit != null) sz += this.forInit.size(); 082 if (this.forUpdate != null) sz += this.forUpdate.size(); 083 return sz + 2; 084 } 085 086 public final Object childAt(int index) { 087 /*throws IndexOutOfBoundsException*/ 088 if (index < 0) 089 throw new IndexOutOfBoundsException("AST child index " + index); 090 int indexPre = index; 091 092 int sz; 093 094 sz = (this.forInit == null ? 0 : this.forInit.size()); 095 if (0 <= index && index < sz) 096 return this.forInit.elementAt(index); 097 else index -= sz; 098 099 if (index == 0) return this.test; 100 else index--; 101 102 sz = (this.forUpdate == null ? 0 : this.forUpdate.size()); 103 if (0 <= index && index < sz) 104 return this.forUpdate.elementAt(index); 105 else index -= sz; 106 107 if (index == 0) return this.body; 108 else index--; 109 110 throw new IndexOutOfBoundsException("AST child index " + indexPre); 111 } //@ nowarn Exception; 112 113 public final String toString() { 114 return "[ForStmt" 115 + " forInit = " + this.forInit 116 + " test = " + this.test 117 + " forUpdate = " + this.forUpdate 118 + " body = " + this.body 119 + " loc = " + this.loc 120 + " locFirstSemi = " + this.locFirstSemi 121 + "]"; 122 } 123 124 public final int getTag() { 125 return TagConstants.FORSTMT; 126 } 127 128 public final void accept(Visitor v) { v.visitForStmt(this); } 129 130 public final Object accept(VisitorArgResult v, Object o) {return v.visitForStmt(this, o); } 131 132 public void check() { 133 super.check(); 134 for(int i = 0; i < this.forInit.size(); i++) 135 this.forInit.elementAt(i).check(); 136 this.test.check(); 137 for(int i = 0; i < this.forUpdate.size(); i++) 138 this.forUpdate.elementAt(i).check(); 139 this.body.check(); 140 postCheck(); 141 } 142 143 //@ requires loc != javafe.util.Location.NULL; 144 //@ requires locFirstSemi != javafe.util.Location.NULL; 145 //@ ensures \result != null; 146 public static ForStmt make(/*@ non_null @*/ StmtVec forInit, /*@ non_null @*/ Expr test, /*@ non_null @*/ ExprVec forUpdate, /*@ non_null @*/ Stmt body, int loc, int locFirstSemi) { 147 //@ set I_will_establish_invariants_afterwards = true; 148 ForStmt result = new ForStmt(); 149 result.forInit = forInit; 150 result.test = test; 151 result.forUpdate = forUpdate; 152 result.body = body; 153 result.loc = loc; 154 result.locFirstSemi = locFirstSemi; 155 return result; 156 } 157 }