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