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    /**
024     * Represents a Java Front End PrimitiveType syntactic unit. 
025     * The tag should be one of the *TYPE constants defined in TagConstants
026     * (e.g., INTTYPE).
027     *
028     * @warning This AST node has associated locations only if syntax is
029     * true.
030     */
031    
032    public class JavafePrimitiveType extends PrimitiveType
033    {
034        /*@ public normal_behavior
035          @   ensures  \result == (tag == TagConstants.BOOLEANTYPE || tag == TagConstants.INTTYPE
036          @  || tag == TagConstants.LONGTYPE || tag == TagConstants.CHARTYPE
037          @  || tag == TagConstants.FLOATTYPE || tag == TagConstants.DOUBLETYPE
038          @  || tag == TagConstants.VOIDTYPE || tag == TagConstants.NULLTYPE
039          @  || tag == TagConstants.BYTETYPE || tag == TagConstants.SHORTTYPE);
040          @*/
041        public static /*@pure*/ boolean isValidTag(int tag) {
042            return (tag == TagConstants.BOOLEANTYPE || tag == TagConstants.INTTYPE
043                    || tag == TagConstants.LONGTYPE || tag == TagConstants.CHARTYPE
044                    || tag == TagConstants.FLOATTYPE || tag == TagConstants.DOUBLETYPE
045                    || tag == TagConstants.VOIDTYPE || tag == TagConstants.NULLTYPE
046                    || tag == TagConstants.BYTETYPE || tag == TagConstants.SHORTTYPE);
047        }
048    
049        /*@ also
050          @ public normal_behavior
051          @   ensures  \result == JavafePrimitiveType.isValidTag(tag);
052          @*/
053        public /*@pure*/ boolean isValidTag() {
054            return JavafePrimitiveType.isValidTag(tag);
055        }
056      /**
057       * Normal maker that produces syntax, but requires a non-NULL location.
058       */
059        /*@ public normal_behavior
060          @   requires  JavafePrimitiveType.isValidTag(tag);
061          @   requires loc != javafe.util.Location.NULL;
062          @   ensures \result.syntax;
063          @*/
064      public static /*@ non_null */ JavafePrimitiveType make(TypeModifierPragmaVec tmodifiers,
065                                       int tag, int loc) {
066         JavafePrimitiveType result = new JavafePrimitiveType(
067                                    tmodifiers,
068                                    tag,
069                                    loc);
070         return result;
071      }
072    
073      /**
074       * Special maker for producing non-syntax, which does not require a
075       * location.
076       */
077        /*@ public normal_behavior
078          @   requires  JavafePrimitiveType.isValidTag(tag);
079          @   ensures !\result.syntax;
080          @*/
081      public static /*@non_null*/ JavafePrimitiveType makeNonSyntax(int tag) {
082         JavafePrimitiveType result = new JavafePrimitiveType(
083                                     null,
084                                     tag,
085                                     Location.NULL);
086         return result;
087      }
088    
089      // manual override for backwards compatibility
090        /*@ public normal_behavior
091          @   requires  JavafePrimitiveType.isValidTag(tag);
092          @   requires loc != javafe.util.Location.NULL;
093          @   ensures \result.syntax;
094          @*/
095      static public /*@non_null*/ JavafePrimitiveType make(int tag, int loc) {
096        return JavafePrimitiveType.make(null, tag, loc);
097      }
098    
099      private void postCheck() {
100        boolean goodtag = JavafePrimitiveType.isValidTag(tag);
101        Assert.notFalse(goodtag); 
102      }
103    
104    
105    // Generated boilerplate constructors:
106    
107      //@ ensures this.tmodifiers == tmodifiers;
108      //@ ensures this.tag == tag;
109      //@ ensures this.loc == loc;
110      protected JavafePrimitiveType(TypeModifierPragmaVec tmodifiers, int tag, int loc) {
111         super(tmodifiers, tag, loc);
112      }
113    
114    // Generated boilerplate methods:
115    
116      public final int childCount() {
117         int sz = 0;
118         if (this.tmodifiers != null) sz += this.tmodifiers.size();
119         return sz + 0;
120      }
121    
122      public final Object childAt(int index) {
123              /*throws IndexOutOfBoundsException*/
124         if (index < 0)
125            throw new IndexOutOfBoundsException("AST child index " + index);
126         int indexPre = index;
127    
128         int sz;
129    
130         sz = (this.tmodifiers == null ? 0 : this.tmodifiers.size());
131         if (0 <= index && index < sz)
132            return this.tmodifiers.elementAt(index);
133         else index -= sz;
134    
135         throw new IndexOutOfBoundsException("AST child index " + indexPre);
136      }   //@ nowarn Exception;
137    
138      public final /*@non_null*/String toString() {
139         return "[JavafePrimitiveType"
140            + " tmodifiers = " + this.tmodifiers
141            + " tag = " + this.tag
142            + " loc = " + this.loc
143            + "]";
144      }
145    
146      public final void accept(Visitor v) { v.visitJavafePrimitiveType(this); }
147    
148      public final Object accept(VisitorArgResult v, Object o) {return v.visitJavafePrimitiveType(this, o); }
149    
150      public void check() {
151         super.check();
152         if (this.tmodifiers != null)
153            for(int i = 0; i < this.tmodifiers.size(); i++)
154               this.tmodifiers.elementAt(i).check();
155         postCheck();
156      }
157    
158    }