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 MapsExprModifierPragma extends ModifierPragma
032 implements javafe.ast.IdPragma
033 {
034 // Extended to support JML
035
036 public int tag;
037
038 public /*@ non_null @*/ Identifier id;
039
040 public /*@ non_null @*/ Expr mapsexpr;
041
042 public int loc;
043
044 public /*@ non_null @*/ Expr expr;
045
046
047 public final int getTag() { return tag; }
048
049 private void postCheck() {
050 boolean goodtag = (tag == TagConstants.MAPS);
051 Assert.notFalse(goodtag);
052 }
053
054 public Identifier id() { return id; }
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.id == id;
068 //@ ensures this.mapsexpr == mapsexpr;
069 //@ ensures this.loc == loc;
070 //@ ensures this.expr == expr;
071 protected MapsExprModifierPragma(int tag, /*@ non_null @*/ Identifier id, /*@ non_null @*/ Expr mapsexpr, int loc, /*@ non_null @*/ Expr expr) {
072 this.tag = tag;
073 this.id = id;
074 this.mapsexpr = mapsexpr;
075 this.loc = loc;
076 this.expr = expr;
077 }
078
079 // Generated boilerplate methods:
080
081 public final int childCount() {
082 return 3;
083 }
084
085 public final Object childAt(int index) {
086 /*throws IndexOutOfBoundsException*/
087 if (index < 0)
088 throw new IndexOutOfBoundsException("AST child index " + index);
089 int indexPre = index;
090
091 int sz;
092
093 if (index == 0) return this.id;
094 else index--;
095
096 if (index == 0) return this.mapsexpr;
097 else index--;
098
099 if (index == 0) return this.expr;
100 else index--;
101
102 throw new IndexOutOfBoundsException("AST child index " + indexPre);
103 } //@ nowarn Exception;
104
105 public final /*@non_null*/String toString() {
106 return "[MapsExprModifierPragma"
107 + " tag = " + this.tag
108 + " id = " + this.id
109 + " mapsexpr = " + this.mapsexpr
110 + " loc = " + this.loc
111 + " expr = " + this.expr
112 + "]";
113 }
114
115 public final void accept(javafe.ast.Visitor v) {
116 if (v instanceof Visitor) ((Visitor)v).visitMapsExprModifierPragma(this);
117 }
118
119 public final Object accept(javafe.ast.VisitorArgResult v, Object o) {
120 if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitMapsExprModifierPragma(this, o); else return null;
121 }
122
123 public void check() {
124 this.id.check();
125 this.mapsexpr.check();
126 this.expr.check();
127 postCheck();
128 }
129
130 //@ ensures \result != null;
131 public static MapsExprModifierPragma make(int tag, /*@ non_null @*/ Identifier id, /*@ non_null @*/ Expr mapsexpr, int loc, /*@ non_null @*/ Expr expr) {
132 MapsExprModifierPragma result = new MapsExprModifierPragma(tag, id, mapsexpr, loc, expr);
133 return result;
134 }
135 }