    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    public class MapsExprModifierPragma extends ModifierPragma
    031      implements javafe.ast.IdPragma
    032    {
    033        // Extended to support JML
    034
    035        public int tag;
    036
    037        public /*@ non_null @*/ Identifier id;
    038
    039        public /*@ non_null @*/ Expr mapsexpr;
    040
    041        public int loc;
    042
    043        public /*@ non_null @*/ Expr expr;
    044
    045
    046        public final int getTag() { return tag; }
    047
    048        private void postCheck() {
    049            boolean goodtag = (tag == TagConstants.MAPS);
    050            Assert.notFalse(goodtag);
    051        }
    052
    053        public Identifier id() { return id; }
    054        public int getStartLoc() { return loc; }
    055        public int getEndLoc() { return expr.getEndLoc(); }
    056
    057
    058    // Generated boilerplate constructors:
    059
    060        /**
    061         * Construct a raw MapsExprModifierPragma whose class invariant(s) have not
    062         * yet been established.  It is the caller's job to
    063         * initialize the returned node's fields so that any
    064         * class invariants hold.
    065         */
    066        //@ requires I_will_establish_invariants_afterwards;
    067        protected MapsExprModifierPragma() {}    //@ nowarn Invariant,NonNullInit;
    068
    069
    070    // Generated boilerplate methods:
    071
    072        public final int childCount() {
    073           return 3;
    074        }
    075
    076        public final Object childAt(int index) {
    077                /*throws IndexOutOfBoundsException*/
    078           if (index < 0)
    079              throw new IndexOutOfBoundsException("AST child index " + index);
    080           int indexPre = index;
    081
    082           int sz;
    083
    084           if (index == 0) return this.id;
    085           else index--;
    086
    087           if (index == 0) return this.mapsexpr;
    088           else index--;
    089
    090           if (index == 0) return this.expr;
    091           else index--;
    092
    093           throw new IndexOutOfBoundsException("AST child index " + indexPre);
    094        }   //@ nowarn Exception;
    095
    096        public final String toString() {
    097           return "[MapsExprModifierPragma"
    098              + " tag = " + this.tag
    099              + " id = " + this.id
    100              + " mapsexpr = " + this.mapsexpr
    101              + " loc = " + this.loc
    102              + " expr = " + this.expr
    103              + "]";
    104        }
    105
    106        public final void accept(javafe.ast.Visitor v) {
    107            if (v instanceof Visitor) ((Visitor)v).visitMapsExprModifierPragma(this);
    108        }
    109
    110        public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
    111            if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitMapsExprModifierPragma(this, o); else return null;
    112        }
    113
    114        public void check() {
    115           this.id.check();
    116           this.mapsexpr.check();
    117           this.expr.check();
    118           postCheck();
    119        }
    120
    121        //@ ensures \result != null;
    122        public static MapsExprModifierPragma make(int tag, /*@ non_null @*/ Identifier id, /*@ non_null @*/ Expr mapsexpr, int loc, /*@ non_null @*/ Expr expr) {
    123           //@ set I_will_establish_invariants_afterwards = true;
    124           MapsExprModifierPragma result = new MapsExprModifierPragma();
    125           result.tag = tag;
    126           result.id = id;
    127           result.mapsexpr = mapsexpr;
    128           result.loc = loc;
    129           result.expr = expr;
    130           return result;
    131        }
    132    }