001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java.declaration;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.Type;
015: import de.uka.ilkd.key.java.abstraction.Variable;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.logic.ProgramElementName;
018: import de.uka.ilkd.key.logic.op.IProgramVariable;
019: import de.uka.ilkd.key.rule.MatchConditions;
020: import de.uka.ilkd.key.util.Debug;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: /**
024: * Variable specification that defines a variable name. This is a part of a
025: * {@link recoder.java.declaration.VariableDeclaration} and does not
026: * contain a type reference or own modifiers. Note that calls to modifiers
027: * are delegated to the enclosing variable declaration and are therefore
028: * discouraged. This was necessary to subtype Declaration as analyses are
029: * interested in the exact location of a variable name.
030: *
031: * @author AL
032: */
033:
034: public class VariableSpecification extends
035: JavaNonTerminalProgramElement implements NamedProgramElement,
036: ExpressionContainer, Variable//,Declaration
037: {
038:
039: private int hashcode = 0; // just cache, does not break immutability
040:
041: /**
042: * Initializer.
043: */
044: protected final Expression initializer;
045:
046: /**
047: * Dimensions.
048: */
049: protected final int dimensions;
050:
051: /** the type
052: */
053: protected final Type type;
054:
055: protected final IProgramVariable var;
056:
057: public VariableSpecification() {
058: this (null, 0, null, null, null);
059: }
060:
061: public VariableSpecification(IProgramVariable var) {
062: this (var, var.getKeYJavaType());
063: }
064:
065: public VariableSpecification(IProgramVariable var, Type type) {
066: this (var, 0, null, type, null);
067: }
068:
069: public VariableSpecification(IProgramVariable var, Expression init,
070: Type type) {
071: this (var, 0, init, type, null);
072: }
073:
074: public VariableSpecification(IProgramVariable var, int dim,
075: Expression init, Type type) {
076: this (var, dim, init, type, PositionInfo.UNDEFINED);
077: }
078:
079: public VariableSpecification(IProgramVariable var, int dim,
080: Expression init, Type type, PositionInfo pi) {
081: super (pi);
082: this .var = var;
083: this .initializer = init;
084: this .dimensions = dim;
085: this .type = type;
086: }
087:
088: /**
089: * Constructor for the transformation of RECODER ASTs to KeY.
090: * @param children the children of this AST element as KeY classes.
091: * May contain:
092: * an Expression (as initializer of the variable)
093: * a Comment
094: * @param dim the dimension of this type
095: */
096: public VariableSpecification(ExtList children,
097: IProgramVariable var, int dim, Type type) {
098: super (children);
099: this .var = var;
100: initializer = (Expression) children.get(Expression.class);
101: dimensions = dim;
102: this .type = type;
103: }
104:
105: /**
106: * Returns the number of children of this node.
107: * @return an int giving the number of children of this node
108: */
109: public int getChildCount() {
110: int result = 0;
111: if (var != null)
112: result++;
113: if (initializer != null)
114: result++;
115: return result;
116: }
117:
118: /**
119: * Returns the child at the specified index in this node's "virtual"
120: * child array
121: * @param index an index into this node's "virtual" child array
122: * @return the program element at the given position
123: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
124: * of bounds
125: */
126: public ProgramElement getChildAt(int index) {
127: if (var != null) {
128: if (index == 0)
129: return var;
130: index--;
131: }
132: if (initializer != null) {
133: if (index == 0)
134: return initializer;
135: }
136: throw new ArrayIndexOutOfBoundsException();
137: }
138:
139: /**
140: * Get the number of expressions in this container.
141: * @return the number of expressions.
142: */
143:
144: public int getExpressionCount() {
145: return (initializer != null) ? 1 : 0;
146: }
147:
148: /*
149: Return the expression at the specified index in this node's
150: "virtual" expression array.
151: @param index an index for an expression.
152: @return the expression with the given index.
153: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
154: of bounds.
155: */
156: public Expression getExpressionAt(int index) {
157: if (initializer != null && index == 0) {
158: return initializer;
159: }
160: throw new ArrayIndexOutOfBoundsException();
161: }
162:
163: /**
164: * Get name.
165: * @return the string.
166: */
167: public final String getName() {
168: return (var == null) ? null : var.name().toString();
169: }
170:
171: /**
172: * Get name.
173: * @return the name.
174: */
175: public ProgramElementName getProgramElementName() {
176: if (var.name() instanceof ProgramElementName) {
177: return (ProgramElementName) var.name();
178: } else {
179: return new ProgramElementName(var.name().toString()); //only with SVs
180: }
181: }
182:
183: /**
184: * Get program variable
185: * @return the program variable.
186: */
187: public IProgramVariable getProgramVariable() {
188: return var;
189: }
190:
191: /**
192: * Get dimensions.
193: * @return the int value.
194: */
195: public int getDimensions() {
196: return dimensions;
197: }
198:
199: /**
200: * Get initializer.
201: * @return the expression.
202: */
203: public Expression getInitializer() {
204: return initializer;
205: }
206:
207: public boolean hasInitializer() {
208: return initializer != null;
209: }
210:
211: public boolean isFinal() {
212: System.out
213: .println("Method in Variable Specification not implemented!");
214: return false;
215: }
216:
217: public Type getType() {
218: return type;
219: }
220:
221: public String getFullName() {
222: return getName();
223: }
224:
225: public SourceElement getFirstElement() {
226: return var;
227: }
228:
229: public SourceElement getLastElement() {
230: if (initializer != null) {
231: return initializer.getLastElement();
232: } else {
233: return var;
234: }
235: }
236:
237: /** calls the corresponding method of a visitor in order to
238: * perform some action/transformation on this element
239: * @param v the Visitor
240: */
241: public void visit(Visitor v) {
242: v.performActionOnVariableSpecification(this );
243: }
244:
245: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
246: p.printVariableSpecification(this );
247: }
248:
249: /** equals modulo renaming is described in the corresponding
250: * comment in class SourceElement. The variables declared in the
251: * local variable declaration have to be added to the
252: * NameAbstractionTable.
253: */
254: public boolean equalsModRenaming(SourceElement se,
255: NameAbstractionTable nat) {
256: if (!(se instanceof VariableSpecification)) {
257: return false;
258: }
259: final VariableSpecification vs = (VariableSpecification) se;
260: if (dimensions != vs.getDimensions()) {
261: return false;
262: }
263: if (type != null) {
264: if (!(type.equals(vs.getType()))) {
265: return false;
266: }
267: } else {
268: if (vs.getType() != null) {
269: return false;
270: }
271: }
272: nat.add(var, vs.getProgramVariable());
273: if (vs.getChildCount() != getChildCount()) {
274: return false;
275: }
276: for (int i = 0, cc = getChildCount(); i < cc; i++) {
277: if (!getChildAt(i).equalsModRenaming(vs.getChildAt(i), nat)) {
278: return false;
279: }
280: }
281: return true;
282: }
283:
284: public int hashCode() {
285: if (hashcode != 0)
286: return hashcode;
287: int result = 17;
288: result = 37 * result + dimensions;
289: result = 37 * result + ((type == null) ? 0 : type.hashCode());
290: result = 37 * result + getChildCount();
291: for (int i = 0, cc = getChildCount(); i < cc; i++) {
292: result = 37 * result + getChildAt(i).hashCode();
293: }
294: return hashcode = result;
295: }
296:
297: public boolean equals(Object o) {
298: return super .equals(o);
299: }
300:
301: public MatchConditions match(SourceData source,
302: MatchConditions matchCond) {
303: final ProgramElement pe = source.getSource();
304: matchCond = super .match(source, matchCond);
305: if (matchCond != null) {
306: if (getDimensions() != ((VariableSpecification) pe)
307: .getDimensions()) {
308: Debug.out(
309: "Program match. Variables have different dimension "
310: + "(template, source)", this, pe);
311: return null;
312: }
313: }
314: return matchCond;
315: }
316: }
|