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 LabelStmt extends Stmt
024    {
025      public /*@ non_null @*/ Identifier label;
026    
027      public /*@ non_null @*/ Stmt stmt;
028    
029      //@ invariant locId != javafe.util.Location.NULL;
030      public int locId;
031    
032    
033      private void postCheck() {
034        int t = stmt.getTag();
035        Assert.notFalse(t != TagConstants.SWITCHLABEL       //@ nowarn Pre;
036                        && t != TagConstants.CONSTRUCTORINVOCATION
037                        && t != TagConstants.VARDECLSTMT);
038      }
039      //@ public represents startLoc <- locId;
040      public /*@ pure @*/ int getStartLoc() { return locId; }
041      //@ also public normal_behavior
042      //@ ensures \result == stmt.getEndLoc();
043      public /*@ pure @*/ int getEndLoc() { return stmt.getEndLoc(); }
044    
045    
046    // Generated boilerplate constructors:
047    
048      //@ ensures this.label == label;
049      //@ ensures this.stmt == stmt;
050      //@ ensures this.locId == locId;
051      protected LabelStmt(/*@ non_null @*/ Identifier label, /*@ non_null @*/ Stmt stmt, int locId) {
052         super();
053         this.label = label;
054         this.stmt = stmt;
055         this.locId = locId;
056      }
057    
058    // Generated boilerplate methods:
059    
060      public final int childCount() {
061         return 2;
062      }
063    
064      public final Object childAt(int index) {
065              /*throws IndexOutOfBoundsException*/
066         if (index < 0)
067            throw new IndexOutOfBoundsException("AST child index " + index);
068         int indexPre = index;
069    
070         int sz;
071    
072         if (index == 0) return this.label;
073         else index--;
074    
075         if (index == 0) return this.stmt;
076         else index--;
077    
078         throw new IndexOutOfBoundsException("AST child index " + indexPre);
079      }   //@ nowarn Exception;
080    
081      public final /*@non_null*/String toString() {
082         return "[LabelStmt"
083            + " label = " + this.label
084            + " stmt = " + this.stmt
085            + " locId = " + this.locId
086            + "]";
087      }
088    
089      public final int getTag() {
090         return TagConstants.LABELSTMT;
091      }
092    
093      public final void accept(Visitor v) { v.visitLabelStmt(this); }
094    
095      public final Object accept(VisitorArgResult v, Object o) {return v.visitLabelStmt(this, o); }
096    
097      public void check() {
098         super.check();
099         if (this.label == null) throw new RuntimeException();
100         this.stmt.check();
101         postCheck();
102      }
103    
104      //@ requires locId != javafe.util.Location.NULL;
105      //@ ensures \result != null;
106      public static LabelStmt make(/*@ non_null @*/ Identifier label, /*@ non_null @*/ Stmt stmt, int locId) {
107         LabelStmt result = new LabelStmt(label, stmt, locId);
108         return result;
109      }
110    }