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