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 SkolemConstantPragma extends StmtPragma
032    {
033      public /*@ non_null @*/ LocalVarDeclVec decls;
034    
035      public int sloc;
036    
037      public int eloc;
038    
039    
040      //@ public represents startLoc <- sloc;
041      public /*@ pure @*/ int getStartLoc() { return sloc; }
042      /*@ also
043        @ public normal_behavior
044        @ ensures \result == eloc;
045        @*/
046      public /*@ pure @*/ int getEndLoc() { return eloc; }
047    
048    
049    // Generated boilerplate constructors:
050    
051      //@ ensures this.decls == decls;
052      //@ ensures this.sloc == sloc;
053      //@ ensures this.eloc == eloc;
054      protected SkolemConstantPragma(/*@ non_null @*/ LocalVarDeclVec decls, int sloc, int eloc) {
055         this.decls = decls;
056         this.sloc = sloc;
057         this.eloc = eloc;
058      }
059    
060    // Generated boilerplate methods:
061    
062      public final int childCount() {
063         int sz = 0;
064         if (this.decls != null) sz += this.decls.size();
065         return sz + 0;
066      }
067    
068      public final Object childAt(int index) {
069              /*throws IndexOutOfBoundsException*/
070         if (index < 0)
071            throw new IndexOutOfBoundsException("AST child index " + index);
072         int indexPre = index;
073    
074         int sz;
075    
076         sz = (this.decls == null ? 0 : this.decls.size());
077         if (0 <= index && index < sz)
078            return this.decls.elementAt(index);
079         else index -= sz;
080    
081         throw new IndexOutOfBoundsException("AST child index " + indexPre);
082      }   //@ nowarn Exception;
083    
084      public final /*@non_null*/String toString() {
085         return "[SkolemConstantPragma"
086            + " decls = " + this.decls
087            + " sloc = " + this.sloc
088            + " eloc = " + this.eloc
089            + "]";
090      }
091    
092      public final int getTag() {
093         return TagConstants.SKOLEMCONSTANTPRAGMA;
094      }
095    
096      public final void accept(javafe.ast.Visitor v) { 
097        if (v instanceof Visitor) ((Visitor)v).visitSkolemConstantPragma(this);
098      }
099    
100      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
101        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitSkolemConstantPragma(this, o); else return null;
102      }
103    
104      public void check() {
105         for(int i = 0; i < this.decls.size(); i++)
106            this.decls.elementAt(i).check();
107      }
108    
109      //@ ensures \result != null;
110      public static SkolemConstantPragma make(/*@ non_null @*/ LocalVarDeclVec decls, int sloc, int eloc) {
111         SkolemConstantPragma result = new SkolemConstantPragma(decls, sloc, eloc);
112         return result;
113      }
114    }