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 escjava.ast;
013    
014    import java.util.Hashtable;
015    import java.util.Set;
016    import java.util.ArrayList;
017    
018    import javafe.ast.*;
019    import javafe.util.Assert;
020    import javafe.util.Location;
021    import escjava.ParsedRoutineSpecs;
022    
023    // Convention: unless otherwise noted, integer fields named "loc" refer
024    // to the location of the first character of the syntactic unit
025    
026    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
027    //# VisitorRoot javafe.ast.Visitor
028    
029    public abstract class VisitorArgResult extends javafe.ast.VisitorArgResult {
030      //@ requires x != null;
031      //@ ensures \result != null;
032      public abstract Object visitAnOverview(AnOverview x, Object o);
033    
034      //@ requires x != null;
035      //@ ensures \result != null;
036      public abstract Object visitGCExpr(GCExpr x, Object o);
037    
038      //@ requires x != null;
039      //@ ensures \result != null;
040      public Object visitNaryExpr(NaryExpr x, Object o) {
041        return visitGCExpr(x, o);
042      }
043    
044      //@ requires x != null;
045      //@ ensures \result != null;
046      public Object visitQuantifiedExpr(QuantifiedExpr x, Object o) {
047        return visitGCExpr(x, o);
048      }
049    
050      //@ requires x != null;
051      //@ ensures \result != null;
052      public Object visitGeneralizedQuantifiedExpr(GeneralizedQuantifiedExpr x, Object o) {
053        return visitGCExpr(x, o);
054      }
055    
056      //@ requires x != null;
057      //@ ensures \result != null;
058      public Object visitNumericalQuantifiedExpr(NumericalQuantifiedExpr x, Object o) {
059        return visitGCExpr(x, o);
060      }
061    
062      //@ requires x != null;
063      //@ ensures \result != null;
064      public Object visitSubstExpr(SubstExpr x, Object o) {
065        return visitGCExpr(x, o);
066      }
067    
068      //@ requires x != null;
069      //@ ensures \result != null;
070      public Object visitTypeExpr(TypeExpr x, Object o) {
071        return visitGCExpr(x, o);
072      }
073    
074      //@ requires x != null;
075      //@ ensures \result != null;
076      public Object visitLabelExpr(LabelExpr x, Object o) {
077        return visitGCExpr(x, o);
078      }
079    
080      //@ requires x != null;
081      //@ ensures \result != null;
082      public abstract Object visitWildRefExpr(WildRefExpr x, Object o);
083    
084      //@ requires x != null;
085      //@ ensures \result != null;
086      public abstract Object visitGuardExpr(GuardExpr x, Object o);
087    
088      //@ requires x != null;
089      //@ ensures \result != null;
090      public abstract Object visitResExpr(ResExpr x, Object o);
091    
092      //@ requires x != null;
093      //@ ensures \result != null;
094      public abstract Object visitSetCompExpr(SetCompExpr x, Object o);
095    
096      //@ requires x != null;
097      //@ ensures \result != null;
098      public abstract Object visitLockSetExpr(LockSetExpr x, Object o);
099    
100      //@ requires x != null;
101      //@ ensures \result != null;
102      public abstract Object visitEverythingExpr(EverythingExpr x, Object o);
103    
104      //@ requires x != null;
105      //@ ensures \result != null;
106      public abstract Object visitNothingExpr(NothingExpr x, Object o);
107    
108      //@ requires x != null;
109      //@ ensures \result != null;
110      public abstract Object visitNotSpecifiedExpr(NotSpecifiedExpr x, Object o);
111    
112      //@ requires x != null;
113      //@ ensures \result != null;
114      public abstract Object visitNotModifiedExpr(NotModifiedExpr x, Object o);
115    
116      //@ requires x != null;
117      //@ ensures \result != null;
118      public abstract Object visitArrayRangeRefExpr(ArrayRangeRefExpr x, Object o);
119    
120      //@ requires x != null;
121      //@ ensures \result != null;
122      public abstract Object visitDefPredLetExpr(DefPredLetExpr x, Object o);
123    
124      //@ requires x != null;
125      //@ ensures \result != null;
126      public abstract Object visitDefPredApplExpr(DefPredApplExpr x, Object o);
127    
128      //@ requires x != null;
129      //@ ensures \result != null;
130      public abstract Object visitGuardedCmd(GuardedCmd x, Object o);
131    
132      //@ requires x != null;
133      //@ ensures \result != null;
134      public Object visitSimpleCmd(SimpleCmd x, Object o) {
135        return visitGuardedCmd(x, o);
136      }
137    
138      //@ requires x != null;
139      //@ ensures \result != null;
140      public Object visitExprCmd(ExprCmd x, Object o) {
141        return visitGuardedCmd(x, o);
142      }
143    
144      //@ requires x != null;
145      //@ ensures \result != null;
146      public Object visitAssignCmd(AssignCmd x, Object o) {
147        return visitGuardedCmd(x, o);
148      }
149    
150      //@ requires x != null;
151      //@ ensures \result != null;
152      public Object visitGetsCmd(GetsCmd x, Object o) {
153        return visitAssignCmd(x, o);
154      }
155    
156      //@ requires x != null;
157      //@ ensures \result != null;
158      public Object visitSubGetsCmd(SubGetsCmd x, Object o) {
159        return visitAssignCmd(x, o);
160      }
161    
162      //@ requires x != null;
163      //@ ensures \result != null;
164      public Object visitSubSubGetsCmd(SubSubGetsCmd x, Object o) {
165        return visitAssignCmd(x, o);
166      }
167    
168      //@ requires x != null;
169      //@ ensures \result != null;
170      public Object visitRestoreFromCmd(RestoreFromCmd x, Object o) {
171        return visitAssignCmd(x, o);
172      }
173    
174      //@ requires x != null;
175      //@ ensures \result != null;
176      public Object visitVarInCmd(VarInCmd x, Object o) {
177        return visitGuardedCmd(x, o);
178      }
179    
180      //@ requires x != null;
181      //@ ensures \result != null;
182      public Object visitDynInstCmd(DynInstCmd x, Object o) {
183        return visitGuardedCmd(x, o);
184      }
185    
186      //@ requires x != null;
187      //@ ensures \result != null;
188      public Object visitSeqCmd(SeqCmd x, Object o) {
189        return visitGuardedCmd(x, o);
190      }
191    
192      //@ requires x != null;
193      //@ ensures \result != null;
194      public Object visitLoopCmd(LoopCmd x, Object o) {
195        return visitGuardedCmd(x, o);
196      }
197    
198      //@ requires x != null;
199      //@ ensures \result != null;
200      public Object visitCmdCmdCmd(CmdCmdCmd x, Object o) {
201        return visitGuardedCmd(x, o);
202      }
203    
204      //@ requires x != null;
205      //@ ensures \result != null;
206      public Object visitCall(Call x, Object o) {
207        return visitGuardedCmd(x, o);
208      }
209    
210      //@ requires x != null;
211      //@ ensures \result != null;
212      public abstract Object visitExprDeclPragma(ExprDeclPragma x, Object o);
213    
214      //@ requires x != null;
215      //@ ensures \result != null;
216      public abstract Object visitIdExprDeclPragma(IdExprDeclPragma x, Object o);
217    
218      //@ requires x != null;
219      //@ ensures \result != null;
220      public abstract Object visitNamedExprDeclPragma(NamedExprDeclPragma x, Object o);
221    
222      //@ requires x != null;
223      //@ ensures \result != null;
224      public abstract Object visitModelDeclPragma(ModelDeclPragma x, Object o);
225    
226      //@ requires x != null;
227      //@ ensures \result != null;
228      public abstract Object visitDependsPragma(DependsPragma x, Object o);
229    
230      //@ requires x != null;
231      //@ ensures \result != null;
232      public abstract Object visitModelConstructorDeclPragma(ModelConstructorDeclPragma x, Object o);
233    
234      //@ requires x != null;
235      //@ ensures \result != null;
236      public abstract Object visitModelTypePragma(ModelTypePragma x, Object o);
237    
238      //@ requires x != null;
239      //@ ensures \result != null;
240      public abstract Object visitModelMethodDeclPragma(ModelMethodDeclPragma x, Object o);
241    
242      //@ requires x != null;
243      //@ ensures \result != null;
244      public abstract Object visitGhostDeclPragma(GhostDeclPragma x, Object o);
245    
246      //@ requires x != null;
247      //@ ensures \result != null;
248      public abstract Object visitStillDeferredDeclPragma(StillDeferredDeclPragma x, Object o);
249    
250      //@ requires x != null;
251      //@ ensures \result != null;
252      public abstract Object visitSimpleStmtPragma(SimpleStmtPragma x, Object o);
253    
254      //@ requires x != null;
255      //@ ensures \result != null;
256      public abstract Object visitIdentifierModifierPragma(IdentifierModifierPragma x, Object o);
257    
258      //@ requires x != null;
259      //@ ensures \result != null;
260      public abstract Object visitExprStmtPragma(ExprStmtPragma x, Object o);
261    
262      //@ requires x != null;
263      //@ ensures \result != null;
264      public abstract Object visitSetStmtPragma(SetStmtPragma x, Object o);
265    
266      //@ requires x != null;
267      //@ ensures \result != null;
268      public abstract Object visitSkolemConstantPragma(SkolemConstantPragma x, Object o);
269    
270      //@ requires x != null;
271      //@ ensures \result != null;
272      public abstract Object visitModelProgamModifierPragma(ModelProgamModifierPragma x, Object o);
273    
274      //@ requires x != null;
275      //@ ensures \result != null;
276      public abstract Object visitNestedModifierPragma(NestedModifierPragma x, Object o);
277    
278      //@ requires x != null;
279      //@ ensures \result != null;
280      public abstract Object visitParsedSpecs(ParsedSpecs x, Object o);
281    
282      //@ requires x != null;
283      //@ ensures \result != null;
284      public abstract Object visitSimpleModifierPragma(SimpleModifierPragma x, Object o);
285    
286      //@ requires x != null;
287      //@ ensures \result != null;
288      public abstract Object visitExprModifierPragma(ExprModifierPragma x, Object o);
289    
290      //@ requires x != null;
291      //@ ensures \result != null;
292      public abstract Object visitModifiesGroupPragma(ModifiesGroupPragma x, Object o);
293    
294      //@ requires x != null;
295      //@ ensures \result != null;
296      public abstract Object visitCondExprModifierPragma(CondExprModifierPragma x, Object o);
297    
298      //@ requires x != null;
299      //@ ensures \result != null;
300      public abstract Object visitMapsExprModifierPragma(MapsExprModifierPragma x, Object o);
301    
302      //@ requires x != null;
303      //@ ensures \result != null;
304      public abstract Object visitReachModifierPragma(ReachModifierPragma x, Object o);
305    
306      //@ requires x != null;
307      //@ ensures \result != null;
308      public abstract Object visitVarDeclModifierPragma(VarDeclModifierPragma x, Object o);
309    
310      //@ requires x != null;
311      //@ ensures \result != null;
312      public abstract Object visitVarExprModifierPragma(VarExprModifierPragma x, Object o);
313    
314      //@ requires x != null;
315      //@ ensures \result != null;
316      public abstract Object visitNowarnPragma(NowarnPragma x, Object o);
317    
318      //@ requires x != null;
319      //@ ensures \result != null;
320      public abstract Object visitImportPragma(ImportPragma x, Object o);
321    
322      //@ requires x != null;
323      //@ ensures \result != null;
324      public abstract Object visitRefinePragma(RefinePragma x, Object o);
325    
326      //@ requires x != null;
327      //@ ensures \result != null;
328      public abstract Object visitSpec(Spec x, Object o);
329    
330      //@ requires x != null;
331      //@ ensures \result != null;
332      public abstract Object visitCondition(Condition x, Object o);
333    
334      //@ requires x != null;
335      //@ ensures \result != null;
336      public abstract Object visitDefPred(DefPred x, Object o);
337    
338    }