-
Notifications
You must be signed in to change notification settings - Fork 22
/
ExecutionLoopStatement.java
80 lines (75 loc) · 2.7 KB
/
ExecutionLoopStatement.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
package de.uka.ilkd.key.symbolic_execution.model.impl;
import de.uka.ilkd.key.java.PrettyPrinter;
import de.uka.ilkd.key.java.statement.*;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionConstraint;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionLoopStatement;
import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
import de.uka.ilkd.key.symbolic_execution.model.ITreeSettings;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
/**
* The default implementation of {@link IExecutionLoopStatement}.
*
* @author Martin Hentschel
*/
public class ExecutionLoopStatement extends AbstractExecutionBlockStartNode<LoopStatement>
implements IExecutionLoopStatement {
/**
* Constructor.
*
* @param settings The {@link ITreeSettings} to use.
* @param proofNode The {@link Node} of KeY's proof tree which is represented by this
* {@link IExecutionNode}.
*/
public ExecutionLoopStatement(ITreeSettings settings, Node proofNode) {
super(settings, proofNode);
}
/**
* {@inheritDoc}
*/
@Override
protected String lazyComputeName() {
LoopStatement ls = getActiveStatement();
if (ls.getGuardExpression() != null) {
if (ls instanceof While) {
StringBuilder sw = new StringBuilder();
PrettyPrinter sb = new PrettyPrinter(sw, true);
sb.printWhile((While) ls, false);
return sw.toString();
} else if (ls instanceof For) {
StringBuilder sw = new StringBuilder();
PrettyPrinter sb = new PrettyPrinter(sw, true);
sb.printFor((For) ls, false);
return sw.toString();
} else if (ls instanceof EnhancedFor) {
StringBuilder sw = new StringBuilder();
PrettyPrinter sb = new PrettyPrinter(sw, true);
sb.printEnhancedFor((EnhancedFor) ls, false);
return sw.toString();
} else if (ls instanceof Do) {
StringBuilder sw = new StringBuilder();
PrettyPrinter sb = new PrettyPrinter(sw, true);
sb.printDo((Do) ls, false);
return sw.toString();
} else {
return ls.toString();
}
} else {
return ls.toString();
}
}
/**
* {@inheritDoc}
*/
@Override
protected IExecutionConstraint[] lazyComputeConstraints() {
return SymbolicExecutionUtil.createExecutionConstraints(this);
}
/**
* {@inheritDoc}
*/
@Override
public String getElementType() {
return "Loop Statement";
}
}