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    public class WhileStmt extends Stmt
024    {
025      public /*@ non_null @*/ Expr expr;
026    
027      public /*@ non_null @*/ Stmt stmt;
028    
029      //@ invariant loc != javafe.util.Location.NULL;
030      public int loc;
031    
032      //@ invariant locGuardOpenParen != javafe.util.Location.NULL;
033      public int locGuardOpenParen;
034    
035    
036      private void postCheck() {
037        int t = stmt.getTag();
038        Assert.notFalse(t != TagConstants.SWITCHLABEL       //@ nowarn Pre;
039                        && t != TagConstants.CONSTRUCTORINVOCATION
040                        && t != TagConstants.VARDECLSTMT);
041      }
042    
043      //@ public represents startLoc <- loc;
044      public /*@ pure @*/ int getStartLoc() { return loc; }
045      //@ also public normal_behavior
046      //@ ensures \result == stmt.getEndLoc();
047      public /*@ pure @*/ int getEndLoc() { return stmt.getEndLoc(); }
048    
049    
050    // Generated boilerplate constructors:
051    
052      //@ ensures this.expr == expr;
053      //@ ensures this.stmt == stmt;
054      //@ ensures this.loc == loc;
055      //@ ensures this.locGuardOpenParen == locGuardOpenParen;
056      protected WhileStmt(/*@ non_null @*/ Expr expr, /*@ non_null @*/ Stmt stmt, int loc, int locGuardOpenParen) {
057         super();
058         this.expr = expr;
059         this.stmt = stmt;
060         this.loc = loc;
061         this.locGuardOpenParen = locGuardOpenParen;
062      }
063    
064    // Generated boilerplate methods:
065    
066      public final int childCount() {
067         return 2;
068      }
069    
070      public final Object childAt(int index) {
071              /*throws IndexOutOfBoundsException*/
072         if (index < 0)
073            throw new IndexOutOfBoundsException("AST child index " + index);
074         int indexPre = index;
075    
076         int sz;
077    
078         if (index == 0) return this.expr;
079         else index--;
080    
081         if (index == 0) return this.stmt;
082         else index--;
083    
084         throw new IndexOutOfBoundsException("AST child index " + indexPre);
085      }   //@ nowarn Exception;
086    
087      public final /*@non_null*/String toString() {
088         return "[WhileStmt"
089            + " expr = " + this.expr
090            + " stmt = " + this.stmt
091            + " loc = " + this.loc
092            + " locGuardOpenParen = " + this.locGuardOpenParen
093            + "]";
094      }
095    
096      public final int getTag() {
097         return TagConstants.WHILESTMT;
098      }
099    
100      public final void accept(Visitor v) { v.visitWhileStmt(this); }
101    
102      public final Object accept(VisitorArgResult v, Object o) {return v.visitWhileStmt(this, o); }
103    
104      public void check() {
105         super.check();
106         this.expr.check();
107         this.stmt.check();
108         postCheck();
109      }
110    
111      //@ requires loc != javafe.util.Location.NULL;
112      //@ requires locGuardOpenParen != javafe.util.Location.NULL;
113      //@ ensures \result != null;
114      public static WhileStmt make(/*@ non_null @*/ Expr expr, /*@ non_null @*/ Stmt stmt, int loc, int locGuardOpenParen) {
115         WhileStmt result = new WhileStmt(expr, stmt, loc, locGuardOpenParen);
116         return result;
117      }
118    }