0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010: //
0011: //
0012: package de.uka.ilkd.key.java.visitor;
0013:
0014: import de.uka.ilkd.key.java.*;
0015: import de.uka.ilkd.key.java.annotation.Annotation;
0016: import de.uka.ilkd.key.java.declaration.ClassInitializer;
0017: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
0018: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
0019: import de.uka.ilkd.key.java.declaration.VariableSpecification;
0020: import de.uka.ilkd.key.java.expression.ArrayInitializer;
0021: import de.uka.ilkd.key.java.expression.ParenthesizedExpression;
0022: import de.uka.ilkd.key.java.expression.PassiveExpression;
0023: import de.uka.ilkd.key.java.expression.operator.*;
0024: import de.uka.ilkd.key.java.reference.*;
0025: import de.uka.ilkd.key.java.statement.*;
0026: import de.uka.ilkd.key.logic.op.IProgramVariable;
0027: import de.uka.ilkd.key.logic.op.ProgramVariable;
0028: import de.uka.ilkd.key.rule.soundness.ProgramSVProxy;
0029: import de.uka.ilkd.key.util.ExtList;
0030: import de.uka.ilkd.key.util.SimpleStackOfExtList;
0031:
0032: /**
0033: * Walks through a java AST in depth-left-fist-order.
0034: */
0035: public abstract class CreatingASTVisitor extends JavaASTVisitor {
0036:
0037: protected static final Boolean CHANGED = new Boolean(true);
0038:
0039: boolean preservesPositionInfo = true;
0040:
0041: /** */
0042: protected SimpleStackOfExtList stack = new SimpleStackOfExtList();
0043:
0044: /**
0045: * create the CreatingASTVisitor
0046: *
0047: * @param root
0048: * the ProgramElement where to begin
0049: */
0050: public CreatingASTVisitor(ProgramElement root, boolean preservesPos) {
0051: super (root);
0052: this .preservesPositionInfo = preservesPos;
0053: }
0054:
0055: /**
0056: * the action that is performed just before leaving the node the last time
0057: */
0058: protected void doAction(ProgramElement node) {
0059: node.visit(this );
0060: }
0061:
0062: public boolean preservesPositionInfo() {
0063: return preservesPositionInfo;
0064: }
0065:
0066: protected void walk(ProgramElement node) {
0067: ExtList l = new ExtList();
0068: l.add(node.getPositionInfo());
0069: stack.push(l);
0070: super .walk(node);
0071: }
0072:
0073: public String toString() {
0074: return stack.peek().toString();
0075: }
0076:
0077: /**
0078: * called if the program element x is unchanged
0079: */
0080: protected void doDefaultAction(SourceElement x) {
0081: addChild(x);
0082: }
0083:
0084: public void performActionOnAssert(Assert x) {
0085: ExtList changeList = stack.peek();
0086: if (changeList.getFirst() == CHANGED) {
0087: changeList.removeFirst();
0088: PositionInfo pos = (PositionInfo) changeList
0089: .removeFirstOccurrence(PositionInfo.class);
0090: if (!preservesPositionInfo) {
0091: pos = PositionInfo.UNDEFINED;
0092: }
0093: Expression condition = (Expression) changeList
0094: .removeFirstOccurrence(Expression.class);
0095: Expression message = (Expression) changeList
0096: .removeFirstOccurrence(Expression.class);
0097:
0098: addChild(new Assert(condition, message, pos));
0099:
0100: changed();
0101: } else {
0102: doDefaultAction(x);
0103: }
0104: }
0105:
0106: public void performActionOnEmptyStatement(EmptyStatement x) {
0107: doDefaultAction(x);
0108: }
0109:
0110: public void performActionOnStatementBlock(StatementBlock x) {
0111: DefaultAction def = new DefaultAction(x) {
0112: ProgramElement createNewElement(ExtList changeList) {
0113: return new StatementBlock(changeList);
0114: }
0115: };
0116: def.doAction(x);
0117: }
0118:
0119: protected void performActionOnAnnotationArray(Annotation[] a) {
0120: for (int i = 0; i < a.length; i++) {
0121: addToTopOfStack(a[i]);
0122: }
0123: }
0124:
0125: // eee
0126: public void performActionOnWhile(While x) {
0127: ExtList changeList = stack.peek();
0128: if (changeList.getFirst() == CHANGED) {
0129: changeList.removeFirst();
0130: PositionInfo pos = (PositionInfo) changeList
0131: .removeFirstOccurrence(PositionInfo.class);
0132: if (!preservesPositionInfo) {
0133: pos = PositionInfo.UNDEFINED;
0134: }
0135: Guard g = (Guard) changeList
0136: .removeFirstOccurrence(Guard.class);
0137: Expression guard = g == null ? null : g.getExpression();
0138: Statement body = (Statement) changeList
0139: .removeFirstOccurrence(Statement.class);
0140: Annotation[] a = (Annotation[]) changeList
0141: .collect(Annotation.class);
0142:
0143: addChild(new While(guard, body, pos, a));
0144:
0145: changed();
0146: } else {
0147: doDefaultAction(x);
0148: }
0149: }
0150:
0151: // eee
0152: public void performActionOnDo(Do x) {
0153: ExtList changeList = stack.peek();
0154: if (changeList.getFirst() == CHANGED) {
0155: changeList.removeFirst();
0156: PositionInfo pos = (PositionInfo) changeList
0157: .removeFirstOccurrence(PositionInfo.class);
0158: if (!preservesPositionInfo) {
0159: pos = PositionInfo.UNDEFINED;
0160: }
0161: Statement body = (Statement) changeList
0162: .removeFirstOccurrence(Statement.class);
0163: Guard g = (Guard) changeList
0164: .removeFirstOccurrence(Guard.class);
0165: Expression guard = g == null ? null : g.getExpression();
0166: Annotation[] a = (Annotation[]) changeList
0167: .collect(Annotation.class);
0168: addChild(new Do(guard, body, pos, a));
0169:
0170: changed();
0171: } else {
0172: doDefaultAction(x);
0173: }
0174: }
0175:
0176: public void performActionOnIf(If x) {
0177:
0178: DefaultAction def = new DefaultAction(x) {
0179: ProgramElement createNewElement(ExtList changeList) {
0180: return new If(changeList);
0181: }
0182: };
0183: def.doAction(x);
0184:
0185: }
0186:
0187: public void performActionOnThen(Then x) {
0188: DefaultAction def = new DefaultAction(x) {
0189: ProgramElement createNewElement(ExtList changeList) {
0190: return new Then(changeList);
0191: }
0192: };
0193: def.doAction(x);
0194: }
0195:
0196: // eee
0197: public void performActionOnVariableSpecification(
0198: VariableSpecification x) {
0199: ExtList changeList = stack.peek();
0200: if (changeList.getFirst() == CHANGED) {
0201: changeList.removeFirst();
0202: PositionInfo pi = (PositionInfo) changeList
0203: .removeFirstOccurrence(PositionInfo.class);
0204:
0205: if (!preservesPositionInfo) {
0206: pi = PositionInfo.UNDEFINED;
0207: }
0208: Expression expr = null;
0209: if (changeList.size() > 1) {
0210: expr = (Expression) changeList.get(1);
0211: }
0212: IProgramVariable pv = (IProgramVariable) changeList.get(0);
0213: addChild(new VariableSpecification(pv, x.getDimensions(),
0214: expr, pv.getKeYJavaType(), pi));
0215: changed();
0216: } else {
0217: doDefaultAction(x);
0218: }
0219:
0220: }
0221:
0222: // eee
0223: public void performActionOnFieldReference(FieldReference x) {
0224: ExtList changeList = stack.peek();
0225: if (changeList.getFirst() == CHANGED) {
0226: changeList.removeFirst();
0227:
0228: PositionInfo pi = (PositionInfo) changeList
0229: .removeFirstOccurrence(PositionInfo.class);
0230:
0231: if (!preservesPositionInfo) {
0232: pi = PositionInfo.UNDEFINED;
0233: }
0234:
0235: if (x.getReferencePrefix() != null) {
0236: final Expression field = (Expression) changeList.get(1);
0237: if (field instanceof ProgramVariable) {
0238: addChild(new FieldReference(
0239: (ProgramVariable) field,
0240: (ReferencePrefix) changeList.get(0), pi));
0241: } else {
0242: addChild(new FieldReference(
0243: ((FieldReference) field)
0244: .getProgramVariable(),
0245: (ReferencePrefix) changeList.get(0), pi));
0246: }
0247: } else {
0248: addChild(new FieldReference(
0249: (ProgramVariable) changeList.get(0), null, pi));
0250: }
0251: changed();
0252: } else {
0253: doDefaultAction(x);
0254: }
0255:
0256: }
0257:
0258: public void performActionOnSchematicFieldReference(
0259: SchematicFieldReference sfr) {
0260: performActionOnFieldReference(sfr);
0261: }
0262:
0263: // eee
0264: public void performActionOnMethodReference(MethodReference x) {
0265: ExtList changeList = stack.peek();
0266: if (changeList.getFirst() == CHANGED) {
0267: changeList.removeFirst();
0268:
0269: PositionInfo pi = (PositionInfo) changeList
0270: .removeFirstOccurrence(PositionInfo.class);
0271:
0272: if (!preservesPositionInfo) {
0273: pi = PositionInfo.UNDEFINED;
0274: }
0275:
0276: ReferencePrefix rp = null;
0277: if (x.getReferencePrefix() != null) {
0278: rp = (ReferencePrefix) changeList.get(0);
0279: }
0280: changeList.remove(rp);
0281: MethodName name = (MethodName) changeList
0282: .get(MethodName.class);
0283: MethodReference mr = new MethodReference(changeList, name,
0284: rp, pi);
0285: addChild(mr);
0286: changed();
0287: } else {
0288: doDefaultAction(x);
0289: }
0290: }
0291:
0292: public void performActionOnTypeReference(final TypeReference x) {
0293: DefaultAction def = new DefaultAction(x) {
0294: ProgramElement createNewElement(ExtList changeList) {
0295: return new TypeRef(changeList, x.getKeYJavaType(), x
0296: .getDimensions());
0297: }
0298: };
0299: def.doAction(x);
0300: }
0301:
0302: public void performActionOnElse(Else x) {
0303: DefaultAction def = new DefaultAction(x) {
0304: ProgramElement createNewElement(ExtList changeList) {
0305: return new Else(changeList);
0306: }
0307: };
0308: def.doAction(x);
0309: }
0310:
0311: // eee
0312: public void performActionOnCase(Case x) {
0313: Expression e = null;
0314: ExtList changeList = stack.peek();
0315: if (changeList.getFirst() == CHANGED) {
0316: changeList.removeFirst();
0317: PositionInfo pi = (PositionInfo) changeList
0318: .removeFirstOccurrence(PositionInfo.class);
0319: if (!preservesPositionInfo) {
0320: pi = PositionInfo.UNDEFINED;
0321: }
0322: if (x.getExpression() != null) {
0323: e = (Expression) changeList.removeFirst();
0324: }
0325: addChild(new Case(changeList, e, pi));
0326: changed();
0327: } else {
0328: doDefaultAction(x);
0329: }
0330: }
0331:
0332: public void performActionOnCatch(Catch x) {
0333: DefaultAction def = new DefaultAction(x) {
0334: ProgramElement createNewElement(ExtList changeList) {
0335: return new Catch(changeList);
0336: }
0337: };
0338: def.doAction(x);
0339: }
0340:
0341: public void performActionOnThrow(Throw x) {
0342: DefaultAction def = new DefaultAction(x) {
0343: ProgramElement createNewElement(ExtList changeList) {
0344: return new Throw(changeList);
0345: }
0346: };
0347: def.doAction(x);
0348: }
0349:
0350: public void performActionOnTry(Try x) {
0351: DefaultAction def = new DefaultAction(x) {
0352: ProgramElement createNewElement(ExtList changeList) {
0353: return new Try(changeList);
0354: }
0355: };
0356: def.doAction(x);
0357: }
0358:
0359: public void performActionOnDefault(Default x) {
0360: DefaultAction def = new DefaultAction(x) {
0361: ProgramElement createNewElement(ExtList changeList) {
0362: return new Default(changeList);
0363: }
0364: };
0365: def.doAction(x);
0366: }
0367:
0368: public void performActionOnFinally(Finally x) {
0369: DefaultAction def = new DefaultAction(x) {
0370: ProgramElement createNewElement(ExtList changeList) {
0371: return new Finally(changeList);
0372: }
0373: };
0374: def.doAction(x);
0375: }
0376:
0377: public void performActionOnInstanceof(Instanceof x) {
0378: DefaultAction def = new DefaultAction(x) {
0379: ProgramElement createNewElement(ExtList changeList) {
0380: return new Instanceof(changeList);
0381: }
0382: };
0383: def.doAction(x);
0384: }
0385:
0386: public void performActionOnBreak(Break x) {
0387: DefaultAction def = new DefaultAction(x) {
0388: ProgramElement createNewElement(ExtList changeList) {
0389: return new Break(changeList);
0390: }
0391: };
0392: def.doAction(x);
0393: }
0394:
0395: public void performActionOnContinue(Continue x) {
0396: DefaultAction def = new DefaultAction(x) {
0397: ProgramElement createNewElement(ExtList changeList) {
0398: return new Continue(changeList);
0399: }
0400: };
0401: def.doAction(x);
0402: }
0403:
0404: public void performActionOnFor(For x) {
0405: DefaultAction def = new DefaultAction(x) {
0406: ProgramElement createNewElement(ExtList changeList) {
0407: return new For(changeList);
0408: }
0409: };
0410: def.doAction(x);
0411: }
0412:
0413: // eee
0414: public void performActionOnLabeledStatement(LabeledStatement x) {
0415: Label l = null;
0416: ExtList changeList = stack.peek();
0417: if (changeList.getFirst() == CHANGED) {
0418: changeList.removeFirst();
0419: PositionInfo pi = (PositionInfo) changeList
0420: .removeFirstOccurrence(PositionInfo.class);
0421: if (!preservesPositionInfo) {
0422: pi = PositionInfo.UNDEFINED;
0423: }
0424: if (x.getLabel() != null) {
0425: l = (Label) changeList.removeFirst();
0426: }
0427: addChild(new LabeledStatement(changeList, l, pi));
0428: changed();
0429: } else {
0430: doDefaultAction(x);
0431: }
0432: }
0433:
0434: // eee
0435: public void performActionOnMethodFrame(MethodFrame x) {
0436: ExtList changeList = stack.peek();
0437: if (!changeList.isEmpty() && changeList.getFirst() == CHANGED) {
0438: changeList.removeFirst();
0439: PositionInfo pi = (PositionInfo) changeList
0440: .removeFirstOccurrence(PositionInfo.class); //Methodframe cannot occur in original program
0441:
0442: if (!preservesPositionInfo()) {
0443: pi = PositionInfo.UNDEFINED;
0444: }
0445:
0446: if (x.getChildCount() == 3) {
0447: addChild(new MethodFrame((IProgramVariable) changeList
0448: .get(0), (IExecutionContext) changeList.get(1),
0449: (StatementBlock) changeList.get(2), x
0450: .getProgramMethod(), pi));
0451:
0452: } else if (x.getChildCount() == 2) {
0453: addChild(new MethodFrame(null,
0454: (IExecutionContext) changeList.get(0),
0455: (StatementBlock) changeList.get(1), x
0456: .getProgramMethod(), pi));
0457: } else {
0458: throw new IllegalStateException(
0459: "Methodframe has not allowed number of children.");
0460: }
0461: changed();
0462: } else {
0463: doDefaultAction(x);
0464: }
0465: }
0466:
0467: public void performActionOnMethodBodyStatement(
0468: final MethodBodyStatement x) {
0469: DefaultAction def = new DefaultAction(x) {
0470: ProgramElement createNewElement(ExtList changeList) {
0471: return new MethodBodyStatement(changeList);
0472: }
0473: };
0474: def.doAction(x);
0475: }
0476:
0477: public void performActionOnSynchronizedBlock(SynchronizedBlock x) {
0478: DefaultAction def = new DefaultAction(x) {
0479: ProgramElement createNewElement(ExtList changeList) {
0480: return new SynchronizedBlock(changeList);
0481: }
0482: };
0483: def.doAction(x);
0484: }
0485:
0486: public void performActionOnCopyAssignment(CopyAssignment x) {
0487: DefaultAction def = new DefaultAction(x) {
0488: ProgramElement createNewElement(ExtList changeList) {
0489: return new CopyAssignment(changeList);
0490: }
0491: };
0492: def.doAction(x);
0493: }
0494:
0495: public void performActionOnPreIncrement(PreIncrement x) {
0496: DefaultAction def = new DefaultAction(x) {
0497: ProgramElement createNewElement(ExtList changeList) {
0498: return new PreIncrement(changeList);
0499: }
0500: };
0501: def.doAction(x);
0502: }
0503:
0504: public void performActionOnPostIncrement(PostIncrement x) {
0505: DefaultAction def = new DefaultAction(x) {
0506: ProgramElement createNewElement(ExtList changeList) {
0507: return new PostIncrement(changeList);
0508: }
0509: };
0510: def.doAction(x);
0511: }
0512:
0513: public void performActionOnPlus(Plus x) {
0514: DefaultAction def = new DefaultAction(x) {
0515: ProgramElement createNewElement(ExtList changeList) {
0516: return new Plus(changeList);
0517: }
0518: };
0519: def.doAction(x);
0520: }
0521:
0522: public void performActionOnTimes(Times x) {
0523: DefaultAction def = new DefaultAction(x) {
0524: ProgramElement createNewElement(ExtList changeList) {
0525: return new Times(changeList);
0526: }
0527: };
0528: def.doAction(x);
0529: }
0530:
0531: public void performActionOnMinus(Minus x) {
0532: DefaultAction def = new DefaultAction(x) {
0533: ProgramElement createNewElement(ExtList changeList) {
0534: return new Minus(changeList);
0535: }
0536: };
0537: def.doAction(x);
0538: }
0539:
0540: public void performActionOnEquals(Equals x) {
0541: DefaultAction def = new DefaultAction(x) {
0542: ProgramElement createNewElement(ExtList changeList) {
0543: return new Equals(changeList);
0544: }
0545: };
0546: def.doAction(x);
0547: }
0548:
0549: public void performActionOnNotEquals(NotEquals x) {
0550: DefaultAction def = new DefaultAction(x) {
0551: ProgramElement createNewElement(ExtList changeList) {
0552: return new NotEquals(changeList);
0553: }
0554: };
0555: def.doAction(x);
0556: }
0557:
0558: public void performActionOnReturn(Return x) {
0559: DefaultAction def = new DefaultAction(x) {
0560: ProgramElement createNewElement(ExtList changeList) {
0561: return new Return(changeList);
0562: }
0563: };
0564: def.doAction(x);
0565: }
0566:
0567: public void performActionOnLessThan(LessThan x) {
0568: DefaultAction def = new DefaultAction(x) {
0569: ProgramElement createNewElement(ExtList changeList) {
0570: return new LessThan(changeList);
0571: }
0572: };
0573: def.doAction(x);
0574: }
0575:
0576: public void performActionOnParenthesizedExpression(
0577: ParenthesizedExpression x) {
0578: DefaultAction def = new DefaultAction(x) {
0579: ProgramElement createNewElement(ExtList changeList) {
0580: return new ParenthesizedExpression(changeList);
0581: }
0582: };
0583: def.doAction(x);
0584: }
0585:
0586: public void performActionOnPassiveExpression(PassiveExpression x) {
0587: DefaultAction def = new DefaultAction(x) {
0588: ProgramElement createNewElement(ExtList changeList) {
0589: return new PassiveExpression(changeList);
0590: }
0591: };
0592: def.doAction(x);
0593: }
0594:
0595: public void performActionOnTypeCast(TypeCast x) {
0596: DefaultAction def = new DefaultAction(x) {
0597: ProgramElement createNewElement(ExtList changeList) {
0598: return new TypeCast(changeList);
0599: }
0600: };
0601: def.doAction(x);
0602: }
0603:
0604: public void performActionOnGreaterThan(GreaterThan x) {
0605: DefaultAction def = new DefaultAction(x) {
0606: ProgramElement createNewElement(ExtList changeList) {
0607: return new GreaterThan(changeList);
0608: }
0609: };
0610: def.doAction(x);
0611: }
0612:
0613: public void performActionOnBinaryAnd(BinaryAnd x) {
0614: DefaultAction def = new DefaultAction(x) {
0615: ProgramElement createNewElement(ExtList changeList) {
0616: return new BinaryAnd(changeList);
0617: }
0618: };
0619: def.doAction(x);
0620: }
0621:
0622: public void performActionOnBinaryOr(BinaryOr x) {
0623: DefaultAction def = new DefaultAction(x) {
0624: ProgramElement createNewElement(ExtList changeList) {
0625: return new BinaryOr(changeList);
0626: }
0627: };
0628: def.doAction(x);
0629: }
0630:
0631: public void performActionOnBinaryXOr(BinaryXOr x) {
0632: DefaultAction def = new DefaultAction(x) {
0633: ProgramElement createNewElement(ExtList changeList) {
0634: return new BinaryXOr(changeList);
0635: }
0636: };
0637: def.doAction(x);
0638: }
0639:
0640: public void performActionOnBinaryNot(BinaryNot x) {
0641: DefaultAction def = new DefaultAction(x) {
0642: ProgramElement createNewElement(ExtList changeList) {
0643: return new BinaryNot(changeList);
0644: }
0645: };
0646: def.doAction(x);
0647: }
0648:
0649: public void performActionOnBinaryAndAssignment(BinaryAndAssignment x) {
0650: DefaultAction def = new DefaultAction(x) {
0651: ProgramElement createNewElement(ExtList changeList) {
0652: return new BinaryAndAssignment(changeList);
0653: }
0654: };
0655: def.doAction(x);
0656: }
0657:
0658: public void performActionOnBinaryOrAssignment(BinaryOrAssignment x) {
0659: DefaultAction def = new DefaultAction(x) {
0660: ProgramElement createNewElement(ExtList changeList) {
0661: return new BinaryOrAssignment(changeList);
0662: }
0663: };
0664: def.doAction(x);
0665: }
0666:
0667: public void performActionOnBinaryXOrAssignment(BinaryXOrAssignment x) {
0668: DefaultAction def = new DefaultAction(x) {
0669: ProgramElement createNewElement(ExtList changeList) {
0670: return new BinaryXOrAssignment(changeList);
0671: }
0672: };
0673: def.doAction(x);
0674: }
0675:
0676: public void performActionOnDivideAssignment(DivideAssignment x) {
0677: DefaultAction def = new DefaultAction(x) {
0678: ProgramElement createNewElement(ExtList changeList) {
0679: return new DivideAssignment(changeList);
0680: }
0681: };
0682: def.doAction(x);
0683: }
0684:
0685: public void performActionOnMinusAssignment(MinusAssignment x) {
0686: DefaultAction def = new DefaultAction(x) {
0687: ProgramElement createNewElement(ExtList changeList) {
0688: return new MinusAssignment(changeList);
0689: }
0690: };
0691: def.doAction(x);
0692: }
0693:
0694: public void performActionOnModuloAssignment(ModuloAssignment x) {
0695: DefaultAction def = new DefaultAction(x) {
0696: ProgramElement createNewElement(ExtList changeList) {
0697: return new ModuloAssignment(changeList);
0698: }
0699: };
0700: def.doAction(x);
0701: }
0702:
0703: public void performActionOnPlusAssignment(PlusAssignment x) {
0704: DefaultAction def = new DefaultAction(x) {
0705: ProgramElement createNewElement(ExtList changeList) {
0706: return new PlusAssignment(changeList);
0707: }
0708: };
0709: def.doAction(x);
0710: }
0711:
0712: public void performActionOnPostDecrement(PostDecrement x) {
0713: DefaultAction def = new DefaultAction(x) {
0714: ProgramElement createNewElement(ExtList changeList) {
0715: return new PostDecrement(changeList);
0716: }
0717: };
0718: def.doAction(x);
0719: }
0720:
0721: public void performActionOnPreDecrement(PreDecrement x) {
0722: DefaultAction def = new DefaultAction(x) {
0723: ProgramElement createNewElement(ExtList changeList) {
0724: return new PreDecrement(changeList);
0725: }
0726: };
0727: def.doAction(x);
0728: }
0729:
0730: public void performActionOnShiftLeftAssignment(ShiftLeftAssignment x) {
0731: DefaultAction def = new DefaultAction(x) {
0732: ProgramElement createNewElement(ExtList changeList) {
0733: return new ShiftLeftAssignment(changeList);
0734: }
0735: };
0736: def.doAction(x);
0737: }
0738:
0739: public void performActionOnShiftRightAssignment(
0740: ShiftRightAssignment x) {
0741: DefaultAction def = new DefaultAction(x) {
0742: ProgramElement createNewElement(ExtList changeList) {
0743: return new ShiftRightAssignment(changeList);
0744: }
0745: };
0746: def.doAction(x);
0747: }
0748:
0749: public void performActionOnTimesAssignment(TimesAssignment x) {
0750: DefaultAction def = new DefaultAction(x) {
0751: ProgramElement createNewElement(ExtList changeList) {
0752: return new TimesAssignment(changeList);
0753: }
0754: };
0755: def.doAction(x);
0756: }
0757:
0758: public void performActionOnConditional(Conditional x) {
0759: DefaultAction def = new DefaultAction(x) {
0760: ProgramElement createNewElement(ExtList changeList) {
0761: return new Conditional(changeList);
0762: }
0763: };
0764: def.doAction(x);
0765: }
0766:
0767: public void performActionOnUnsignedShiftRightAssignment(
0768: UnsignedShiftRightAssignment x) {
0769: DefaultAction def = new DefaultAction(x) {
0770: ProgramElement createNewElement(ExtList changeList) {
0771: return new UnsignedShiftRightAssignment(changeList);
0772: }
0773: };
0774: def.doAction(x);
0775: }
0776:
0777: public void performActionOnDivide(Divide x) {
0778: DefaultAction def = new DefaultAction(x) {
0779: ProgramElement createNewElement(ExtList changeList) {
0780: return new Divide(changeList);
0781: }
0782: };
0783: def.doAction(x);
0784: }
0785:
0786: public void performActionOnNewArray(NewArray x) {
0787: DefaultAction def = new DefaultAction(x) {
0788: NewArray y = (NewArray) pe;
0789:
0790: ProgramElement createNewElement(ExtList children) {
0791: ArrayInitializer arrInit = (ArrayInitializer) children
0792: .get(ArrayInitializer.class);
0793: children.remove(arrInit);
0794: return new NewArray(children, y.getKeYJavaType(),
0795: arrInit, y.getDimensions());
0796: }
0797: };
0798: def.doAction(x);
0799: }
0800:
0801: // ppp
0802: public void performActionOnNew(New x) {
0803: DefaultAction def = new DefaultAction(x) {
0804: ProgramElement createNewElement(ExtList children) {
0805: PositionInfo pi = (PositionInfo) children
0806: .removeFirstOccurrence(PositionInfo.class);
0807: if (!preservesPositionInfo) {
0808: pi = PositionInfo.UNDEFINED;
0809: }
0810: New y = (New) pe;
0811: ReferencePrefix rp = null;
0812: int rpPos = getPosition(y, y.getReferencePrefix());
0813: if (rpPos != -1) {
0814: rp = (ReferencePrefix) children.get(rpPos);
0815: children.remove(rpPos);
0816: }
0817: return new New(children, rp, pi);
0818: }
0819: };
0820: def.doAction(x);
0821: }
0822:
0823: public void performActionOnLogicalNot(LogicalNot x) {
0824: DefaultAction def = new DefaultAction(x) {
0825: ProgramElement createNewElement(ExtList changeList) {
0826: return new LogicalNot(changeList);
0827: }
0828: };
0829: def.doAction(x);
0830: }
0831:
0832: public void performActionOnLogicalAnd(LogicalAnd x) {
0833: DefaultAction def = new DefaultAction(x) {
0834: ProgramElement createNewElement(ExtList changeList) {
0835: return new LogicalAnd(changeList);
0836: }
0837: };
0838: def.doAction(x);
0839: }
0840:
0841: public void performActionOnLogicalOr(LogicalOr x) {
0842: DefaultAction def = new DefaultAction(x) {
0843: ProgramElement createNewElement(ExtList changeList) {
0844: return new LogicalOr(changeList);
0845: }
0846: };
0847: def.doAction(x);
0848: }
0849:
0850: public void performActionOnModulo(Modulo x) {
0851: DefaultAction def = new DefaultAction(x) {
0852: ProgramElement createNewElement(ExtList changeList) {
0853: return new Modulo(changeList);
0854: }
0855: };
0856: def.doAction(x);
0857: }
0858:
0859: public void performActionOnNegative(Negative x) {
0860: DefaultAction def = new DefaultAction(x) {
0861: ProgramElement createNewElement(ExtList changeList) {
0862: return new Negative(changeList);
0863: }
0864: };
0865: def.doAction(x);
0866: }
0867:
0868: public void performActionOnPositive(Positive x) {
0869: DefaultAction def = new DefaultAction(x) {
0870: ProgramElement createNewElement(ExtList changeList) {
0871: return new Positive(changeList);
0872: }
0873: };
0874: def.doAction(x);
0875: }
0876:
0877: public void performActionOnShiftLeft(ShiftLeft x) {
0878: DefaultAction def = new DefaultAction(x) {
0879: ProgramElement createNewElement(ExtList changeList) {
0880: return new ShiftLeft(changeList);
0881: }
0882: };
0883: def.doAction(x);
0884: }
0885:
0886: public void performActionOnShiftRight(ShiftRight x) {
0887: DefaultAction def = new DefaultAction(x) {
0888: ProgramElement createNewElement(ExtList changeList) {
0889: return new ShiftRight(changeList);
0890: }
0891: };
0892: def.doAction(x);
0893: }
0894:
0895: // ppp
0896: public void performActionOnArrayReference(ArrayReference x) {
0897: DefaultAction def = new DefaultAction(x) {
0898: ProgramElement createNewElement(ExtList children) {
0899: PositionInfo pos = (PositionInfo) children
0900: .removeFirstOccurrence(PositionInfo.class);
0901: ArrayReference y = (ArrayReference) pe;
0902: ReferencePrefix prefix = null;
0903: int prefixPos = getPosition(y, y.getReferencePrefix());
0904: if (prefixPos != -1) {
0905: prefix = (ReferencePrefix) children.get(prefixPos);
0906: children.remove(prefixPos);
0907: }
0908: if (!preservesPositionInfo) {
0909: pos = PositionInfo.UNDEFINED;
0910: }
0911: return new ArrayReference(children, prefix, pos);
0912: }
0913: };
0914: def.doAction(x);
0915: }
0916:
0917: public void performActionOnMetaClassReference(MetaClassReference x) {
0918: DefaultAction def = new DefaultAction(x) {
0919: ProgramElement createNewElement(ExtList changeList) {
0920: return new MetaClassReference(changeList);
0921: }
0922: };
0923: def.doAction(x);
0924: }
0925:
0926: // ppp
0927: public void performActionOnSuperConstructorReference(
0928: SuperConstructorReference x) {
0929: DefaultAction def = new DefaultAction(x) {
0930: ProgramElement createNewElement(ExtList children) {
0931: PositionInfo pos = (PositionInfo) children
0932: .removeFirstOccurrence(PositionInfo.class);
0933: SuperConstructorReference y = (SuperConstructorReference) pe;
0934: ReferencePrefix prefix = null;
0935: int prefixPos = getPosition(y, y.getReferencePrefix());
0936: if (prefixPos != -1) {
0937: prefix = (ReferencePrefix) children.get(prefixPos);
0938: children.remove(prefixPos);
0939: }
0940:
0941: if (!preservesPositionInfo) {
0942: pos = PositionInfo.UNDEFINED;
0943: }
0944:
0945: return new SuperConstructorReference(children, prefix,
0946: pos);
0947: }
0948: };
0949: def.doAction(x);
0950: }
0951:
0952: public void performActionOnThisConstructorReference(
0953: ThisConstructorReference x) {
0954: DefaultAction def = new DefaultAction(x) {
0955: ProgramElement createNewElement(ExtList changeList) {
0956: return new ThisConstructorReference(changeList);
0957: }
0958: };
0959: def.doAction(x);
0960: }
0961:
0962: public void performActionOnExecutionContext(ExecutionContext x) {
0963: DefaultAction def = new DefaultAction(x) {
0964: ProgramElement createNewElement(ExtList changeList) {
0965: return new ExecutionContext(changeList);
0966: }
0967: };
0968: def.doAction(x);
0969: }
0970:
0971: public void performActionOnSuperReference(final SuperReference x) {
0972: DefaultAction def = new DefaultAction(x) {
0973: ProgramElement createNewElement(ExtList changeList) {
0974: return new SuperReference(changeList);
0975: }
0976: };
0977: def.doAction(x);
0978: }
0979:
0980: public void performActionOnThisReference(final ThisReference x) {
0981: DefaultAction def = new DefaultAction(x) {
0982: ProgramElement createNewElement(ExtList changeList) {
0983: return new ThisReference(changeList);
0984: }
0985: };
0986: def.doAction(x);
0987: }
0988:
0989: public void performActionOnArrayLengthReference(
0990: ArrayLengthReference x) {
0991: DefaultAction def = new DefaultAction(x) {
0992: ProgramElement createNewElement(ExtList changeList) {
0993: return new ArrayLengthReference(changeList);
0994: }
0995: };
0996: def.doAction(x);
0997: }
0998:
0999: public void performActionOnSwitch(Switch x) {
1000: DefaultAction def = new DefaultAction(x) {
1001: ProgramElement createNewElement(ExtList changeList) {
1002: return new Switch(changeList);
1003: }
1004: };
1005: def.doAction(x);
1006: }
1007:
1008: public void performActionOnClassInitializer(ClassInitializer x) {
1009: DefaultAction def = new DefaultAction(x) {
1010: ProgramElement createNewElement(ExtList changeList) {
1011: return new ClassInitializer(changeList);
1012: }
1013: };
1014: def.doAction(x);
1015: }
1016:
1017: public void performActionOnArrayInitializer(ArrayInitializer x) {
1018: DefaultAction def = new DefaultAction(x) {
1019: ProgramElement createNewElement(ExtList changeList) {
1020: return new ArrayInitializer(changeList);
1021: }
1022: };
1023: def.doAction(x);
1024: }
1025:
1026: public void performActionOnPackageReference(PackageReference x) {
1027: DefaultAction def = new DefaultAction(x) {
1028: ProgramElement createNewElement(ExtList changeList) {
1029: return new PackageReference(changeList);
1030: }
1031: };
1032: def.doAction(x);
1033: }
1034:
1035: public void performActionOnPackageSpecification(
1036: PackageSpecification x) {
1037: DefaultAction def = new DefaultAction(x) {
1038: ProgramElement createNewElement(ExtList changeList) {
1039: return new PackageSpecification(changeList);
1040: }
1041: };
1042: def.doAction(x);
1043: }
1044:
1045: public void performActionOnLessOrEquals(LessOrEquals x) {
1046: DefaultAction def = new DefaultAction(x) {
1047: ProgramElement createNewElement(ExtList changeList) {
1048: return new LessOrEquals(changeList);
1049: }
1050: };
1051: def.doAction(x);
1052: }
1053:
1054: public void performActionOnGreaterOrEquals(GreaterOrEquals x) {
1055: DefaultAction def = new DefaultAction(x) {
1056: ProgramElement createNewElement(ExtList changeList) {
1057: return new GreaterOrEquals(changeList);
1058: }
1059: };
1060: def.doAction(x);
1061: }
1062:
1063: public void performActionOnLocalVariableDeclaration(
1064: LocalVariableDeclaration x) {
1065: DefaultAction def = new DefaultAction(x) {
1066: ProgramElement createNewElement(ExtList changeList) {
1067: return new LocalVariableDeclaration(changeList);
1068: }
1069: };
1070: def.doAction(x);
1071: }
1072:
1073: public void performActionOnParameterDeclaration(
1074: ParameterDeclaration x) {
1075: DefaultAction def = new ParameterDeclarationAction(x);
1076: def.doAction(x);
1077: }
1078:
1079: private class ParameterDeclarationAction extends DefaultAction {
1080: ParameterDeclaration x;
1081:
1082: ParameterDeclarationAction(ParameterDeclaration x) {
1083: super (x);
1084: this .x = x;
1085: }
1086:
1087: ProgramElement createNewElement(ExtList changeList) {
1088: return new ParameterDeclaration(changeList, x
1089: .parentIsInterfaceDeclaration());
1090: }
1091: }
1092:
1093: // eee
1094: public void performActionOnForUpdates(final ForUpdates x) {
1095: DefaultAction def = new DefaultAction(x) {
1096: ProgramElement createNewElement(ExtList changeList) {
1097: PositionInfo pi;
1098: if (!preservesPositionInfo) {
1099: pi = PositionInfo.UNDEFINED;
1100: } else {
1101: pi = (PositionInfo) changeList
1102: .removeFirstOccurrence(PositionInfo.class);
1103: }
1104: return new ForUpdates(changeList, pi);
1105: }
1106: };
1107: def.doAction(x);
1108: }
1109:
1110: public void performActionOnGuard(Guard x) {
1111: DefaultAction def = new DefaultAction(x) {
1112: ProgramElement createNewElement(ExtList changeList) {
1113: return new Guard(changeList);
1114: }
1115: };
1116: def.doAction(x);
1117: }
1118:
1119: public void performActionOnLoopInit(LoopInit x) {
1120: DefaultAction def = new DefaultAction(x) {
1121: ProgramElement createNewElement(ExtList changeList) {
1122: final PositionInfo pi;
1123: if (!preservesPositionInfo) {
1124: pi = PositionInfo.UNDEFINED;
1125: } else {
1126: pi = (PositionInfo) changeList
1127: .removeFirstOccurrence(PositionInfo.class);
1128: }
1129: return new LoopInit(changeList, pi);
1130: }
1131: };
1132: def.doAction(x);
1133: }
1134:
1135: public void performActionOnProgramSVProxy(ProgramSVProxy x) {
1136: DefaultAction def = new DefaultAction(x) {
1137: ProgramElement createNewElement(ExtList changeList) {
1138: return new ProgramSVProxy(changeList);
1139: }
1140: };
1141: def.doAction(x);
1142: }
1143:
1144: /**
1145: * returns the position of pe2 in the virtual child array of pe1
1146: */
1147: protected static int getPosition(NonTerminalProgramElement pe1,
1148: ProgramElement pe2) {
1149: int n = pe1.getChildCount();
1150: int i = 0;
1151: while ((i < n) && (pe1.getChildAt(i) != pe2))
1152: i++;
1153: return (i == n) ? -1 : i;
1154: }
1155:
1156: protected void changed() {
1157: ExtList list = stack.peek();
1158: if (list.isEmpty() || list.getFirst() != CHANGED) {
1159: list.addFirst(CHANGED);
1160: }
1161: }
1162:
1163: protected void addToTopOfStack(SourceElement x) {
1164: if (x != null) {
1165: ExtList list = stack.peek();
1166: list.add(x);
1167: }
1168: }
1169:
1170: protected void addChild(SourceElement x) {
1171: stack.pop();
1172: addToTopOfStack(x);
1173: }
1174:
1175: protected void addChildren(ArrayOfProgramElement arr) {
1176: stack.pop();
1177: for (int i = 0, sz = arr.size(); i < sz; i++) {
1178: addToTopOfStack(arr.getProgramElement(i));
1179: }
1180: }
1181:
1182: protected abstract class DefaultAction {
1183: abstract ProgramElement createNewElement(ExtList changeList);
1184:
1185: protected ProgramElement pe;
1186:
1187: protected DefaultAction(ProgramElement pe) {
1188: this .pe = pe;
1189: }
1190:
1191: protected void addNewChild(ExtList changeList) {
1192: addChild(createNewElement(changeList));
1193: changed();
1194: }
1195:
1196: public void doAction(ProgramElement x) {
1197: ExtList changeList = stack.peek();
1198: if (changeList.size() == 0) {
1199: doDefaultAction(x);
1200: return;
1201: }
1202: if (changeList.getFirst() == CHANGED) {
1203: changeList.removeFirst();
1204: if (!preservesPositionInfo) {
1205: changeList
1206: .removeFirstOccurrence(PositionInfo.class);
1207: }
1208: addNewChild(changeList);
1209: } else {
1210: doDefaultAction(x);
1211: }
1212: }
1213: }
1214: }
|