    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    }