01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.java.visitor;
12:
13: import de.uka.ilkd.key.java.Expression;
14: import de.uka.ilkd.key.java.PositionInfo;
15: import de.uka.ilkd.key.java.PrettyPrinter;
16: import de.uka.ilkd.key.java.ProgramElement;
17: import de.uka.ilkd.key.java.reference.ArrayLengthReference;
18: import de.uka.ilkd.key.java.reference.FieldReference;
19: import de.uka.ilkd.key.java.reference.MethodReference;
20: import de.uka.ilkd.key.java.reference.ReferencePrefix;
21: import de.uka.ilkd.key.logic.ProgramElementName;
22: import de.uka.ilkd.key.logic.op.ProgramVariable;
23: import de.uka.ilkd.key.util.ExtList;
24:
25: /**
26: * Replaces field references o.a by methodcalls o._a(). This is needed for
27: * unit test generation.
28: */
29: public class FieldReplaceVisitor extends CreatingASTVisitor {
30:
31: private ProgramElement result = null;
32:
33: // private KeYJavaType containingKJT=null
34:
35: public FieldReplaceVisitor(ProgramElement pe) {
36: super (pe, true);
37: }
38:
39: /** starts the walker*/
40: public void start() {
41: stack.push(new ExtList());
42: walk(root());
43: ExtList el = stack.peek();
44: int i = 0;
45: while (!(el.get(i) instanceof ProgramElement)) {
46: i++;
47: }
48: result = (ProgramElement) stack.peek().get(i);
49: }
50:
51: public ProgramElement result() {
52: return result;
53: }
54:
55: public void performActionOnFieldReference(FieldReference x) {
56: ExtList changeList = stack.peek();
57: if (changeList.getFirst() == CHANGED) {
58: changeList.removeFirst();
59: }
60: changeList.removeFirstOccurrence(PositionInfo.class);
61: if (x.getReferencePrefix() != null) {
62: Expression field = (Expression) changeList.get(1);
63: if (field instanceof ProgramVariable) {
64: final String shortName = ((ProgramVariable) field)
65: .getProgramElementName().getProgramName();
66: if ("length".equals(shortName)) {
67: ExtList l = new ExtList();
68: l.add(changeList.get(0));
69: addChild(new ArrayLengthReference(l));
70: } else {
71: String typeName = ((ProgramVariable) x
72: .getChildAt(1)).getKeYJavaType().getName();
73: typeName = PrettyPrinter
74: .getTypeNameForAccessMethods(typeName);
75: addChild(new MethodReference(new ExtList(),
76: new ProgramElementName("_" + shortName
77: + typeName),
78: (ReferencePrefix) changeList.get(0)));
79: }
80: }
81: } else {
82: String typeName = ((ProgramVariable) x.getChildAt(0))
83: .getKeYJavaType().getName();
84: typeName = PrettyPrinter
85: .getTypeNameForAccessMethods(typeName);
86: addChild(new MethodReference(new ExtList(),
87: new ProgramElementName("_"
88: + ((ProgramVariable) changeList.get(0))
89: .getProgramElementName()
90: .getProgramName() + typeName), null));
91: }
92: changed();
93: }
94: }
|