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 javafe.ast;
014    
015    import javafe.util.Assert;
016    import javafe.util.Location;
017    import javafe.util.ErrorSet;
018    
019    // Convention: unless otherwise noted, integer fields named "loc" refer
020    // to the location of the first character of the syntactic unit
021    
022    
023    public class TryFinallyStmt extends Stmt
024    {
025      // @note locTry might will be shared with tryClause.locTry if
026      // tryClause is a TryCatchStmt
027      public /*@ non_null @*/ Stmt tryClause;
028    
029      public /*@ non_null @*/ Stmt finallyClause;
030    
031      //@ invariant loc != javafe.util.Location.NULL;
032      public int loc;
033    
034      //@ invariant locFinally != javafe.util.Location.NULL;
035      public int locFinally;
036    
037    
038      private void postCheck() {
039        int t = tryClause.getTag();
040        Assert.notFalse(t != TagConstants.SWITCHLABEL       //@ nowarn Pre;
041                        && t != TagConstants.CONSTRUCTORINVOCATION
042                        && t != TagConstants.VARDECLSTMT);
043        t = finallyClause.getTag();
044        Assert.notFalse(t != TagConstants.SWITCHLABEL       //@ nowarn Pre;
045                        && t != TagConstants.CONSTRUCTORINVOCATION
046                        && t != TagConstants.VARDECLSTMT);
047      }
048    
049      //@ public represents startLoc <- loc;
050      public /*@ pure @*/ int getStartLoc() { return loc; }
051      //@ also public normal_behavior
052      //@ ensures \result == finallyClause.getEndLoc();
053      public /*@ pure @*/ int getEndLoc() { return finallyClause.getEndLoc(); }
054    
055    
056    // Generated boilerplate constructors:
057    
058      //@ ensures this.tryClause == tryClause;
059      //@ ensures this.finallyClause == finallyClause;
060      //@ ensures this.loc == loc;
061      //@ ensures this.locFinally == locFinally;
062      protected TryFinallyStmt(/*@ non_null @*/ Stmt tryClause, /*@ non_null @*/ Stmt finallyClause, int loc, int locFinally) {
063         super();
064         this.tryClause = tryClause;
065         this.finallyClause = finallyClause;
066         this.loc = loc;
067         this.locFinally = locFinally;
068      }
069    
070    // Generated boilerplate methods:
071    
072      public final int childCount() {
073         return 2;
074      }
075    
076      public final Object childAt(int index) {
077              /*throws IndexOutOfBoundsException*/
078         if (index < 0)
079            throw new IndexOutOfBoundsException("AST child index " + index);
080         int indexPre = index;
081    
082         int sz;
083    
084         if (index == 0) return this.tryClause;
085         else index--;
086    
087         if (index == 0) return this.finallyClause;
088         else index--;
089    
090         throw new IndexOutOfBoundsException("AST child index " + indexPre);
091      }   //@ nowarn Exception;
092    
093      public final /*@non_null*/String toString() {
094         return "[TryFinallyStmt"
095            + " tryClause = " + this.tryClause
096            + " finallyClause = " + this.finallyClause
097            + " loc = " + this.loc
098            + " locFinally = " + this.locFinally
099            + "]";
100      }
101    
102      public final int getTag() {
103         return TagConstants.TRYFINALLYSTMT;
104      }
105    
106      public final void accept(Visitor v) { v.visitTryFinallyStmt(this); }
107    
108      public final Object accept(VisitorArgResult v, Object o) {return v.visitTryFinallyStmt(this, o); }
109    
110      public void check() {
111         super.check();
112         this.tryClause.check();
113         this.finallyClause.check();
114         postCheck();
115      }
116    
117      //@ requires loc != javafe.util.Location.NULL;
118      //@ requires locFinally != javafe.util.Location.NULL;
119      //@ ensures \result != null;
120      public static TryFinallyStmt make(/*@ non_null @*/ Stmt tryClause, /*@ non_null @*/ Stmt finallyClause, int loc, int locFinally) {
121         TryFinallyStmt result = new TryFinallyStmt(tryClause, finallyClause, loc, locFinally);
122         return result;
123      }
124    }