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