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