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