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