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