    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 ArrayType extends Type
    023    {
    024      // We have associated locations iff elemType does:
    025      //@ invariant elemType.syntax == syntax;
    026
    027      public /*@ non_null @*/ Type elemType;
    028
    029      //@ invariant locOpenBracket != javafe.util.Location.NULL;
    030      public int locOpenBracket;
    031
    032      public int getStartLoc() { return elemType.getStartLoc(); }
    033      public int getEndLoc() {
    034        return Location.inc(locOpenBracket, 1);
    035      }
    036
    037      // Generate this manually to add condition about syntax:
    038      //@ requires locOpenBracket != javafe.util.Location.NULL;
    039      //@ ensures elemType.syntax ==> \result.syntax;
    040      //@ ensures \result != null;
    041      public static ArrayType make(/*@ non_null @*/ Type elemType,
    042                                   int locOpenBracket) {
    043         //@ set I_will_establish_invariants_afterwards = true;
    044         ArrayType result = new ArrayType();
    045         // Can't fix this since elemType is *not* injective:
    046         //@ assume (\forall ArrayType a; a.elemType != result);
    047         result.elemType = elemType;
    048         result.locOpenBracket = locOpenBracket;
    049         //@ set result.syntax = elemType.syntax;
    050         return result;
    051      }
    052
    053      //@ requires locOpenBracket != javafe.util.Location.NULL;
    054      //@ ensures elemType.syntax ==> \result.syntax;
    055      //@ ensures \result != null;
    056      public static ArrayType make(TypeModifierPragmaVec tmodifiers,
    057                                   /*@ non_null @*/ Type elemType,
    058                                   int locOpenBracket) {
    059            ArrayType at = ArrayType.make(elemType, locOpenBracket);
    060            at.tmodifiers = tmodifiers;
    061            return at;
    062      }
    063
    064
    065    // Generated boilerplate constructors:
    066
    067      /**
    068       * Construct a raw ArrayType whose class invariant(s) have not
    069       * yet been established.  It is the caller's job to
    070       * initialize the returned node's fields so that any
    071       * class invariants hold.
    072       */
    073      //@ requires I_will_establish_invariants_afterwards;
    074      protected ArrayType() {}    //@ nowarn Invariant,NonNullInit;
    075
    076
    077    // Generated boilerplate methods:
    078
    079      public final int childCount() {
    080         int sz = 0;
    081         if (this.tmodifiers != null) sz += this.tmodifiers.size();
    082         return sz + 1;
    083      }
    084
    085      public final Object childAt(int index) {
    086              /*throws IndexOutOfBoundsException*/
    087         if (index < 0)
    088            throw new IndexOutOfBoundsException("AST child index " + index);
    089         int indexPre = index;
    090
    091         int sz;
    092
    093         sz = (this.tmodifiers == null ? 0 : this.tmodifiers.size());
    094         if (0 <= index && index < sz)
    095            return this.tmodifiers.elementAt(index);
    096         else index -= sz;
    097
    098         if (index == 0) return this.elemType;
    099         else index--;
    100
    101         throw new IndexOutOfBoundsException("AST child index " + indexPre);
    102      }   //@ nowarn Exception;
    103
    104      public final String toString() {
    105         return "[ArrayType"
    106            + " tmodifiers = " + this.tmodifiers
    107            + " elemType = " + this.elemType
    108            + " locOpenBracket = " + this.locOpenBracket
    109            + "]";
    110      }
    111
    112      public final int getTag() {
    113         return TagConstants.ARRAYTYPE;
    114      }
    115
    116      public final void accept(Visitor v) { v.visitArrayType(this); }
    117
    118      public final Object accept(VisitorArgResult v, Object o) {return v.visitArrayType(this, o); }
    119
    120      public void check() {
    121         super.check();
    122         if (this.tmodifiers != null)
    123            for(int i = 0; i < this.tmodifiers.size(); i++)
    124               this.tmodifiers.elementAt(i).check();
    125         this.elemType.check();
    126      }
    127
    128    }