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