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