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