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 escjava.ast;
014
015 import java.util.Hashtable;
016 import java.util.Set;
017 import java.util.ArrayList;
018
019 import javafe.ast.*;
020 import javafe.util.Assert;
021 import javafe.util.Location;
022 import escjava.ParsedRoutineSpecs;
023
024 // Convention: unless otherwise noted, integer fields named "loc" refer
025 // to the location of the first character of the syntactic unit
026
027 //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
028 //# VisitorRoot javafe.ast.Visitor
029
030
031 public class ReachModifierPragma extends ModifierPragma
032 {
033 public /*@ non_null @*/ Expr expr;
034
035 public /*@ non_null @*/ Identifier id;
036
037 public /*@ non_null @*/ IdentifierVec storerefs;
038
039 public int loc;
040
041
042 //@ public represents startLoc <- loc;
043 public /*@ pure @*/ int getStartLoc() { return loc; }
044
045
046 // Generated boilerplate constructors:
047
048 //@ ensures this.expr == expr;
049 //@ ensures this.id == id;
050 //@ ensures this.storerefs == storerefs;
051 //@ ensures this.loc == loc;
052 protected ReachModifierPragma(/*@ non_null @*/ Expr expr, /*@ non_null @*/ Identifier id, /*@ non_null @*/ IdentifierVec storerefs, int loc) {
053 this.expr = expr;
054 this.id = id;
055 this.storerefs = storerefs;
056 this.loc = loc;
057 }
058
059 // Generated boilerplate methods:
060
061 public final int childCount() {
062 int sz = 0;
063 if (this.storerefs != null) sz += this.storerefs.size();
064 return sz + 2;
065 }
066
067 public final Object childAt(int index) {
068 /*throws IndexOutOfBoundsException*/
069 if (index < 0)
070 throw new IndexOutOfBoundsException("AST child index " + index);
071 int indexPre = index;
072
073 int sz;
074
075 if (index == 0) return this.expr;
076 else index--;
077
078 if (index == 0) return this.id;
079 else index--;
080
081 sz = (this.storerefs == null ? 0 : this.storerefs.size());
082 if (0 <= index && index < sz)
083 return this.storerefs.elementAt(index);
084 else index -= sz;
085
086 throw new IndexOutOfBoundsException("AST child index " + indexPre);
087 } //@ nowarn Exception;
088
089 public final /*@non_null*/String toString() {
090 return "[ReachModifierPragma"
091 + " expr = " + this.expr
092 + " id = " + this.id
093 + " storerefs = " + this.storerefs
094 + " loc = " + this.loc
095 + "]";
096 }
097
098 public final int getTag() {
099 return TagConstants.REACHMODIFIERPRAGMA;
100 }
101
102 public final void accept(javafe.ast.Visitor v) {
103 if (v instanceof Visitor) ((Visitor)v).visitReachModifierPragma(this);
104 }
105
106 public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
107 if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitReachModifierPragma(this, o); else return null;
108 }
109
110 public void check() {
111 this.expr.check();
112 this.id.check();
113 for(int i = 0; i < this.storerefs.size(); i++)
114 this.storerefs.elementAt(i).check();
115 }
116
117 //@ ensures \result != null;
118 public static ReachModifierPragma make(/*@ non_null @*/ Expr expr, /*@ non_null @*/ Identifier id, /*@ non_null @*/ IdentifierVec storerefs, int loc) {
119 ReachModifierPragma result = new ReachModifierPragma(expr, id, storerefs, loc);
120 return result;
121 }
122 }