public class SymbolicExecutionBreakpointStopCondition extends ExecutedSymbolicExecutionTreeNodesStopCondition implements IBreakpointStopCondition
IBreakpointStopCondition
which can be used during symbolic execution.Modifier and Type | Field and Description |
---|---|
private java.util.Set<IBreakpoint> |
breakpoints
The used
IBreakpoint s. |
MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_FOR_ONE_STEP, MAXIMAL_NUMBER_OF_SET_NODES_TO_EXECUTE_PER_GOAL_IN_COMPLETE_RUN
Constructor and Description |
---|
SymbolicExecutionBreakpointStopCondition(IBreakpoint... breakpoints)
Creates a new
SymbolicExecutionBreakpointStopCondition . |
Modifier and Type | Method and Description |
---|---|
void |
addBreakpoint(IBreakpoint breakpoint)
Adds a new
IBreakpoint . |
java.util.Set<IBreakpoint> |
getBreakpoints()
Returns all available
IBreakpoint s. |
int |
getMaximalWork(int maxApplications,
long timeout,
Proof proof)
Returns the maximal amount of work needed to complete the task,
used to display a progress bar.
|
protected void |
handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected boolean |
isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
boolean |
isGoalAllowed(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal)
Checks if it is allowed to apply the next rule on the selected
Goal
chosen by the GoalChooser before it is applied. |
void |
removeBreakpoint(IBreakpoint breakpoint)
Removes an
IBreakpoint . |
getExectuedSetNodesPerGoal, getGoalNotAllowedMessage, getMaximalNumberOfSetNodesToExecutePerGoal, getStopMessage, handleNodeLimitExceeded, setMaximalNumberOfSetNodesToExecutePerGoal, shouldStop, wasSetNodeExecuted
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getGoalNotAllowedMessage, getStopMessage, shouldStop
private final java.util.Set<IBreakpoint> breakpoints
IBreakpoint
s.public SymbolicExecutionBreakpointStopCondition(IBreakpoint... breakpoints)
SymbolicExecutionBreakpointStopCondition
.breakpoints
- The IBreakpoint
to use.public int getMaximalWork(int maxApplications, long timeout, Proof proof)
0
to indicate unknown size.getMaximalWork
in interface StopCondition
getMaximalWork
in class ExecutedSymbolicExecutionTreeNodesStopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.0
if it is unknown.public boolean isGoalAllowed(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal)
Goal
chosen by the GoalChooser
before it is applied.
If it is not allowed the apply strategy will stop.isGoalAllowed
in interface StopCondition
isGoalAllowed
in class ExecutedSymbolicExecutionTreeNodesStopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.currentTimeMillis()
countApplied
- The number of already applied rules.goal
- The current Goal
on which the next rule will be applied.true
rule application is allowed, false
rule application is not allowed so stop apply strategyprotected void handleNodeLimitNotExceeded(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal, Node node, RuleApp ruleApp, java.lang.Integer executedNumberOfSetNodes)
handleNodeLimitNotExceeded
in class ExecutedSymbolicExecutionTreeNodesStopCondition
maxApplications
- The defined maximal number of rules to apply. Can be different to StrategySettings.getMaxSteps()
in side proofs.timeout
- The defined timeout in ms or -1
if disabled. Can be different to StrategySettings.getTimeout()
in side proofs.proof
- The current Proof
.startTime
- The timestamp when the apply strategy has started, computed via System.nanoTime()
countApplied
- The number of already applied rules.goal
- The current Goal
on which the next rule will be applied.node
- The Node
of the current Goal
.ruleApp
- The current RuleApp
.executedNumberOfSetNodes
- The executed number of SET nodes.protected boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node)
activeStatement
- the activeStatement of the noderuleApp
- the applied RuleApp
proof
- the current proofnode
- the current nodetrue
at least one breakpoint is hit, false
all breakpoints are not hit.public void addBreakpoint(IBreakpoint breakpoint)
IBreakpoint
.addBreakpoint
in interface IBreakpointStopCondition
breakpoint
- The IBreakpoint
to add.public void removeBreakpoint(IBreakpoint breakpoint)
IBreakpoint
.removeBreakpoint
in interface IBreakpointStopCondition
breakpoint
- The IBreakpoint
to remove.public java.util.Set<IBreakpoint> getBreakpoints()
IBreakpoint
s.getBreakpoints
in interface IBreakpointStopCondition
IBreakpoint
s.