    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
    030    /**
    031     * The files in this package extend the AST classes defined in
    032     * <code>javafe.ast</code>.  The following diagram shows how the new
    033     * classes related to the old classes in the class hierarchy:
    034     *
    035     * <pre>
    036     * - ASTNode
    037     *    - VarInit ()
    038     *       - Expr ()
    039     *         + GCExpr
    040     *           + LabelExpr (Identifier label, Expr expr)
    041     *           + NaryExpr (int op, Identifier methodName, Expr* exprs)
    042     *           + QuantifiedExpr (GenericVarDecl* vars, Expr rangeExpr, Expr expr)
    043     *           + GeneralizedQuantifiedExpr (GenericVarDecl* vars, Expr expr)
    044     *                // Sum, Product, Max, Min
    045     *           + NumericalQuantifiedExpr (GenericVarDecl* vars, Expr expr)
    046     *                // NumOf
    047     *           + SubstExpr (GenericVarDecl var, Expr val, Expr target)
    048     *           + TypeExpr (Type type)
    049     *         + EverythingExpr ()
    050     *         + LockSetExpr ()
    051     *         + NotSpecifiedExpr ()
    052     *         + NothingExpr ()
    053     *         + StoreRefExpr(Expr,Expr)
    054     *         + NotModifiedExpr(Expr)
    055     *         + ResExpr ()
    056     *         + SetCompExpr(Type type, Type typeBound, Identifier id, Expr e)
    057     *         + WildRefExpr (Expr expr)
    058     *         + GuardExpr (Expr expr)
    059     *         + DefPredLetExpr (DefPred* preds, Expr body)
    060     *         + DefPredApplExpr (Identifier predId, Expr* args)
    061     *         + ArrayRangeRefExpr(Expr, Expr, Expr)
    062     *    + GuardedCmd
    063     *      + SimpleCmd (int cmd) // Skip, Raise
    064     *      + ExprCmd (int cmd, Expr pred) // Assert, Assume
    065     *      + AssignCmd (VariableAccess v, Expr rhs)
    066     *        + GetsCmd ()
    067     *        + SubGetsCmd (Expr index)
    068     *        + SubSubGetsCmd (Expr index1, Expr index2)
    069     *        + RestoreFromCmd ()
    070     *      + VarInCmd (GenericVarDecl v*, GuardedCmd g)
    071     *      + DynInstCmd (String s, GuardedCmd g)
    072     *      + SeqCmd (GuardedCmd cmds*)
    073     *      + LoopCmd (Condition invariants*, DecreasesInfo decreases*,
    074     *                 LocalVarDecl skolemConstants*, Expr predicates*,
    075     *                 GenericVarDecl tempVars*, GuardedCmd guard, GuardedCmd body)
    076     *      + CmdCmdCmd (int cmd, GuardedCmd g1, GuardedCmd g2)// Try, Choose
    077     *      + Call (RoutineDecl rd, Expr* args, TypeDecl scope)
    078     *    - TypeDeclElem ()
    079     *       - TypeDeclElemPragma ()
    080     *         + ExprDeclPragma (Expr expr) // Axiom, ObjectInvariant
    081     *         + GhostDeclPragma (GhostFieldDecl decl)
    082     *         + ModelDeclPragma (ModelFieldDecl decl)
    083     *         + ModelTypePragma (TypeDecl decl)
    084     *         + NamedExprDeclPragma (Expr target, Expr expr)
    085     *         + IdExprDeclPragma (Id target, Expr expr)
    086     *         + ModelMethodDeclPragma (MethodDecl decl)
    087     *         + ModelConstructorPragma (ConstructorDecl decl)
    088     *         + StillDeferredDeclPragma (Identifier var)
    089     *         + DependsPragma (Expr* exprs) // Depends clause
    090     *    - Stmt ()
    091     *       - StmtPragma ()
    092     *         + SimpleStmtPragma () // Unreachable
    093     *         + ExprStmtPragma (Expr expr, Expr label)
    094     *             // Assume, Assert, LoopInvariant, LoopPredicate
    095     *         + SetStmtPragma (Expr target, Expr value)
    096     *         + SkolemConstantPragma (LocalVarDecl* decl)
    097     *    - ModifierPragma ()
    098     *         + SimpleModifierPragma ()
    099     *                   // Uninitialized, Monitored, NonNull, WritableDeferred,
    100     *                   // Helper, \Peer, \ReadOnly, \Rep,
    101     *                   // may_be_null, null_ref_by_default, non_null_ref_by_default,
    102     *                   // obs_pure,
    103     *                   // code_java_math, code_safe_math, code_bigint_math,
    104     *                   // spec_java_math, spec_safe_math, spec_bigint_math
    105     *         + NestedModifierPragma (ArrayList list)
    106     *         + ExprModifierPragma (Expr expr)
    107     *                   // DefinedIf, Writable, Requires, Pre, Ensures, Post,
    108     *                   // AlsoEnsures, MonitoredBy, Constraint, InvariantFor, Space,
    109     *                   // \Duration, \WorkingSpace,
    110     *                   // \java_math, \safe_math, \bigint_math
    111     *         + IdentifierModifierPramga (Identifier id)
    112     *                   // IsInitialized
    113     *         + ReachModifierPragma (Expr expr, Identifier id, StoreRefExpr)
    114     *                   // \Reach
    115     *         + CondExprModifierPragma (Expr expr, Expr cond)
    116     *                   // Modifies, AlsoModifiers, Assignable, Modifiable
    117     *         + ModifiesGroupPragma
    118     *                   // Group of Modifies, etc., pragmas from one spec case
    119     *         + MapsExprModifierPragma (Identifier id, Expr mapsexpr, Expr expr)
    120     *                   // maps
    121     *         + VarExprModifierPragma (GenericVarDecl arg, Expr expr)
    122     *                   // Exsures, AlsoExsures, Signals, AlsoSignals
    123     *         + ModelProgramModifierPragma()
    124     *         + VarDeclModifierPragma (LocalVarDecl decl)
    125     *    - LexicalPragma ()
    126     *      + NowarnPragma (Identifier* checks)
    127     *      + ImportPragma (ImportDecl decl)
    128     *      + RefinePragma (String filename)
    129     *    + Spec (MethodDecl md, Expr* targets, Hashtable preVarMap,
    130     *            Condition* pre, Condition* post)
    131     *    + Condition(int label, Expr pred)
    132     *    + DefPred (Identifier predId, GenericVarDecl* args, Expr body)
    133     * </pre>
    134     *
    135     * <p> (Classes with a <code>-</code> next to them are defined in
    136     * <code>javafe.ast</code>; classes with a <code>+</code> are defined
    137     * in this package. </p>
    138     *
    139     * <p> (P.S. Ignore the stuff that appears below; the only purpose of
    140     * this class is to contain the above overview.) </p>
    141     *
    142     */
    143
    144    public abstract class AnOverview extends ASTNode
    145    {
    146
    147    // Generated boilerplate constructors:
    148
    149       /**
    150        * Construct a raw AnOverview whose class invariant(s) have not
    151        * yet been established.  It is the caller's job to
    152        * initialize the returned node's fields so that any
    153        * class invariants hold.
    154        */
    155
    156
    157
    158    // Generated boilerplate methods:
    159
    160       /** Return the number of children a node has. */
    161       public abstract int childCount();
    162
    163       /** Return the first-but-ith child of a node. */
    164       public abstract Object childAt(int i);
    165
    166       /** Return the tag of a node. */
    167       public abstract int getTag();
    168
    169       /** Return a string representation of <code>this</code>.
    170       Meant for debugging use only, not for presentation. */
    171       public abstract String toString();
    172
    173       /** Accept a visit from <code>v</code>.  This method simply
    174       calls the method of <code>v</code> corresponding to the
    175       allocated type of <code>this</code>, passing <code>this</code>
    176       as the argument.  See the design patterns book. */
    177       public abstract void accept(javafe.ast.Visitor v);
    178
    179    public abstract Object accept(javafe.ast.VisitorArgResult v, Object o);
    180
    181       public void check() {
    182       }
    183
    184    }