    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    public class IfStmt extends Stmt
    023    {
    024      public /*@ non_null @*/ Expr expr;
    025
    026      public /*@ non_null @*/ Stmt thn;
    027
    028      public /*@ non_null @*/ Stmt els;
    029
    030      //@ invariant loc != javafe.util.Location.NULL;
    031      public int loc;
    032
    033
    034      private void postCheck() {
    035        int t = thn.getTag();
    036        Assert.notFalse(t != TagConstants.SWITCHLABEL       //@ nowarn Pre;
    037                        && t != TagConstants.CONSTRUCTORINVOCATION
    038                        && t != TagConstants.VARDECLSTMT);
    039        t = els.getTag();
    040        Assert.notFalse(t != TagConstants.SWITCHLABEL       //@ nowarn Pre;
    041                        && t != TagConstants.CONSTRUCTORINVOCATION
    042                        && t != TagConstants.VARDECLSTMT);
    043      }
    044      public int getStartLoc() { return loc; }
    045      public int getEndLoc() {
    046        int thenL = thn.getEndLoc();
    047        int elseL = els.getEndLoc();
    048        return Math.max(thenL, elseL);
    049      }
    050
    051
    052    // Generated boilerplate constructors:
    053
    054      /**
    055       * Construct a raw IfStmt whose class invariant(s) have not
    056       * yet been established.  It is the caller's job to
    057       * initialize the returned node's fields so that any
    058       * class invariants hold.
    059       */
    060      //@ requires I_will_establish_invariants_afterwards;
    061      protected IfStmt() {}    //@ nowarn Invariant,NonNullInit;
    062
    063
    064    // Generated boilerplate methods:
    065
    066      public final int childCount() {
    067         return 3;
    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.thn;
    082         else index--;
    083
    084         if (index == 0) return this.els;
    085         else index--;
    086
    087         throw new IndexOutOfBoundsException("AST child index " + indexPre);
    088      }   //@ nowarn Exception;
    089
    090      public final String toString() {
    091         return "[IfStmt"
    092            + " expr = " + this.expr
    093            + " thn = " + this.thn
    094            + " els = " + this.els
    095            + " loc = " + this.loc
    096            + "]";
    097      }
    098
    099      public final int getTag() {
    100         return TagConstants.IFSTMT;
    101      }
    102
    103      public final void accept(Visitor v) { v.visitIfStmt(this); }
    104
    105      public final Object accept(VisitorArgResult v, Object o) {return v.visitIfStmt(this, o); }
    106
    107      public void check() {
    108         super.check();
    109         this.expr.check();
    110         this.thn.check();
    111         this.els.check();
    112         postCheck();
    113      }
    114
    115      //@ requires loc != javafe.util.Location.NULL;
    116      //@ ensures \result != null;
    117      public static IfStmt make(/*@ non_null @*/ Expr expr, /*@ non_null @*/ Stmt thn, /*@ non_null @*/ Stmt els, int loc) {
    118         //@ set I_will_establish_invariants_afterwards = true;
    119         IfStmt result = new IfStmt();
    120         result.expr = expr;
    121         result.thn = thn;
    122         result.els = els;
    123         result.loc = loc;
    124         return result;
    125      }
    126    }