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 javafe.ast;
014
015 import javafe.util.Assert;
016 import javafe.util.Location;
017 import javafe.util.ErrorSet;
018
019 // Convention: unless otherwise noted, integer fields named "loc" refer
020 // to the location of the first character of the syntactic unit
021
022
023 /**
024 * <code>ASTNode</code> is the root of the abstract syntax tree node
025 * hierarchy. Every class representing a node in the AST is a (direct
026 * or indirect) subclass of this class.
027 *
028 * <p> In designing our AST classes, the following, broad approach was
029 * taken:
030 *
031 * <ul>
032 *
033 * <li> <b>Design package javafe.ast to stand alone.</b>
034 *
035 * <li> <b>Have a large, deep hierarchy, using the type system to
036 * encode many invariants.</b> (Used a program to generate boilerplate
037 * code, making it the large hierarchy more manageable.)
038 *
039 * <li> <b>Represent children with public fields.</b>
040 *
041 * <li> <b>Put most code outside AST classes.</b>
042 *
043 * <li> <b>Support both switch-based and visitor-based traversal.</b>
044 *
045 * <li> <b>Liberal use of locations.</b> AST classes contain location
046 * fields that indicate the corresponding part of the source program.
047 *
048 * <li> <b>Use generic decorations.</b>
049 *
050 * <li> <b>Rewrite tree to handle disambiguation.</b> Expression names
051 * and method names are ambiguous: the be of the form
052 * <i>package.type.members</i> or <i>type.members</i> or
053 * <i>local-variable.members</i> or even <i>members</i>. The parser
054 * does not attempt to disambiguate among these, but rather generates
055 * either <code>ExprName</code> or <code>MethodName</code>. A later
056 * pass replaces these nodes with either <code>VariableAccess</code>
057 * or concrete subclasses of <code>FieldAccess</code> or
058 * <code>MethodInvocation</code>.
059 *
060 * <li> <b>Fill in fields and decorations to handle resolution.</b>
061 * The nodes that need to be resolved are: <code>TypeName</code>,
062 * <code>VariableAccess</code>, (three subclasses of)
063 * <code>FieldAccess</code>, (three subclasses of)
064 * <code>MethodInvocation</code>, <code>ConstructorInvocation</code>,
065 * and <code>NewInstanceExpr</code>. All nodes except
066 * <code>TypeName</code> have a field named <code>decl</code> of the
067 * approriate type that is initialized to <code>null</code> and is
068 * filled in by name resolution. For <code>TypeName</code> we use a
069 * decoration rather than a field to avoid a dependency on the
070 * <code>javafe.tc</code> package.
071 *
072 * </ul>
073 *
074 * <p> Measurements (circa SRC ESC/Java):
075 * <blockquote>
076 * Node abstract classes: 13
077 * <br> Node concrete classes: 59
078 * <br> Sequence classes: 12
079 * <br> Total classes: 84
080 * <br>
081 * <br> Input to code generator: 842 lines of code (513 excluding comments)
082 * <br> Code generator: 993 (675)
083 * <br> Total lines of code: 1835 (1188)
084 * <br> Output of code generator: 4298
085 * </blockquote>
086 *
087 * <p> The complete list of subclasses is shown below. The names of
088 * subclasses of this class correspond (in general) to the syntactic
089 * units that they represent. Any exceptions to this rule are
090 * documented. All non-leaf classes are abstract. In parenthesis,
091 * the names and types of fields holding the locally-defined children
092 * classes are listed; a postfix <code>*</code> on a type indicates a
093 * sequence. Square brackets indicate optional elements; the only
094 * these fields can be null.
095 *
096 * <pre>
097 * ASTNode
098 * CompilationUnit ([Name pkgName], [LexicalPragma* lexicalPragmas], ImportDecl* imports, TypeDecl* elems)
099 * ImportDecl ()
100 * SingleTypeImport (TypeName typeName)
101 * OnDemandImport (Name pkgName)
102 * TypeDecl (int modifiers, [ModifierPragma* pmodifiers], Identifier id, [TypeModifierPragma* tmodifiers], TypeName* superInterfaces, TypeDeclElem* elems)
103 * ClassDecl ([TypeName superClass])
104 * InterfaceDecl ()
105 * TypeDeclElem () NOTE: This is an <em>interface</em>
106 * TypeDecl
107 * FieldDecl
108 * RoutineDecl (int modifiers, [ModifierPragma* pmodifiers], FormalParaDecl* args, TypeName* raises, [BlockStmt body])
109 * ConstructorDecl ([TypeModifierPragma* tmodifiers])
110 * MethodDecl (Identifier id, Type returnType)
111 * InitBlock (int modifiers, [ModifierPragma* pmodifiers], BlockStmt block)
112 * TypeDeclElemPragma ()
113 * GenericVarDecl (int modifiers, [ModifierPragma* pmodifiers], Identifier id, Type type)
114 * LocalVarDecl ([VarInit init])
115 * FieldDecl ([VarInit init])
116 * FormalParaDecl ()
117 * Stmt ()
118 * GenericBlockStmt (Stmt* stmts)
119 * BlockStmt ()
120 * SwitchStmt (Expr expr)
121 * AssertStmt (Expr expr, String l)
122 * VarDeclStmt (LocalVarDecl decl)
123 * ClassDeclStmt (ClassDecl anonDecl)
124 * WhileStmt (Expr expr, Stmt stmt)
125 * DoStmt (Expr expr, Stmt stmt)
126 * SynchronizeStmt (Expr expr, BlockStmt stmt)
127 * EvalStmt (Expr expr)
128 * ReturnStmt ([Expr expr])
129 * ThrowStmt (Expr expr)
130 * BranchStmt ([Identifier label])
131 * BreakStmt ()
132 * ContinueStmt ()
133 * LabelStmt (Identifier label, Stmt stmt)
134 * IfStmt (Expr expr, Stmt thn, Stmt els)
135 * ForStmt (Stmt* forInit, Expr test, Expr* forUpdate, Stmt body)
136 * SkipStmt ()
137 * SwitchLabel ([Expr expr])
138 * TryFinallyStmt (Stmt tryClause, Stmt finallyClause)
139 * TryCatchStmt (Stmt tryClause, CatchClause* catchClauses)
140 * StmtPragma ()
141 * ConstructorInvocation (boolean superCall, [Expr enclosingInstance], Expr* args)
142 * CatchClause (FormalParaDecl arg, Stmt body)
143 * VarInit ()
144 * ArrayInit (VarInit* elems)
145 * Expr ()
146 * ThisExpr (Type classPrefix)
147 * LiteralExpr (int tag, [Object value])
148 * ArrayRefExpr (Expr array, Expr index)
149 * NewInstanceExpr ([Expr enclosingInstance], TypeName type, Expr* args, [ClassDecl decl])
150 * NewArrayExpr (Type type, Expr* dims, [ArrayInit init])
151 * CondExpr (Expr test, Expr thn, Expr els)
152 * InstanceOfExpr (Expr expr, Type type)
153 * CastExpr (Expr expr, Type type)
154 * BinaryExpr (int op, Expr left, Expr right)
155 * UnaryExpr (int op, Expr expr)
156 * ParenExpr (Expr expr)
157 * AmbiguousVariableAccess (Name name)
158 * VariableAccess (Identifier id)
159 * FieldAccess (ObjectDesignator od, Identifier id)
160 * AmbiguousMethodInvocation (Name name, Expr* args)
161 * MethodInvocation (ObjectDesignator od, Identifier id, Expr* args)
162 * ClassLiteral (Type type)
163 * ObjectDesignator () // "expr.", "type." or "super."
164 * ExprObjectDesignator (Expr expr)
165 * TypeObjectDesignator (Type type)
166 * SuperObjectDesignator ()
167 * Type ()
168 * ErrorType() // was previously represented as a PrimitiveType
169 * PrimitiveType (int tag)
170 * JavafePrimitiveType () // this is a new type introduced to allow for other (e.g., esc) primitive types
171 * TypeName (Name name)
172 * ArrayType (Type elemType)
173 * Name ()
174 * SimpleName (Identifier id)
175 * CompoundName (Identifier* ids)
176 * ModifierPragma ()
177 * LexicalPragma ()
178 * TypeModifierPragma ()
179 * </pre>
180 */
181
182 public abstract class ASTNode implements Cloneable
183 {
184 /**
185 * The decorations that have been attached to this node. This is a
186 * package-level field accessed by the <code>ASTDecoration</code>
187 * class. There are different ways to implement decorations; this
188 * way is not space-efficient, but it's pretty fast.
189 */
190
191 //@ invariant decorations != null ==> (\typeof(decorations) == \type(Object[]));
192 /*@spec_public*/ private Object[] decorations;
193
194 public int bogusField;
195 //@ public model int startLoc;
196 //@ public model boolean isInternal;
197 //@ public represents isInternal <- startLoc == Location.NULL;
198
199 /*@ public normal_behavior
200 @ ensures \result == startLoc;
201 @*/
202 public /*@ pure @*/ abstract int getStartLoc();
203
204 public /*@ pure @*/ int getEndLoc() {
205 return getStartLoc();
206 }
207
208 //@ public model int endLoc;
209 //@ public represents endLoc <- getEndLoc();
210 //@ public invariant startLoc == Location.NULL <==> endLoc == Location.NULL;
211
212 /** returns true iff this in an internally declared node. Note
213 * that internally declared types have no associated location.
214 */
215 /*@ public normal_behavior
216 @ ensures \result == isInternal;
217 @*/
218 public /*@ pure @*/ boolean isInternal() {
219 return getStartLoc() == Location.NULL;
220 }
221
222 //@ ensures \typeof(\result) == \typeof(this);
223 //@ ensures \result.owner == null;
224 public /*@ non_null */ Object clone(boolean b) {
225 ASTNode n = null;
226 try {
227 n = (ASTNode)super.clone();
228 if (!b) {
229 n.decorations = null;
230 }
231 } catch(java.lang.CloneNotSupportedException e) {
232 ErrorSet.fatal("Internal error in AST hierarchy: no clone");
233 n = this; // dummy assingment to appease escjava.
234 }
235 return n;
236 }
237
238 /**
239 * Clone node, where the clone has the same decorations as original.
240 */
241 public Object clone() {
242 return clone(true);
243 }
244
245 public Object[] getDecorations() {
246 return decorations;
247 }
248
249 //@ requires d != null ==> \typeof(d) == \type(Object[]);
250 public void setDecorations(Object d[]) {
251 decorations = d;
252 }
253
254 //$$
255 static public int dotCounter = 0 ;
256 public int dotId;
257
258 /*
259 * Constructor needed for GRAPHICAL representation (dot output)
260 *
261 * This is temporary as I don't know how the class generator works.
262 * And it always generate a constructor empty (which classes with this one
263 * if I remove this useless boolean).
264 */
265 // protected ASTNode(){
266 // dotCounter += 1;
267 // dotId = dotCounter;
268 // }
269 //$$
270
271
272
273 // Generated boilerplate constructors:
274
275 protected ASTNode() {
276 }
277
278
279 // Generated boilerplate methods:
280
281 /** Return the number of children a node has. */
282 //@ ensures \result >= 0;
283 public abstract int childCount();
284
285 /** Return the first-but-ith child of a node. */
286 //@ requires 0 <= i;
287 public abstract Object childAt(int i);
288
289 /** Return the tag of a node. */
290 //@ ensures (this instanceof LiteralExpr) ==> \result==((LiteralExpr)this).tag;
291 //@ ensures (this instanceof BinaryExpr) ==> \result==((BinaryExpr)this).op;
292 //@ ensures (this instanceof UnaryExpr) ==> \result==((UnaryExpr)this).op;
293 //@ ensures (this instanceof PrimitiveType) ==>\result==((PrimitiveType)this).tag;
294 //
295 //@ ensures (\result==javafe.tc.TagConstants.TYPESIG) ==> \typeof(this) <: \type(javafe.tc.TypeSig);
296 //
297 // Remaining part of spec is automatically generated:
298 //@ ensures (\result==TagConstants.COMPILATIONUNIT) ==> \typeof(this) <: \type(javafe.ast.CompilationUnit);
299 //@ ensures (\result==TagConstants.SINGLETYPEIMPORTDECL) ==> \typeof(this) <: \type(javafe.ast.SingleTypeImportDecl);
300 //@ ensures (\result==TagConstants.ONDEMANDIMPORTDECL) ==> \typeof(this) <: \type(javafe.ast.OnDemandImportDecl);
301 //@ ensures (\result==TagConstants.CLASSDECL) ==> \typeof(this) <: \type(javafe.ast.ClassDecl);
302 //@ ensures (\result==TagConstants.INTERFACEDECL) ==> \typeof(this) <: \type(javafe.ast.InterfaceDecl);
303 //@ ensures (\result==TagConstants.CONSTRUCTORDECL) ==> \typeof(this) <: \type(javafe.ast.ConstructorDecl);
304 //@ ensures (\result==TagConstants.METHODDECL) ==> \typeof(this) <: \type(javafe.ast.MethodDecl);
305 //@ ensures (\result==TagConstants.INITBLOCK) ==> \typeof(this) <: \type(javafe.ast.InitBlock);
306 //@ ensures (\result==TagConstants.LOCALVARDECL) ==> \typeof(this) <: \type(javafe.ast.LocalVarDecl);
307 //@ ensures (\result==TagConstants.FIELDDECL) ==> \typeof(this) <: \type(javafe.ast.FieldDecl);
308 //@ ensures (\result==TagConstants.FORMALPARADECL) ==> \typeof(this) <: \type(javafe.ast.FormalParaDecl);
309 //@ ensures (\result==TagConstants.BLOCKSTMT) ==> \typeof(this) <: \type(javafe.ast.BlockStmt);
310 //@ ensures (\result==TagConstants.SWITCHSTMT) ==> \typeof(this) <: \type(javafe.ast.SwitchStmt);
311 //@ ensures (\result==TagConstants.ASSERTSTMT) ==> \typeof(this) <: \type(javafe.ast.AssertStmt);
312 //@ ensures (\result==TagConstants.VARDECLSTMT) ==> \typeof(this) <: \type(javafe.ast.VarDeclStmt);
313 //@ ensures (\result==TagConstants.CLASSDECLSTMT) ==> \typeof(this) <: \type(javafe.ast.ClassDeclStmt);
314 //@ ensures (\result==TagConstants.WHILESTMT) ==> \typeof(this) <: \type(javafe.ast.WhileStmt);
315 //@ ensures (\result==TagConstants.DOSTMT) ==> \typeof(this) <: \type(javafe.ast.DoStmt);
316 //@ ensures (\result==TagConstants.SYNCHRONIZESTMT) ==> \typeof(this) <: \type(javafe.ast.SynchronizeStmt);
317 //@ ensures (\result==TagConstants.EVALSTMT) ==> \typeof(this) <: \type(javafe.ast.EvalStmt);
318 //@ ensures (\result==TagConstants.RETURNSTMT) ==> \typeof(this) <: \type(javafe.ast.ReturnStmt);
319 //@ ensures (\result==TagConstants.THROWSTMT) ==> \typeof(this) <: \type(javafe.ast.ThrowStmt);
320 //@ ensures (\result==TagConstants.BREAKSTMT) ==> \typeof(this) <: \type(javafe.ast.BreakStmt);
321 //@ ensures (\result==TagConstants.CONTINUESTMT) ==> \typeof(this) <: \type(javafe.ast.ContinueStmt);
322 //@ ensures (\result==TagConstants.LABELSTMT) ==> \typeof(this) <: \type(javafe.ast.LabelStmt);
323 //@ ensures (\result==TagConstants.IFSTMT) ==> \typeof(this) <: \type(javafe.ast.IfStmt);
324 //@ ensures (\result==TagConstants.FORSTMT) ==> \typeof(this) <: \type(javafe.ast.ForStmt);
325 //@ ensures (\result==TagConstants.SKIPSTMT) ==> \typeof(this) <: \type(javafe.ast.SkipStmt);
326 //@ ensures (\result==TagConstants.SWITCHLABEL) ==> \typeof(this) <: \type(javafe.ast.SwitchLabel);
327 //@ ensures (\result==TagConstants.TRYFINALLYSTMT) ==> \typeof(this) <: \type(javafe.ast.TryFinallyStmt);
328 //@ ensures (\result==TagConstants.TRYCATCHSTMT) ==> \typeof(this) <: \type(javafe.ast.TryCatchStmt);
329 //@ ensures (\result==TagConstants.CONSTRUCTORINVOCATION) ==> \typeof(this) <: \type(javafe.ast.ConstructorInvocation);
330 //@ ensures (\result==TagConstants.CATCHCLAUSE) ==> \typeof(this) <: \type(javafe.ast.CatchClause);
331 //@ ensures (\result==TagConstants.ARRAYINIT) ==> \typeof(this) <: \type(javafe.ast.ArrayInit);
332 //@ ensures (\result==TagConstants.THISEXPR) ==> \typeof(this) <: \type(javafe.ast.ThisExpr);
333 //@ ensures (\result==TagConstants.ARRAYREFEXPR) ==> \typeof(this) <: \type(javafe.ast.ArrayRefExpr);
334 //@ ensures (\result==TagConstants.NEWINSTANCEEXPR) ==> \typeof(this) <: \type(javafe.ast.NewInstanceExpr);
335 //@ ensures (\result==TagConstants.NEWARRAYEXPR) ==> \typeof(this) <: \type(javafe.ast.NewArrayExpr);
336 //@ ensures (\result==TagConstants.CONDEXPR) ==> \typeof(this) <: \type(javafe.ast.CondExpr);
337 //@ ensures (\result==TagConstants.INSTANCEOFEXPR) ==> \typeof(this) <: \type(javafe.ast.InstanceOfExpr);
338 //@ ensures (\result==TagConstants.CASTEXPR) ==> \typeof(this) <: \type(javafe.ast.CastExpr);
339 //@ ensures (\result==TagConstants.PARENEXPR) ==> \typeof(this) <: \type(javafe.ast.ParenExpr);
340 //@ ensures (\result==TagConstants.AMBIGUOUSVARIABLEACCESS) ==> \typeof(this) <: \type(javafe.ast.AmbiguousVariableAccess);
341 //@ ensures (\result==TagConstants.VARIABLEACCESS) ==> \typeof(this) <: \type(javafe.ast.VariableAccess);
342 //@ ensures (\result==TagConstants.FIELDACCESS) ==> \typeof(this) <: \type(javafe.ast.FieldAccess);
343 //@ ensures (\result==TagConstants.AMBIGUOUSMETHODINVOCATION) ==> \typeof(this) <: \type(javafe.ast.AmbiguousMethodInvocation);
344 //@ ensures (\result==TagConstants.METHODINVOCATION) ==> \typeof(this) <: \type(javafe.ast.MethodInvocation);
345 //@ ensures (\result==TagConstants.CLASSLITERAL) ==> \typeof(this) <: \type(javafe.ast.ClassLiteral);
346 //@ ensures (\result==TagConstants.EXPROBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.ExprObjectDesignator);
347 //@ ensures (\result==TagConstants.TYPEOBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.TypeObjectDesignator);
348 //@ ensures (\result==TagConstants.SUPEROBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.SuperObjectDesignator);
349 //@ ensures (\result==TagConstants.ERRORTYPE) ==> \typeof(this) <: \type(javafe.ast.ErrorType);
350 //@ ensures (\result==TagConstants.TYPENAME) ==> \typeof(this) <: \type(javafe.ast.TypeName);
351 //@ ensures (\result==TagConstants.ARRAYTYPE) ==> \typeof(this) <: \type(javafe.ast.ArrayType);
352 //@ ensures (\result==TagConstants.SIMPLENAME) ==> \typeof(this) <: \type(javafe.ast.SimpleName);
353 //@ ensures (\result==TagConstants.COMPOUNDNAME) ==> \typeof(this) <: \type(javafe.ast.CompoundName);
354 //@ ensures (\result==TagConstants.OR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
355 //@ ensures (\result==TagConstants.AND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
356 //@ ensures (\result==TagConstants.BITOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
357 //@ ensures (\result==TagConstants.BITXOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
358 //@ ensures (\result==TagConstants.BITAND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
359 //@ ensures (\result==TagConstants.NE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
360 //@ ensures (\result==TagConstants.EQ) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
361 //@ ensures (\result==TagConstants.GE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
362 //@ ensures (\result==TagConstants.GT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
363 //@ ensures (\result==TagConstants.LE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
364 //@ ensures (\result==TagConstants.LT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
365 //@ ensures (\result==TagConstants.LSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
366 //@ ensures (\result==TagConstants.RSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
367 //@ ensures (\result==TagConstants.URSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
368 //@ ensures (\result==TagConstants.ADD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
369 //@ ensures (\result==TagConstants.SUB) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
370 //@ ensures (\result==TagConstants.DIV) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
371 //@ ensures (\result==TagConstants.MOD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
372 //@ ensures (\result==TagConstants.STAR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
373 //@ ensures (\result==TagConstants.ASSIGN) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
374 //@ ensures (\result==TagConstants.ASGMUL) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
375 //@ ensures (\result==TagConstants.ASGDIV) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
376 //@ ensures (\result==TagConstants.ASGREM) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
377 //@ ensures (\result==TagConstants.ASGADD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
378 //@ ensures (\result==TagConstants.ASGSUB) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
379 //@ ensures (\result==TagConstants.ASGLSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
380 //@ ensures (\result==TagConstants.ASGRSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
381 //@ ensures (\result==TagConstants.ASGURSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
382 //@ ensures (\result==TagConstants.ASGBITAND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
383 //@ ensures (\result==TagConstants.ASGBITOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
384 //@ ensures (\result==TagConstants.ASGBITXOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
385 //@ ensures (\result==TagConstants.UNARYADD) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
386 //@ ensures (\result==TagConstants.UNARYSUB) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
387 //@ ensures (\result==TagConstants.NOT) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
388 //@ ensures (\result==TagConstants.BITNOT) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
389 //@ ensures (\result==TagConstants.INC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
390 //@ ensures (\result==TagConstants.DEC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
391 //@ ensures (\result==TagConstants.POSTFIXINC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
392 //@ ensures (\result==TagConstants.POSTFIXDEC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
393 //@ ensures (\result==TagConstants.BOOLEANTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
394 //@ ensures (\result==TagConstants.INTTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
395 //@ ensures (\result==TagConstants.LONGTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
396 //@ ensures (\result==TagConstants.CHARTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
397 //@ ensures (\result==TagConstants.FLOATTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
398 //@ ensures (\result==TagConstants.DOUBLETYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
399 //@ ensures (\result==TagConstants.VOIDTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
400 //@ ensures (\result==TagConstants.NULLTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
401 //@ ensures (\result==TagConstants.BYTETYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
402 //@ ensures (\result==TagConstants.SHORTTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
403 //@ ensures (\result==TagConstants.BOOLEANLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
404 //@ ensures (\result==TagConstants.INTLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
405 //@ ensures (\result==TagConstants.LONGLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
406 //@ ensures (\result==TagConstants.CHARLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
407 //@ ensures (\result==TagConstants.FLOATLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
408 //@ ensures (\result==TagConstants.DOUBLELIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
409 //@ ensures (\result==TagConstants.STRINGLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
410 //@ ensures (\result==TagConstants.NULLLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
411 public abstract int getTag();
412
413 /** Return a string representation of <code>this</code>.
414 Meant for debugging use only, not for presentation. */
415 public abstract /*@non_null*/ String toString();
416
417 /** Accept a visit from <code>v</code>. This method simply
418 calls the method of <code>v</code> corresponding to the
419 allocated type of <code>this</code>, passing <code>this</code>
420 as the argument. See the design patterns book. */
421 //@ requires v != null;
422 public abstract void accept(Visitor v);
423
424 //@ requires v != null;
425 //@ ensures \result != null;
426 public abstract Object accept(VisitorArgResult v, Object o);
427
428 public void check() {
429 }
430
431 }