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.visitor;
012:
013: import de.uka.ilkd.key.java.ArrayOfExpression;
014: import de.uka.ilkd.key.java.Expression;
015: import de.uka.ilkd.key.java.PositionInfo;
016: import de.uka.ilkd.key.java.ProgramElement;
017: import de.uka.ilkd.key.java.reference.ArrayReference;
018: import de.uka.ilkd.key.java.reference.ReferencePrefix;
019: import de.uka.ilkd.key.logic.op.ProgramVariable;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /** Replaces array references a[expr] by a[dat] where dat is the concrete
023: * value for expr. This is needed for unit test generation.
024: */
025: public class IndexReplaceVisitor extends CreatingASTVisitor {
026:
027: private ProgramElement result = null;
028: // private KeYJavaType containingKJT=null
029: private Expression[][] testLocation;
030: private boolean singleTuple;
031: private ProgramVariable partCounter;
032: // private ProgramVariable[] lCounter;
033: private ProgramVariable[] testArray;
034:
035: public IndexReplaceVisitor(ProgramElement pe,
036: Expression[][] testLocation, boolean singleTuple,
037: ProgramVariable partCounter,
038: // ProgramVariable[] lCounter,
039: ProgramVariable[] testArray) {
040: super (pe, true);
041: this .testLocation = testLocation;
042: this .singleTuple = singleTuple;
043: this .partCounter = partCounter;
044: // this.lCounter = lCounter;
045: this .testArray = testArray;
046: }
047:
048: /** starts the walker*/
049: public void start() {
050: stack.push(new ExtList());
051: walk(root());
052: ExtList el = stack.peek();
053: int i = 0;
054: while (!(el.get(i) instanceof ProgramElement)) {
055: i++;
056: }
057: result = (ProgramElement) stack.peek().get(i);
058: }
059:
060: public ProgramElement result() {
061: return result;
062: }
063:
064: private Expression tryToReplaceByTestDatum(Expression e) {
065: int i = findLocIndex(e);
066: if (i != -1) {
067: Expression testDat = singleTuple ? (Expression) testArray[i]
068: : (Expression) new ArrayReference(testArray[i],
069: new Expression[] { partCounter });
070: return testDat;
071: }
072: return e;
073: }
074:
075: private int findLocIndex(Expression e) {
076: for (int i = 0; i < testLocation.length; i++) {
077: for (int j = 0; j < testLocation[i].length; j++) {
078: if (testLocation[i][j].toString().equals(e.toString())) {
079: return i;
080: }
081: }
082: }
083: return -1;
084: }
085:
086: public void performActionOnArrayReference(ArrayReference x) {
087: ExtList changeList = stack.peek();
088: if (changeList.getFirst() == CHANGED) {
089: changeList.removeFirst();
090: }
091: changeList.removeFirstOccurrence(PositionInfo.class);
092: ReferencePrefix rp = (ReferencePrefix) changeList.get(0);
093: ArrayOfExpression aoe = x.getDimensionExpressions();
094: Expression[] indices = new Expression[aoe.size()];
095: for (int i = 0; i < aoe.size(); i++) {
096: indices[i] = tryToReplaceByTestDatum(aoe.getExpression(i));
097: }
098: ArrayReference ar = new ArrayReference(rp, indices);
099: addChild(ar);
100: changed();
101: }
102:
103: }
|