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 Spec extends ASTNode
031    {
032      public /*@ non_null @*/ DerivedMethodDecl dmd;
033    
034      public /*@ non_null @*/ ExprVec targets;
035    
036      public /*@ non_null @*/ ExprVec specialTargets;
037    
038      public /*@ non_null @*/ Hashtable preVarMap;
039    
040      public /*@ non_null @*/ ExprVec preAssumptions;
041    
042      public /*@ non_null @*/ ConditionVec pre;
043    
044      public /*@ non_null @*/ ExprVec postAssumptions;
045    
046      public /*@ non_null @*/ ConditionVec post;
047    
048      public boolean modifiesEverything;
049    
050      public /*@ non_null @*/ Set postconditionLocations;
051    
052    
053      public int getStartLoc() { return dmd.original.getStartLoc(); }
054      public int getEndLoc() { return dmd.original.getEndLoc(); }
055    
056    
057    // Generated boilerplate constructors:
058    
059      /**
060       * Construct a raw Spec whose class invariant(s) have not
061       * yet been established.  It is the caller's job to
062       * initialize the returned node's fields so that any
063       * class invariants hold.
064       */
065      //@ requires I_will_establish_invariants_afterwards;
066      protected Spec() {}    //@ nowarn Invariant,NonNullInit;
067    
068    
069    // Generated boilerplate methods:
070    
071      public final int childCount() {
072         int sz = 0;
073         if (this.targets != null) sz += this.targets.size();
074         if (this.specialTargets != null) sz += this.specialTargets.size();
075         if (this.preAssumptions != null) sz += this.preAssumptions.size();
076         if (this.pre != null) sz += this.pre.size();
077         if (this.postAssumptions != null) sz += this.postAssumptions.size();
078         if (this.post != null) sz += this.post.size();
079         return sz + 3;
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.dmd;
091         else index--;
092    
093         sz = (this.targets == null ? 0 : this.targets.size());
094         if (0 <= index && index < sz)
095            return this.targets.elementAt(index);
096         else index -= sz;
097    
098         sz = (this.specialTargets == null ? 0 : this.specialTargets.size());
099         if (0 <= index && index < sz)
100            return this.specialTargets.elementAt(index);
101         else index -= sz;
102    
103         if (index == 0) return this.preVarMap;
104         else index--;
105    
106         sz = (this.preAssumptions == null ? 0 : this.preAssumptions.size());
107         if (0 <= index && index < sz)
108            return this.preAssumptions.elementAt(index);
109         else index -= sz;
110    
111         sz = (this.pre == null ? 0 : this.pre.size());
112         if (0 <= index && index < sz)
113            return this.pre.elementAt(index);
114         else index -= sz;
115    
116         sz = (this.postAssumptions == null ? 0 : this.postAssumptions.size());
117         if (0 <= index && index < sz)
118            return this.postAssumptions.elementAt(index);
119         else index -= sz;
120    
121         sz = (this.post == null ? 0 : this.post.size());
122         if (0 <= index && index < sz)
123            return this.post.elementAt(index);
124         else index -= sz;
125    
126         if (index == 0) return this.postconditionLocations;
127         else index--;
128    
129         throw new IndexOutOfBoundsException("AST child index " + indexPre);
130      }   //@ nowarn Exception;
131    
132      public final String toString() {
133         return "[Spec"
134            + " dmd = " + this.dmd
135            + " targets = " + this.targets
136            + " specialTargets = " + this.specialTargets
137            + " preVarMap = " + this.preVarMap
138            + " preAssumptions = " + this.preAssumptions
139            + " pre = " + this.pre
140            + " postAssumptions = " + this.postAssumptions
141            + " post = " + this.post
142            + " modifiesEverything = " + this.modifiesEverything
143            + " postconditionLocations = " + this.postconditionLocations
144            + "]";
145      }
146    
147      public final int getTag() {
148         return TagConstants.SPEC;
149      }
150    
151      public final void accept(javafe.ast.Visitor v) { 
152        if (v instanceof Visitor) ((Visitor)v).visitSpec(this);
153      }
154    
155      public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 
156        if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitSpec(this, o); else return null;
157      }
158    
159      public void check() {
160         if (this.dmd == null) throw new RuntimeException();
161         for(int i = 0; i < this.targets.size(); i++)
162            this.targets.elementAt(i).check();
163         for(int i = 0; i < this.specialTargets.size(); i++)
164            this.specialTargets.elementAt(i).check();
165         if (this.preVarMap == null) throw new RuntimeException();
166         for(int i = 0; i < this.preAssumptions.size(); i++)
167            this.preAssumptions.elementAt(i).check();
168         for(int i = 0; i < this.pre.size(); i++)
169            this.pre.elementAt(i).check();
170         for(int i = 0; i < this.postAssumptions.size(); i++)
171            this.postAssumptions.elementAt(i).check();
172         for(int i = 0; i < this.post.size(); i++)
173            this.post.elementAt(i).check();
174         if (this.postconditionLocations == null) throw new RuntimeException();
175      }
176    
177      //@ ensures \result != null;
178      public static Spec make(/*@ non_null @*/ DerivedMethodDecl dmd, /*@ non_null @*/ ExprVec targets, /*@ non_null @*/ ExprVec specialTargets, /*@ non_null @*/ Hashtable preVarMap, /*@ non_null @*/ ExprVec preAssumptions, /*@ non_null @*/ ConditionVec pre, /*@ non_null @*/ ExprVec postAssumptions, /*@ non_null @*/ ConditionVec post, boolean modifiesEverything, /*@ non_null @*/ Set postconditionLocations) {
179         //@ set I_will_establish_invariants_afterwards = true;
180         Spec result = new Spec();
181         result.dmd = dmd;
182         result.targets = targets;
183         result.specialTargets = specialTargets;
184         result.preVarMap = preVarMap;
185         result.preAssumptions = preAssumptions;
186         result.pre = pre;
187         result.postAssumptions = postAssumptions;
188         result.post = post;
189         result.modifiesEverything = modifiesEverything;
190         result.postconditionLocations = postconditionLocations;
191         return result;
192      }
193    }