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 escjava.ast;
014
015 import java.util.Hashtable;
016 import java.util.Set;
017 import java.util.ArrayList;
018
019 import javafe.ast.*;
020 import javafe.util.Assert;
021 import javafe.util.Location;
022 import escjava.ParsedRoutineSpecs;
023
024 // Convention: unless otherwise noted, integer fields named "loc" refer
025 // to the location of the first character of the syntactic unit
026
027 //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
028 //# VisitorRoot javafe.ast.Visitor
029
030
031 /**
032 * The files in this package extend the AST classes defined in
033 * <code>javafe.ast</code>. The following diagram shows how the new
034 * classes related to the old classes in the class hierarchy:
035 *
036 * <pre>
037 * - ASTNode
038 * - VarInit ()
039 * - Expr ()
040 * + GCExpr
041 * + LabelExpr (Identifier label, Expr expr)
042 * + NaryExpr (int op, Identifier methodName, Expr* exprs)
043 * + QuantifiedExpr (GenericVarDecl* vars, Expr rangeExpr, Expr expr)
044 * + GeneralizedQuantifiedExpr (GenericVarDecl* vars, Expr expr)
045 * // Sum, Product, Max, Min
046 * + NumericalQuantifiedExpr (GenericVarDecl* vars, Expr expr)
047 * // NumOf
048 * + SubstExpr (GenericVarDecl var, Expr val, Expr target)
049 * + TypeExpr (Type type)
050 * + EverythingExpr ()
051 * + LockSetExpr ()
052 * + NotSpecifiedExpr ()
053 * + NothingExpr ()
054 * + StoreRefExpr(Expr,Expr)
055 * + NotModifiedExpr(Expr)
056 * + ResExpr ()
057 * + SetCompExpr(Type type, Type typeBound, Identifier id, Expr e)
058 * + WildRefExpr (Expr expr)
059 * + GuardExpr (Expr expr)
060 * + DefPredLetExpr (DefPred* preds, Expr body)
061 * + DefPredApplExpr (Identifier predId, Expr* args)
062 * + ArrayRangeRefExpr(Expr, Expr, Expr)
063 * - Type ()
064 * - PrimitiveType (tag)
065 * + EscPrimitiveType ()
066 * + GuardedCmd
067 * + SimpleCmd (int cmd) // Skip, Raise
068 * + ExprCmd (int cmd, Expr pred) // Assert, Assume
069 * + AssignCmd (VariableAccess v, Expr rhs)
070 * + GetsCmd ()
071 * + SubGetsCmd (Expr index)
072 * + SubSubGetsCmd (Expr index1, Expr index2)
073 * + RestoreFromCmd ()
074 * + VarInCmd (GenericVarDecl v*, GuardedCmd g)
075 * + DynInstCmd (String s, GuardedCmd g)
076 * + SeqCmd (GuardedCmd cmds*)
077 * + LoopCmd (Condition invariants*, DecreasesInfo decreases*,
078 * LocalVarDecl skolemConstants*, Expr predicates*,
079 * GenericVarDecl tempVars*, GuardedCmd guard, GuardedCmd body)
080 * + CmdCmdCmd (int cmd, GuardedCmd g1, GuardedCmd g2)// Try, Choose
081 * + Call (RoutineDecl rd, Expr* args, TypeDecl scope)
082 * - TypeDeclElem ()
083 * - TypeDeclElemPragma ()
084 * + ExprDeclPragma (Expr expr) // Axiom, ObjectInvariant
085 * + GhostDeclPragma (GhostFieldDecl decl)
086 * + ModelDeclPragma (ModelFieldDecl decl)
087 * + ModelTypePragma (TypeDecl decl)
088 * + NamedExprDeclPragma (Expr target, Expr expr)
089 * + IdExprDeclPragma (Id target, Expr expr)
090 * + ModelMethodDeclPragma (MethodDecl decl)
091 * + ModelConstructorPragma (ConstructorDecl decl)
092 * + StillDeferredDeclPragma (Identifier var)
093 * + DependsPragma (Expr* exprs) // Depends clause
094 * - Stmt ()
095 * - StmtPragma ()
096 * + SimpleStmtPragma () // Unreachable
097 * + ExprStmtPragma (Expr expr, Expr label)
098 * // Assume, Assert, LoopInvariant, LoopPredicate
099 * + SetStmtPragma (Expr target, Expr value)
100 * + SkolemConstantPragma (LocalVarDecl* decl)
101 * - ModifierPragma ()
102 * + SimpleModifierPragma ()
103 * // Uninitialized, Monitored, NonNull, WritableDeferred,
104 * // Helper, \Peer, \ReadOnly, \Rep,
105 * // may_be_null, nullable_by_default, non_null_by_default,
106 * // obs_pure,
107 * // code_java_math, code_safe_math, code_bigint_math,
108 * // spec_java_math, spec_safe_math, spec_bigint_math
109 * + NestedModifierPragma (ArrayList list)
110 * + ExprModifierPragma (Expr expr)
111 * // DefinedIf, Writable, Requires, Pre, Ensures, Post,
112 * // AlsoEnsures, MonitoredBy, Constraint, InvariantFor, Space,
113 * // \Duration, \WorkingSpace,
114 * // \java_math, \safe_math, \bigint_math
115 * + IdentifierModifierPramga (Identifier id)
116 * // IsInitialized
117 * + ReachModifierPragma (Expr expr, Identifier id, StoreRefExpr)
118 * // \Reach
119 * + CondExprModifierPragma (Expr expr, Expr cond)
120 * // Modifies, AlsoModifiers, Assignable, Modifiable
121 * + ModifiesGroupPragma
122 * // Group of Modifies, etc., pragmas from one spec case
123 * + MapsExprModifierPragma (Identifier id, Expr mapsexpr, Expr expr)
124 * // maps
125 * + VarExprModifierPragma (GenericVarDecl arg, Expr expr)
126 * // Exsures, AlsoExsures, Signals, AlsoSignals
127 * + ModelProgramModifierPragma()
128 * + VarDeclModifierPragma (LocalVarDecl decl)
129 * - LexicalPragma ()
130 * + NowarnPragma (Identifier* checks)
131 * + ImportPragma (ImportDecl decl)
132 * + RefinePragma (String filename)
133 * + Spec (MethodDecl md, Expr* targets, Hashtable preVarMap,
134 * Condition* pre, Condition* post)
135 * + Condition (int label, Expr pred)
136 * + DefPred (Identifier predId, GenericVarDecl* args, Expr body)
137 * + DecreasesInfo (Expr f, VariableAccess fOld)
138 * </pre>
139 *
140 * <p> (Classes with a <code>-</code> next to them are defined in
141 * <code>javafe.ast</code>; classes with a <code>+</code> are defined
142 * in this package. </p>
143 *
144 * <p> (P.S. Ignore the stuff that appears below; the only purpose of
145 * this class is to contain the above overview.) </p>
146 *
147 */
148
149 public abstract class AnOverview extends ASTNode
150 {
151
152 // Generated boilerplate constructors:
153
154 protected AnOverview() {
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 /*@non_null*/ 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 }