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    }