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 Spec extends ASTNode 031 { 032 public /*@ non_null @*/ DerivedMethodDecl dmd; 033 034 public /*@ non_null @*/ ExprVec targets; 035 036 public /*@ non_null @*/ ExprVec specialTargets; 037 038 public /*@ non_null @*/ Hashtable preVarMap; 039 040 public /*@ non_null @*/ ExprVec preAssumptions; 041 042 public /*@ non_null @*/ ConditionVec pre; 043 044 public /*@ non_null @*/ ExprVec postAssumptions; 045 046 public /*@ non_null @*/ ConditionVec post; 047 048 public boolean modifiesEverything; 049 050 public /*@ non_null @*/ Set postconditionLocations; 051 052 053 public int getStartLoc() { return dmd.original.getStartLoc(); } 054 public int getEndLoc() { return dmd.original.getEndLoc(); } 055 056 057 // Generated boilerplate constructors: 058 059 /** 060 * Construct a raw Spec whose class invariant(s) have not 061 * yet been established. It is the caller's job to 062 * initialize the returned node's fields so that any 063 * class invariants hold. 064 */ 065 //@ requires I_will_establish_invariants_afterwards; 066 protected Spec() {} //@ nowarn Invariant,NonNullInit; 067 068 069 // Generated boilerplate methods: 070 071 public final int childCount() { 072 int sz = 0; 073 if (this.targets != null) sz += this.targets.size(); 074 if (this.specialTargets != null) sz += this.specialTargets.size(); 075 if (this.preAssumptions != null) sz += this.preAssumptions.size(); 076 if (this.pre != null) sz += this.pre.size(); 077 if (this.postAssumptions != null) sz += this.postAssumptions.size(); 078 if (this.post != null) sz += this.post.size(); 079 return sz + 3; 080 } 081 082 public final Object childAt(int index) { 083 /*throws IndexOutOfBoundsException*/ 084 if (index < 0) 085 throw new IndexOutOfBoundsException("AST child index " + index); 086 int indexPre = index; 087 088 int sz; 089 090 if (index == 0) return this.dmd; 091 else index--; 092 093 sz = (this.targets == null ? 0 : this.targets.size()); 094 if (0 <= index && index < sz) 095 return this.targets.elementAt(index); 096 else index -= sz; 097 098 sz = (this.specialTargets == null ? 0 : this.specialTargets.size()); 099 if (0 <= index && index < sz) 100 return this.specialTargets.elementAt(index); 101 else index -= sz; 102 103 if (index == 0) return this.preVarMap; 104 else index--; 105 106 sz = (this.preAssumptions == null ? 0 : this.preAssumptions.size()); 107 if (0 <= index && index < sz) 108 return this.preAssumptions.elementAt(index); 109 else index -= sz; 110 111 sz = (this.pre == null ? 0 : this.pre.size()); 112 if (0 <= index && index < sz) 113 return this.pre.elementAt(index); 114 else index -= sz; 115 116 sz = (this.postAssumptions == null ? 0 : this.postAssumptions.size()); 117 if (0 <= index && index < sz) 118 return this.postAssumptions.elementAt(index); 119 else index -= sz; 120 121 sz = (this.post == null ? 0 : this.post.size()); 122 if (0 <= index && index < sz) 123 return this.post.elementAt(index); 124 else index -= sz; 125 126 if (index == 0) return this.postconditionLocations; 127 else index--; 128 129 throw new IndexOutOfBoundsException("AST child index " + indexPre); 130 } //@ nowarn Exception; 131 132 public final String toString() { 133 return "[Spec" 134 + " dmd = " + this.dmd 135 + " targets = " + this.targets 136 + " specialTargets = " + this.specialTargets 137 + " preVarMap = " + this.preVarMap 138 + " preAssumptions = " + this.preAssumptions 139 + " pre = " + this.pre 140 + " postAssumptions = " + this.postAssumptions 141 + " post = " + this.post 142 + " modifiesEverything = " + this.modifiesEverything 143 + " postconditionLocations = " + this.postconditionLocations 144 + "]"; 145 } 146 147 public final int getTag() { 148 return TagConstants.SPEC; 149 } 150 151 public final void accept(javafe.ast.Visitor v) { 152 if (v instanceof Visitor) ((Visitor)v).visitSpec(this); 153 } 154 155 public final Object accept(javafe.ast.VisitorArgResult v, Object o) { 156 if (v instanceof VisitorArgResult) return ((VisitorArgResult)v).visitSpec(this, o); else return null; 157 } 158 159 public void check() { 160 if (this.dmd == null) throw new RuntimeException(); 161 for(int i = 0; i < this.targets.size(); i++) 162 this.targets.elementAt(i).check(); 163 for(int i = 0; i < this.specialTargets.size(); i++) 164 this.specialTargets.elementAt(i).check(); 165 if (this.preVarMap == null) throw new RuntimeException(); 166 for(int i = 0; i < this.preAssumptions.size(); i++) 167 this.preAssumptions.elementAt(i).check(); 168 for(int i = 0; i < this.pre.size(); i++) 169 this.pre.elementAt(i).check(); 170 for(int i = 0; i < this.postAssumptions.size(); i++) 171 this.postAssumptions.elementAt(i).check(); 172 for(int i = 0; i < this.post.size(); i++) 173 this.post.elementAt(i).check(); 174 if (this.postconditionLocations == null) throw new RuntimeException(); 175 } 176 177 //@ ensures \result != null; 178 public static Spec make(/*@ non_null @*/ DerivedMethodDecl dmd, /*@ non_null @*/ ExprVec targets, /*@ non_null @*/ ExprVec specialTargets, /*@ non_null @*/ Hashtable preVarMap, /*@ non_null @*/ ExprVec preAssumptions, /*@ non_null @*/ ConditionVec pre, /*@ non_null @*/ ExprVec postAssumptions, /*@ non_null @*/ ConditionVec post, boolean modifiesEverything, /*@ non_null @*/ Set postconditionLocations) { 179 //@ set I_will_establish_invariants_afterwards = true; 180 Spec result = new Spec(); 181 result.dmd = dmd; 182 result.targets = targets; 183 result.specialTargets = specialTargets; 184 result.preVarMap = preVarMap; 185 result.preAssumptions = preAssumptions; 186 result.pre = pre; 187 result.postAssumptions = postAssumptions; 188 result.post = post; 189 result.modifiesEverything = modifiesEverything; 190 result.postconditionLocations = postconditionLocations; 191 return result; 192 } 193 }