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