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 LoopCmd extends GuardedCmd
032 {
033 public int locStart;
034
035 public int locEnd;
036
037 public int locHotspot;
038
039 public /*@ non_null @*/ Hashtable oldmap;
040
041 public /*@ non_null @*/ ConditionVec invariants;
042
043 public /*@ non_null @*/ DecreasesInfoVec decreases;
044
045 public /*@ non_null @*/ LocalVarDeclVec skolemConstants;
046
047 public /*@ non_null @*/ ExprVec predicates;
048
049 public /*@ non_null @*/ GenericVarDeclVec tempVars;
050
051 public /*@ non_null @*/ GuardedCmd guard;
052
053 public /*@ non_null @*/ GuardedCmd body;
054
055
056 public GuardedCmd desugared;
057
058 //@ public represents startLoc <- locStart;
059 public /*@ pure @*/ int getStartLoc() { return locStart; }
060 /*@ also
061 @ public normal_behavior
062 @ ensures \result == locEnd;
063 @*/
064 public /*@ pure @*/ int getEndLoc() { return locEnd; }
065
066
067 // Generated boilerplate constructors:
068
069 //@ ensures this.locStart == locStart;
070 //@ ensures this.locEnd == locEnd;
071 //@ ensures this.locHotspot == locHotspot;
072 //@ ensures this.oldmap == oldmap;
073 //@ ensures this.invariants == invariants;
074 //@ ensures this.decreases == decreases;
075 //@ ensures this.skolemConstants == skolemConstants;
076 //@ ensures this.predicates == predicates;
077 //@ ensures this.tempVars == tempVars;
078 //@ ensures this.guard == guard;
079 //@ ensures this.body == body;
080 protected LoopCmd(int locStart, int locEnd, int locHotspot, /*@ non_null @*/ Hashtable oldmap, /*@ non_null @*/ ConditionVec invariants, /*@ non_null @*/ DecreasesInfoVec decreases, /*@ non_null @*/ LocalVarDeclVec skolemConstants, /*@ non_null @*/ ExprVec predicates, /*@ non_null @*/ GenericVarDeclVec tempVars, /*@ non_null @*/ GuardedCmd guard, /*@ non_null @*/ GuardedCmd body) {
081 super();
082 this.locStart = locStart;
083 this.locEnd = locEnd;
084 this.locHotspot = locHotspot;
085 this.oldmap = oldmap;
086 this.invariants = invariants;
087 this.decreases = decreases;
088 this.skolemConstants = skolemConstants;
089 this.predicates = predicates;
090 this.tempVars = tempVars;
091 this.guard = guard;
092 this.body = body;
093 }
094
095 // Generated boilerplate methods:
096
097 public final int childCount() {
098 int sz = 0;
099 if (this.invariants != null) sz += this.invariants.size();
100 if (this.decreases != null) sz += this.decreases.size();
101 if (this.skolemConstants != null) sz += this.skolemConstants.size();
102 if (this.predicates != null) sz += this.predicates.size();
103 if (this.tempVars != null) sz += this.tempVars.size();
104 return sz + 3;
105 }
106
107 public final Object childAt(int index) {
108 /*throws IndexOutOfBoundsException*/
109 if (index < 0)
110 throw new IndexOutOfBoundsException("AST child index " + index);
111 int indexPre = index;
112
113 int sz;
114
115 if (index == 0) return this.oldmap;
116 else index--;
117
118 sz = (this.invariants == null ? 0 : this.invariants.size());
119 if (0 <= index && index < sz)
120 return this.invariants.elementAt(index);
121 else index -= sz;
122
123 sz = (this.decreases == null ? 0 : this.decreases.size());
124 if (0 <= index && index < sz)
125 return this.decreases.elementAt(index);
126 else index -= sz;
127
128 sz = (this.skolemConstants == null ? 0 : this.skolemConstants.size());
129 if (0 <= index && index < sz)
130 return this.skolemConstants.elementAt(index);
131 else index -= sz;
132
133 sz = (this.predicates == null ? 0 : this.predicates.size());
134 if (0 <= index && index < sz)
135 return this.predicates.elementAt(index);
136 else index -= sz;
137
138 sz = (this.tempVars == null ? 0 : this.tempVars.size());
139 if (0 <= index && index < sz)
140 return this.tempVars.elementAt(index);
141 else index -= sz;
142
143 if (index == 0) return this.guard;
144 else index--;
145
146 if (index == 0) return this.body;
147 else index--;
148
149 throw new IndexOutOfBoundsException("AST child index " + indexPre);
150 } //@ nowarn Exception;
151
152 public final /*@non_null*/String toString() {
153 return "[LoopCmd"
154 + " locStart = " + this.locStart
155 + " locEnd = " + this.locEnd
156 + " locHotspot = " + this.locHotspot
157 + " oldmap = " + this.oldmap
158 + " invariants = " + this.invariants
159 + " decreases = " + this.decreases
160 + " skolemConstants = " + this.skolemConstants
161 + " predicates = " + this.predicates
162 + " tempVars = " + this.tempVars
163 + " guard = " + this.guard
164 + " body = " + this.body
165 + "]";
166 }
167
168 public final int getTag() {
169 return TagConstants.LOOPCMD;
170 }
171
172 public final void accept(javafe.ast.Visitor v) {
173 if (v instanceof Visitor) ((Visitor)v).visitLoopCmd(this);
174 }
175
176 public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
177 if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitLoopCmd(this, o); else return null;
178 }
179
180 public void check() {
181 super.check();
182 if (this.oldmap == null) throw new RuntimeException();
183 for(int i = 0; i < this.invariants.size(); i++)
184 this.invariants.elementAt(i).check();
185 for(int i = 0; i < this.decreases.size(); i++)
186 this.decreases.elementAt(i).check();
187 for(int i = 0; i < this.skolemConstants.size(); i++)
188 this.skolemConstants.elementAt(i).check();
189 for(int i = 0; i < this.predicates.size(); i++)
190 this.predicates.elementAt(i).check();
191 for(int i = 0; i < this.tempVars.size(); i++)
192 this.tempVars.elementAt(i).check();
193 this.guard.check();
194 this.body.check();
195 }
196
197 //@ ensures \result != null;
198 public static LoopCmd make(int locStart, int locEnd, int locHotspot, /*@ non_null @*/ Hashtable oldmap, /*@ non_null @*/ ConditionVec invariants, /*@ non_null @*/ DecreasesInfoVec decreases, /*@ non_null @*/ LocalVarDeclVec skolemConstants, /*@ non_null @*/ ExprVec predicates, /*@ non_null @*/ GenericVarDeclVec tempVars, /*@ non_null @*/ GuardedCmd guard, /*@ non_null @*/ GuardedCmd body) {
199 LoopCmd result = new LoopCmd(locStart, locEnd, locHotspot, oldmap, invariants, decreases, skolemConstants, predicates, tempVars, guard, body);
200 return result;
201 }
202 }