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