001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    /* IF THIS IS A JAVA FILE, DO NOT EDIT IT!  
004    
005       Most Java files in this directory which are part of the Javafe AST
006       are automatically generated using the astgen comment (see
007       ESCTools/Javafe/astgen) from the input file 'hierarchy.h'.  If you
008       wish to modify AST classes or introduce new ones, modify
009       'hierarchy.j.'
010     */
011    
012    package escjava.ast;
013    
014    import java.util.Hashtable;
015    import java.util.Set;
016    import java.util.ArrayList;
017    
018    import javafe.ast.*;
019    import javafe.util.Assert;
020    import javafe.util.Location;
021    import escjava.ParsedRoutineSpecs;
022    
023    // Convention: unless otherwise noted, integer fields named "loc" refer
024    // to the location of the first character of the syntactic unit
025    
026    //# TagBase javafe.tc.TagConstants.LAST_TAG + 1
027    //# VisitorRoot javafe.ast.Visitor
028    
029    
030    public class LoopCmd extends GuardedCmd
031    {
032      public int locStart;
033    
034      public int locEnd;
035    
036      public int locHotspot;
037    
038      public /*@ non_null @*/ Hashtable oldmap;
039    
040      public /*@ non_null @*/ ConditionVec invariants;
041    
042      public /*@ non_null @*/ DecreasesInfoVec decreases;
043    
044      public /*@ non_null @*/ LocalVarDeclVec skolemConstants;
045    
046      public /*@ non_null @*/ ExprVec predicates;
047    
048      public /*@ non_null @*/ GenericVarDeclVec tempVars;
049    
050      public /*@ non_null @*/ GuardedCmd guard;
051    
052      public /*@ non_null @*/ GuardedCmd body;
053    
054    
055      public GuardedCmd desugared;
056      
057      public int getStartLoc() { return locStart; }
058      public int getEndLoc() { return locEnd; }
059    
060    
061    // Generated boilerplate constructors:
062    
063      /**
064       * Construct a raw LoopCmd whose class invariant(s) have not
065       * yet been established.  It is the caller's job to
066       * initialize the returned node's fields so that any
067       * class invariants hold.
068       */
069      //@ requires I_will_establish_invariants_afterwards;
070      protected LoopCmd() {}    //@ nowarn Invariant,NonNullInit;
071    
072    
073    // Generated boilerplate methods:
074    
075      public final int childCount() {
076         int sz = 0;
077         if (this.invariants != null) sz += this.invariants.size();
078         if (this.decreases != null) sz += this.decreases.size();
079         if (this.skolemConstants != null) sz += this.skolemConstants.size();
080         if (this.predicates != null) sz += this.predicates.size();
081         if (this.tempVars != null) sz += this.tempVars.size();
082         return sz + 3;
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.oldmap;
094         else index--;
095    
096         sz = (this.invariants == null ? 0 : this.invariants.size());
097         if (0 <= index && index < sz)
098            return this.invariants.elementAt(index);
099         else index -= sz;
100    
101         sz = (this.decreases == null ? 0 : this.decreases.size());
102         if (0 <= index && index < sz)
103            return this.decreases.elementAt(index);
104         else index -= sz;
105    
106         sz = (this.skolemConstants == null ? 0 : this.skolemConstants.size());
107         if (0 <= index && index < sz)
108            return this.skolemConstants.elementAt(index);
109         else index -= sz;
110    
111         sz = (this.predicates == null ? 0 : this.predicates.size());
112         if (0 <= index && index < sz)
113            return this.predicates.elementAt(index);
114         else index -= sz;
115    
116         sz = (this.tempVars == null ? 0 : this.tempVars.size());
117         if (0 <= index && index < sz)
118            return this.tempVars.elementAt(index);
119         else index -= sz;
120    
121         if (index == 0) return this.guard;
122         else index--;
123    
124         if (index == 0) return this.body;
125         else index--;
126    
127         throw new IndexOutOfBoundsException("AST child index " + indexPre);
128      }   //@ nowarn Exception;
129    
130      public final String toString() {
131         return "[LoopCmd"
132            + " locStart = " + this.locStart
133            + " locEnd = " + this.locEnd
134            + " locHotspot = " + this.locHotspot
135            + " oldmap = " + this.oldmap
136            + " invariants = " + this.invariants
137            + " decreases = " + this.decreases
138            + " skolemConstants = " + this.skolemConstants
139            + " predicates = " + this.predicates
140            + " tempVars = " + this.tempVars
141            + " guard = " + this.guard
142            + " body = " + this.body
143            + "]";
144      }
145    
146      public final int getTag() {
147         return TagConstants.LOOPCMD;
148      }
149    
150      public final void accept(javafe.ast.Visitor v) { 
151        if (v instanceof Visitor) ((Visitor)v).visitLoopCmd(this);
152      }
153    
154      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
155        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitLoopCmd(this, o); else return null;
156      }
157    
158      public void check() {
159         super.check();
160         if (this.oldmap == null) throw new RuntimeException();
161         for(int i = 0; i < this.invariants.size(); i++)
162            this.invariants.elementAt(i).check();
163         for(int i = 0; i < this.decreases.size(); i++)
164            this.decreases.elementAt(i).check();
165         for(int i = 0; i < this.skolemConstants.size(); i++)
166            this.skolemConstants.elementAt(i).check();
167         for(int i = 0; i < this.predicates.size(); i++)
168            this.predicates.elementAt(i).check();
169         for(int i = 0; i < this.tempVars.size(); i++)
170            this.tempVars.elementAt(i).check();
171         this.guard.check();
172         this.body.check();
173      }
174    
175      //@ ensures \result != null;
176      public static LoopCmd make(int locStart, int locEnd, int locHotspot, /*@ non_null @*/ Hashtable oldmap, /*@ non_null @*/ ConditionVec invariants, /*@ non_null @*/ DecreasesInfoVec decreases, /*@ non_null @*/ LocalVarDeclVec skolemConstants, /*@ non_null @*/ ExprVec predicates, /*@ non_null @*/ GenericVarDeclVec tempVars, /*@ non_null @*/ GuardedCmd guard, /*@ non_null @*/ GuardedCmd body) {
177         //@ set I_will_establish_invariants_afterwards = true;
178         LoopCmd result = new LoopCmd();
179         result.locStart = locStart;
180         result.locEnd = locEnd;
181         result.locHotspot = locHotspot;
182         result.oldmap = oldmap;
183         result.invariants = invariants;
184         result.decreases = decreases;
185         result.skolemConstants = skolemConstants;
186         result.predicates = predicates;
187         result.tempVars = tempVars;
188         result.guard = guard;
189         result.body = body;
190         return result;
191      }
192    }