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 }