001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 /* IF THIS IS A JAVA FILE, DO NOT EDIT IT! 004 005 Most Java files in this directory which are part of the Javafe AST 006 are automatically generated using the astgen comment (see 007 ESCTools/Javafe/astgen) from the input file 'hierarchy.h'. If you 008 wish to modify AST classes or introduce new ones, modify 009 'hierarchy.j.' 010 */ 011 012 package escjava.ast; 013 014 import java.util.Hashtable; 015 import java.util.Set; 016 import java.util.ArrayList; 017 018 import javafe.ast.*; 019 import javafe.util.Assert; 020 import javafe.util.Location; 021 import escjava.ParsedRoutineSpecs; 022 023 // Convention: unless otherwise noted, integer fields named "loc" refer 024 // to the location of the first character of the syntactic unit 025 026 //# TagBase javafe.tc.TagConstants.LAST_TAG + 1 027 //# VisitorRoot javafe.ast.Visitor 028 029 030 public class ExprModifierPragma extends ModifierPragma 031 { 032 // Extended to support JML 033 034 public int tag; 035 036 public /*@ non_null @*/ Expr expr; 037 038 public int loc; 039 040 public int errorTag = 0; 041 042 public final int getTag() { return tag; } 043 044 private void postCheck() { 045 boolean goodtag = (tag == TagConstants.ALSO_ENSURES 046 || tag == TagConstants.ALSO_REQUIRES 047 || tag == TagConstants.ENSURES 048 || tag == TagConstants.MONITORED_BY 049 || tag == TagConstants.READABLE_IF 050 || tag == TagConstants.REQUIRES 051 || tag == TagConstants.WACK_DURATION 052 || tag == TagConstants.WACK_WORKING_SPACE 053 || tag == TagConstants.WRITABLE_IF 054 ); 055 boolean isJMLExprModifier = isJMLExprModifier(); 056 Assert.notFalse(goodtag || isJMLExprModifier); 057 } 058 059 private boolean isJMLExprModifier() { 060 return tag == TagConstants.ALSO 061 || tag == TagConstants.PRECONDITION 062 || tag == TagConstants.POSTCONDITION; 063 } 064 065 public int getStartLoc() { return loc; } 066 public int getEndLoc() { return expr.getEndLoc(); } 067 068 069 // Generated boilerplate constructors: 070 071 /** 072 * Construct a raw ExprModifierPragma whose class invariant(s) have not 073 * yet been established. It is the caller's job to 074 * initialize the returned node's fields so that any 075 * class invariants hold. 076 */ 077 //@ requires I_will_establish_invariants_afterwards; 078 protected ExprModifierPragma() {} //@ nowarn Invariant,NonNullInit; 079 080 081 // Generated boilerplate methods: 082 083 public final int childCount() { 084 return 1; 085 } 086 087 public final Object childAt(int index) { 088 /*throws IndexOutOfBoundsException*/ 089 if (index < 0) 090 throw new IndexOutOfBoundsException("AST child index " + index); 091 int indexPre = index; 092 093 int sz; 094 095 if (index == 0) return this.expr; 096 else index--; 097 098 throw new IndexOutOfBoundsException("AST child index " + indexPre); 099 } //@ nowarn Exception; 100 101 public final String toString() { 102 return "[ExprModifierPragma" 103 + " tag = " + this.tag 104 + " expr = " + this.expr 105 + " loc = " + this.loc 106 + "]"; 107 } 108 109 public final void accept(javafe.ast.Visitor v) { 110 if (v instanceof Visitor) ((Visitor)v).visitExprModifierPragma(this); 111 } 112 113 public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 114 if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitExprModifierPragma(this, o); else return null; 115 } 116 117 public void check() { 118 this.expr.check(); 119 postCheck(); 120 } 121 122 //@ ensures \result != null; 123 public static ExprModifierPragma make(int tag, /*@ non_null @*/ Expr expr, int loc) { 124 //@ set I_will_establish_invariants_afterwards = true; 125 ExprModifierPragma result = new ExprModifierPragma(); 126 result.tag = tag; 127 result.expr = expr; 128 result.loc = loc; 129 return result; 130 } 131 }