    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 escjava.ast;
    013
    014    import java.util.Hashtable;
    015    import java.util.Set;
    016    import java.util.ArrayList;
    017
    018    import javafe.ast.*;
    019    import javafe.util.Assert;
    020    import javafe.util.Location;
    021    import escjava.ParsedRoutineSpecs;
    022
    023    // Convention: unless otherwise noted, integer fields named "loc" refer
    024    // to the location of the first character of the syntactic unit
    025
    026    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
    027    //# VisitorRoot javafe.ast.Visitor
    028
    029
    030    public class ArrayRangeRefExpr extends Expr
    031    {
    032      public int locOpenBracket;
    033
    034      public /*@ non_null @*/ Expr array;
    035
    036      public Expr lowIndex;
    037
    038      public Expr highIndex;
    039
    040
    041      public int getStartLoc() { return locOpenBracket; }
    042
    043
    044    // Generated boilerplate constructors:
    045
    046      /**
    047       * Construct a raw ArrayRangeRefExpr whose class invariant(s) have not
    048       * yet been established.  It is the caller's job to
    049       * initialize the returned node's fields so that any
    050       * class invariants hold.
    051       */
    052      //@ requires I_will_establish_invariants_afterwards;
    053      protected ArrayRangeRefExpr() {}    //@ nowarn Invariant,NonNullInit;
    054
    055
    056    // Generated boilerplate methods:
    057
    058      public final int childCount() {
    059         return 3;
    060      }
    061
    062      public final Object childAt(int index) {
    063              /*throws IndexOutOfBoundsException*/
    064         if (index < 0)
    065            throw new IndexOutOfBoundsException("AST child index " + index);
    066         int indexPre = index;
    067
    068         int sz;
    069
    070         if (index == 0) return this.array;
    071         else index--;
    072
    073         if (index == 0) return this.lowIndex;
    074         else index--;
    075
    076         if (index == 0) return this.highIndex;
    077         else index--;
    078
    079         throw new IndexOutOfBoundsException("AST child index " + indexPre);
    080      }   //@ nowarn Exception;
    081
    082      public final String toString() {
    083         return "[ArrayRangeRefExpr"
    084            + " locOpenBracket = " + this.locOpenBracket
    085            + " array = " + this.array
    086            + " lowIndex = " + this.lowIndex
    087            + " highIndex = " + this.highIndex
    088            + "]";
    089      }
    090
    091      public final int getTag() {
    092         return TagConstants.ARRAYRANGEREFEXPR;
    093      }
    094
    095      public final void accept(javafe.ast.Visitor v) {
    096        if (v instanceof Visitor) ((Visitor)v).visitArrayRangeRefExpr(this);
    097      }
    098
    099      public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
    100        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitArrayRangeRefExpr(this, o); else return null;
    101      }
    102
    103      public void check() {
    104         this.array.check();
    105         if (this.lowIndex != null)
    106            this.lowIndex.check();
    107         if (this.highIndex != null)
    108            this.highIndex.check();
    109      }
    110
    111      //@ ensures \result != null;
    112      public static ArrayRangeRefExpr make(int locOpenBracket, /*@ non_null @*/ Expr array, Expr lowIndex, Expr highIndex) {
    113         //@ set I_will_establish_invariants_afterwards = true;
    114         ArrayRangeRefExpr result = new ArrayRangeRefExpr();
    115         result.locOpenBracket = locOpenBracket;
    116         result.array = array;
    117         result.lowIndex = lowIndex;
    118         result.highIndex = highIndex;
    119         return result;
    120      }
    121    }