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    //// Pragmas
032    
033    public class ExprDeclPragma extends TypeDeclElemPragma
034    {
035      public int tag;
036    
037      public /*@ non_null @*/ Expr expr;
038    
039      public int modifiers;
040    
041      public int loc;
042    
043    
044      public final int getTag() { return tag; }
045      public int getModifiers() { return modifiers; }
046    
047      private void postCheck() {
048        boolean goodtag =
049          (tag == TagConstants.AXIOM || 
050           tag == TagConstants.INVARIANT );
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      public boolean isRedundant() { return redundant; }
062      public void setRedundant(boolean v) { redundant = v; }
063    
064    
065    // Generated boilerplate constructors:
066    
067      //@ ensures this.tag == tag;
068      //@ ensures this.expr == expr;
069      //@ ensures this.modifiers == modifiers;
070      //@ ensures this.loc == loc;
071      protected ExprDeclPragma(int tag, /*@ non_null @*/ Expr expr, int modifiers, int loc) {
072         this.tag = tag;
073         this.expr = expr;
074         this.modifiers = modifiers;
075         this.loc = loc;
076      }
077    
078    // Generated boilerplate methods:
079    
080      public final int childCount() {
081         return 1;
082      }
083    
084      public final Object childAt(int index) {
085              /*throws IndexOutOfBoundsException*/
086         if (index < 0)
087            throw new IndexOutOfBoundsException("AST child index " + index);
088         int indexPre = index;
089    
090         int sz;
091    
092         if (index == 0) return this.expr;
093         else index--;
094    
095         throw new IndexOutOfBoundsException("AST child index " + indexPre);
096      }   //@ nowarn Exception;
097    
098      public final /*@non_null*/String toString() {
099         return "[ExprDeclPragma"
100            + " tag = " + this.tag
101            + " expr = " + this.expr
102            + " modifiers = " + this.modifiers
103            + " loc = " + this.loc
104            + "]";
105      }
106    
107      public final void accept(javafe.ast.Visitor v) { 
108        if (v instanceof Visitor) ((Visitor)v).visitExprDeclPragma(this);
109      }
110    
111      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
112        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitExprDeclPragma(this, o); else return null;
113      }
114    
115      public void check() {
116         this.expr.check();
117         postCheck();
118      }
119    
120      //@ ensures \result != null;
121      public static ExprDeclPragma make(int tag, /*@ non_null @*/ Expr expr, int modifiers, int loc) {
122         ExprDeclPragma result = new ExprDeclPragma(tag, expr, modifiers, loc);
123         return result;
124      }
125    }