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    }