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: package de.uka.ilkd.key.strategy.feature;
09:
10: import de.uka.ilkd.key.logic.PosInOccurrence;
11: import de.uka.ilkd.key.proof.Goal;
12: import de.uka.ilkd.key.rule.IteratorOfRuleSet;
13: import de.uka.ilkd.key.rule.RuleApp;
14: import de.uka.ilkd.key.rule.RuleSet;
15: import de.uka.ilkd.key.rule.TacletApp;
16: import de.uka.ilkd.key.visualdebugger.BreakpointManager;
17: import de.uka.ilkd.key.visualdebugger.SourceElementId;
18: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
19:
20: /**
21: * TODO changes this!!!!!!!!!
22: *
23: * @author baum
24: *
25: */
26: public class BreakpointFeature extends BinaryFeature {
27: BreakpointManager bpManager;
28:
29: private BreakpointFeature() {
30: bpManager = VisualDebugger.getVisualDebugger().getBpManager();
31: }
32:
33: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
34: try {
35: if (app instanceof TacletApp) {
36: TacletApp tapp = (TacletApp) app;
37: if (bpManager.isNoEx())
38: for (IteratorOfRuleSet it = tapp.taclet()
39: .getRuleSets().iterator(); it.hasNext();) {
40: RuleSet next = it.next();
41: if (next.name().toString().startsWith(
42: "method_expand"))
43: return true;
44: }
45:
46: SourceElementId id = VisualDebugger.getVisualDebugger()
47: .getProgramCounter(pos);
48: if (id != null) {
49: /* VisualDebugger.print("BP Manger for node "+goal.node().serialNr()+ " "+bpManager+ " StatementId "+id);
50: VisualDebugger.print("Reached StatementID "+id);
51: VisualDebugger.print("Parent StatementIdcount "+goal.node().parent().getNodeInfo().getVisualDebuggerState().getStatementIdcount());*/
52: if (bpManager.suspend(goal.node(), id)) {
53: return true;
54: }
55: }
56: }
57:
58: } catch (Exception e) {
59: e.printStackTrace();
60: }
61: return false;
62: }
63:
64: public static BreakpointFeature create() {
65: return new BreakpointFeature();
66: }
67:
68: }
|