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 public abstract class Visitor extends javafe.ast.Visitor { 030 //@ requires x != null; 031 public abstract void visitAnOverview(AnOverview x); 032 033 //@ requires x != null; 034 public abstract void visitGCExpr(GCExpr x); 035 036 //@ requires x != null; 037 public void visitNaryExpr(NaryExpr x) { 038 visitGCExpr(x); 039 } 040 041 //@ requires x != null; 042 public void visitQuantifiedExpr(QuantifiedExpr x) { 043 visitGCExpr(x); 044 } 045 046 //@ requires x != null; 047 public void visitGeneralizedQuantifiedExpr(GeneralizedQuantifiedExpr x) { 048 visitGCExpr(x); 049 } 050 051 //@ requires x != null; 052 public void visitNumericalQuantifiedExpr(NumericalQuantifiedExpr x) { 053 visitGCExpr(x); 054 } 055 056 //@ requires x != null; 057 public void visitSubstExpr(SubstExpr x) { 058 visitGCExpr(x); 059 } 060 061 //@ requires x != null; 062 public void visitTypeExpr(TypeExpr x) { 063 visitGCExpr(x); 064 } 065 066 //@ requires x != null; 067 public void visitLabelExpr(LabelExpr x) { 068 visitGCExpr(x); 069 } 070 071 //@ requires x != null; 072 public abstract void visitWildRefExpr(WildRefExpr x); 073 074 //@ requires x != null; 075 public abstract void visitGuardExpr(GuardExpr x); 076 077 //@ requires x != null; 078 public abstract void visitResExpr(ResExpr x); 079 080 //@ requires x != null; 081 public abstract void visitSetCompExpr(SetCompExpr x); 082 083 //@ requires x != null; 084 public abstract void visitLockSetExpr(LockSetExpr x); 085 086 //@ requires x != null; 087 public abstract void visitEverythingExpr(EverythingExpr x); 088 089 //@ requires x != null; 090 public abstract void visitNothingExpr(NothingExpr x); 091 092 //@ requires x != null; 093 public abstract void visitNotSpecifiedExpr(NotSpecifiedExpr x); 094 095 //@ requires x != null; 096 public abstract void visitNotModifiedExpr(NotModifiedExpr x); 097 098 //@ requires x != null; 099 public abstract void visitArrayRangeRefExpr(ArrayRangeRefExpr x); 100 101 //@ requires x != null; 102 public abstract void visitDefPredLetExpr(DefPredLetExpr x); 103 104 //@ requires x != null; 105 public abstract void visitDefPredApplExpr(DefPredApplExpr x); 106 107 //@ requires x != null; 108 public abstract void visitGuardedCmd(GuardedCmd x); 109 110 //@ requires x != null; 111 public void visitSimpleCmd(SimpleCmd x) { 112 visitGuardedCmd(x); 113 } 114 115 //@ requires x != null; 116 public void visitExprCmd(ExprCmd x) { 117 visitGuardedCmd(x); 118 } 119 120 //@ requires x != null; 121 public void visitAssignCmd(AssignCmd x) { 122 visitGuardedCmd(x); 123 } 124 125 //@ requires x != null; 126 public void visitGetsCmd(GetsCmd x) { 127 visitAssignCmd(x); 128 } 129 130 //@ requires x != null; 131 public void visitSubGetsCmd(SubGetsCmd x) { 132 visitAssignCmd(x); 133 } 134 135 //@ requires x != null; 136 public void visitSubSubGetsCmd(SubSubGetsCmd x) { 137 visitAssignCmd(x); 138 } 139 140 //@ requires x != null; 141 public void visitRestoreFromCmd(RestoreFromCmd x) { 142 visitAssignCmd(x); 143 } 144 145 //@ requires x != null; 146 public void visitVarInCmd(VarInCmd x) { 147 visitGuardedCmd(x); 148 } 149 150 //@ requires x != null; 151 public void visitDynInstCmd(DynInstCmd x) { 152 visitGuardedCmd(x); 153 } 154 155 //@ requires x != null; 156 public void visitSeqCmd(SeqCmd x) { 157 visitGuardedCmd(x); 158 } 159 160 //@ requires x != null; 161 public void visitLoopCmd(LoopCmd x) { 162 visitGuardedCmd(x); 163 } 164 165 //@ requires x != null; 166 public void visitCmdCmdCmd(CmdCmdCmd x) { 167 visitGuardedCmd(x); 168 } 169 170 //@ requires x != null; 171 public void visitCall(Call x) { 172 visitGuardedCmd(x); 173 } 174 175 //@ requires x != null; 176 public abstract void visitExprDeclPragma(ExprDeclPragma x); 177 178 //@ requires x != null; 179 public abstract void visitIdExprDeclPragma(IdExprDeclPragma x); 180 181 //@ requires x != null; 182 public abstract void visitNamedExprDeclPragma(NamedExprDeclPragma x); 183 184 //@ requires x != null; 185 public abstract void visitModelDeclPragma(ModelDeclPragma x); 186 187 //@ requires x != null; 188 public abstract void visitDependsPragma(DependsPragma x); 189 190 //@ requires x != null; 191 public abstract void visitModelConstructorDeclPragma(ModelConstructorDeclPragma x); 192 193 //@ requires x != null; 194 public abstract void visitModelTypePragma(ModelTypePragma x); 195 196 //@ requires x != null; 197 public abstract void visitModelMethodDeclPragma(ModelMethodDeclPragma x); 198 199 //@ requires x != null; 200 public abstract void visitGhostDeclPragma(GhostDeclPragma x); 201 202 //@ requires x != null; 203 public abstract void visitStillDeferredDeclPragma(StillDeferredDeclPragma x); 204 205 //@ requires x != null; 206 public abstract void visitSimpleStmtPragma(SimpleStmtPragma x); 207 208 //@ requires x != null; 209 public abstract void visitIdentifierModifierPragma(IdentifierModifierPragma x); 210 211 //@ requires x != null; 212 public abstract void visitExprStmtPragma(ExprStmtPragma x); 213 214 //@ requires x != null; 215 public abstract void visitSetStmtPragma(SetStmtPragma x); 216 217 //@ requires x != null; 218 public abstract void visitSkolemConstantPragma(SkolemConstantPragma x); 219 220 //@ requires x != null; 221 public abstract void visitModelProgamModifierPragma(ModelProgamModifierPragma x); 222 223 //@ requires x != null; 224 public abstract void visitNestedModifierPragma(NestedModifierPragma x); 225 226 //@ requires x != null; 227 public abstract void visitParsedSpecs(ParsedSpecs x); 228 229 //@ requires x != null; 230 public abstract void visitSimpleModifierPragma(SimpleModifierPragma x); 231 232 //@ requires x != null; 233 public abstract void visitExprModifierPragma(ExprModifierPragma x); 234 235 //@ requires x != null; 236 public abstract void visitModifiesGroupPragma(ModifiesGroupPragma x); 237 238 //@ requires x != null; 239 public abstract void visitCondExprModifierPragma(CondExprModifierPragma x); 240 241 //@ requires x != null; 242 public abstract void visitMapsExprModifierPragma(MapsExprModifierPragma x); 243 244 //@ requires x != null; 245 public abstract void visitReachModifierPragma(ReachModifierPragma x); 246 247 //@ requires x != null; 248 public abstract void visitVarDeclModifierPragma(VarDeclModifierPragma x); 249 250 //@ requires x != null; 251 public abstract void visitVarExprModifierPragma(VarExprModifierPragma x); 252 253 //@ requires x != null; 254 public abstract void visitNowarnPragma(NowarnPragma x); 255 256 //@ requires x != null; 257 public abstract void visitImportPragma(ImportPragma x); 258 259 //@ requires x != null; 260 public abstract void visitRefinePragma(RefinePragma x); 261 262 //@ requires x != null; 263 public abstract void visitSpec(Spec x); 264 265 //@ requires x != null; 266 public abstract void visitCondition(Condition x); 267 268 //@ requires x != null; 269 public abstract void visitDefPred(DefPred x); 270 271 }