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