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