    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 GetsCmd extends AssignCmd
    031    {
    032      // denotes v := rhs
    033
    034
    035    // Generated boilerplate constructors:
    036
    037       /**
    038        * Construct a raw GetsCmd whose class invariant(s) have not
    039        * yet been established.  It is the caller's job to
    040        * initialize the returned node's fields so that any
    041        * class invariants hold.
    042        */
    043       //@ requires I_will_establish_invariants_afterwards;
    044       protected GetsCmd() {}    //@ nowarn Invariant,NonNullInit;
    045
    046
    047    // Generated boilerplate methods:
    048
    049       public final int childCount() {
    050          return 2;
    051       }
    052
    053       public final Object childAt(int index) {
    054               /*throws IndexOutOfBoundsException*/
    055          if (index < 0)
    056             throw new IndexOutOfBoundsException("AST child index " + index);
    057          int indexPre = index;
    058
    059          int sz;
    060
    061          if (index == 0) return this.v;
    062          else index--;
    063
    064          if (index == 0) return this.rhs;
    065          else index--;
    066
    067          throw new IndexOutOfBoundsException("AST child index " + indexPre);
    068       }   //@ nowarn Exception;
    069
    070       public final String toString() {
    071          return "[GetsCmd"
    072             + " v = " + this.v
    073             + " rhs = " + this.rhs
    074             + "]";
    075       }
    076
    077       public final int getTag() {
    078          return TagConstants.GETSCMD;
    079       }
    080
    081       public final void accept(javafe.ast.Visitor v) {
    082          if (v instanceof Visitor) ((Visitor)v).visitGetsCmd(this);
    083       }
    084
    085       public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
    086          if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitGetsCmd(this, o); else return null;
    087       }
    088
    089       public void check() {
    090          super.check();
    091          this.v.check();
    092          this.rhs.check();
    093       }
    094
    095       //@ ensures \result != null;
    096       public static GetsCmd make(/*@ non_null @*/ VariableAccess v, /*@ non_null @*/ Expr rhs) {
    097          //@ set I_will_establish_invariants_afterwards = true;
    098          GetsCmd result = new GetsCmd();
    099          result.v = v;
    100          result.rhs = rhs;
    101          return result;
    102       }
    103    }