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