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.rule.metaconstruct;
12:
13: import de.uka.ilkd.key.java.*;
14: import de.uka.ilkd.key.java.statement.Break;
15: import de.uka.ilkd.key.java.statement.LabeledStatement;
16: import de.uka.ilkd.key.rule.inst.SVInstantiations;
17:
18: /**
19: * This class performs a labeled break. This means
20: * <code>
21: * l1:l2:{l3:{l4:{break l3;}} ...}
22: * </code>
23: * becomes
24: * <code>
25: * l1:l2:{...}
26: * </code>
27: */
28: public class DoBreak extends ProgramMetaConstruct {
29:
30: /** creates a do-break ProgramMetaConstruct
31: * @param labeledBreak the LabeledStatement contained by
32: * the meta construct
33: */
34: public DoBreak(LabeledStatement labeledBreak) {
35: super ("do-break", labeledBreak);
36: }
37:
38: /** a helper method to perform the symbolic execution of the
39: * doBreak metaconstruct.
40: * @param block the NonTerminalProgramElement to go through and
41: * look for the label
42: * @param breakLabel the Label the break statement marked
43: */
44: private ProgramElement doBreak(NonTerminalProgramElement block,
45: Label breakLabel, Break b) {
46:
47: if (block instanceof LabeledStatement) {
48: // we enter a labeled block so we have to check the label
49: Label blockLabel = ((LabeledStatement) block).getLabel();
50: if (blockLabel.equals(breakLabel)) {
51: // skip this block
52: return new StatementBlock(new ArrayOfStatement(
53: new Statement[0]));
54: } else {
55: // we assume that the doBreak is only applied in case
56: // of success. That is why we create a new
57: // LabeledBlock here and why we assume that the body
58: // of this LabeledStatement is a NonTerminalProgramElement
59: return b;
60: }
61: }
62: return null;
63: }
64:
65: /** performs the program transformation needed for symbolic
66: * program transformation
67: * @param services the Services with all necessary information
68: * about the java programs
69: * @return the transformated program
70: */
71: public ProgramElement symbolicExecution(ProgramElement pe,
72: Services services, SVInstantiations insts) {
73: // get label of break
74: // ContextInstantiationEntry ctx = insts.getContextInstantiation();
75: // Break breakStmnt = (Break) PosInProgram.
76: // getProgramAt(ctx.prefix(), pe);
77: LabeledStatement lst = (LabeledStatement) pe;
78: Break breakStmnt;
79: if (lst.getChildAt(1) instanceof Break) {
80: breakStmnt = (Break) lst.getChildAt(1);
81: } else {
82: breakStmnt = (Break) ((StatementBlock) lst.getChildAt(1))
83: .getChildAt(0);
84: }
85: return doBreak((NonTerminalProgramElement) pe, breakStmnt
86: .getLabel(), breakStmnt);
87: }
88: }
|