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 }