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