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