    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    }