    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    }