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