001    // -*- mode: java -*-
002    /* Copyright 2000, 2001, Compaq Computer Corporation */
003    
004    /* IF THIS IS A JAVA FILE, DO NOT EDIT IT!  
005    
006       Most Java files in this directory which are part of the Javafe AST
007       are automatically generated using the astgen comment (see
008       ESCTools/Javafe/astgen) from the input file 'hierarchy.h'.  If you
009       wish to modify AST classes or introduce new ones, modify
010       'hierarchy.j.'
011     */
012    
013    package escjava.ast;
014    
015    import java.util.Hashtable;
016    import java.util.Set;
017    import java.util.ArrayList;
018    
019    import javafe.ast.*;
020    import javafe.util.Assert;
021    import javafe.util.Location;
022    import escjava.ParsedRoutineSpecs;
023    
024    // Convention: unless otherwise noted, integer fields named "loc" refer
025    // to the location of the first character of the syntactic unit
026    
027    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
028    //# VisitorRoot javafe.ast.Visitor
029    
030    
031    public class CondExprModifierPragma extends ModifierPragma
032    {
033        // Extended to support JML
034    
035        public int tag;
036    
037        public /*@ non_null @*/ Expr expr;
038    
039        public int loc;
040    
041        public /*@ non_null @*/ Expr cond;
042    
043    
044        public final int getTag() { return tag; }
045    
046        private void postCheck() {
047            boolean goodtag = (tag == TagConstants.ALSO_MODIFIES ||
048                               tag == TagConstants.MODIFIES);
049            boolean isJMLExprModifier = isJMLExprModifier();
050            Assert.notFalse(goodtag || isJMLExprModifier);
051        }
052    
053        private boolean isJMLExprModifier() {
054            return (tag == TagConstants.ASSIGNABLE ||
055                    tag == TagConstants.MODIFIABLE);
056        }
057    
058        //@ public represents startLoc <- loc;
059        public /*@ pure @*/ int getStartLoc() { return loc; }
060        /*@ also
061          @ public normal_behavior
062          @ ensures \result == cond.getEndLoc();
063          @*/
064        public /*@ pure @*/ int getEndLoc() { return cond.getEndLoc(); }
065    
066    
067    // Generated boilerplate constructors:
068    
069        //@ ensures this.tag == tag;
070        //@ ensures this.expr == expr;
071        //@ ensures this.loc == loc;
072        //@ ensures this.cond == cond;
073        protected CondExprModifierPragma(int tag, /*@ non_null @*/ Expr expr, int loc, /*@ non_null @*/ Expr cond) {
074           this.tag = tag;
075           this.expr = expr;
076           this.loc = loc;
077           this.cond = cond;
078        }
079    
080    // Generated boilerplate methods:
081    
082        public final int childCount() {
083           return 2;
084        }
085    
086        public final Object childAt(int index) {
087                /*throws IndexOutOfBoundsException*/
088           if (index < 0)
089              throw new IndexOutOfBoundsException("AST child index " + index);
090           int indexPre = index;
091    
092           int sz;
093    
094           if (index == 0) return this.expr;
095           else index--;
096    
097           if (index == 0) return this.cond;
098           else index--;
099    
100           throw new IndexOutOfBoundsException("AST child index " + indexPre);
101        }   //@ nowarn Exception;
102    
103        public final /*@non_null*/String toString() {
104           return "[CondExprModifierPragma"
105              + " tag = " + this.tag
106              + " expr = " + this.expr
107              + " loc = " + this.loc
108              + " cond = " + this.cond
109              + "]";
110        }
111    
112        public final void accept(javafe.ast.Visitor v) { 
113            if (v instanceof Visitor) ((Visitor)v).visitCondExprModifierPragma(this);
114        }
115    
116        public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
117            if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitCondExprModifierPragma(this, o); else return null;
118        }
119    
120        public void check() {
121           this.expr.check();
122           this.cond.check();
123           postCheck();
124        }
125    
126        //@ ensures \result != null;
127        public static CondExprModifierPragma make(int tag, /*@ non_null @*/ Expr expr, int loc, /*@ non_null @*/ Expr cond) {
128           CondExprModifierPragma result = new CondExprModifierPragma(tag, expr, loc, cond);
129           return result;
130        }
131    }