de.uka.ilkd.key.symbolic_execution.strategy.breakpoint

Class SymbolicExecutionExceptionBreakpoint

java.lang.Object

de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractBreakpoint

de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractHitCountBreakpoint

de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.SymbolicExecutionExceptionBreakpoint

All Implemented Interfaces:

IBreakpoint

public class SymbolicExecutionExceptionBreakpoint
extends AbstractHitCountBreakpoint

ThisSymbolicExecutionExceptionBreakpoint represents an exception breakpoint and is responsible to tell the debugger to stop execution when the respective breakpoint is hit.

Author:

Marco Drebing

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	caught a flag whether to watch for an uncaught exception
private java.lang.String	exceptionName The exception to watch for
private java.util.Set<Node>	exceptionNodes a Set of Nodes that represent exceptions
private java.util.Set<Node>	exceptionParentNodes a list of nodes of the Symbolic Execution Tree whose children represent exceptions
private boolean	suspendOnSubclasses a flag whether to suspend on subclasses of the exception aswell
private boolean	uncaught a flag to tell whether to stop at uncaught exceptions or not

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionExceptionBreakpoint(Proof proof, java.lang.String exceptionName, boolean caught, boolean uncaught, boolean suspendOnSubclasses, boolean enabled, int hitCount) Creates a new AbstractHitCountBreakpoint.

Method Summary

Modifier and Type	Method and Description
boolean	isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node) Determines if the breakpoint represented by this BreakpointStopConition is triggered.
boolean	isCaught()
boolean	isParentNode(Node node, Node parent) Checks if the given node is a parent of the other given node.
boolean	isSuspendOnSubclasses()
boolean	isUncaught()
void	setCaught(boolean isCaught)
void	setSuspendOnSubclasses(boolean suspendOnSubclasses)
void	setUncaught(boolean isUncaught)
void	updateState(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal) This method is called from StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal) and can be used to update the state of the IBreakpoint.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractHitCountBreakpoint

getHitCount, hitcountExceeded, setHitCount

Methods inherited from class de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractBreakpoint

getProof, isEnabled, setEnabled

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

exceptionName

private java.lang.String exceptionName

The exception to watch for

exceptionNodes

private java.util.Set<Node> exceptionNodes

a Set of Nodes that represent exceptions

exceptionParentNodes

private java.util.Set<Node> exceptionParentNodes

a list of nodes of the Symbolic Execution Tree whose children represent exceptions

caught

private boolean caught

a flag whether to watch for an uncaught exception

suspendOnSubclasses

private boolean suspendOnSubclasses

a flag whether to suspend on subclasses of the exception aswell

uncaught

private boolean uncaught

a flag to tell whether to stop at uncaught exceptions or not

Constructor Detail

SymbolicExecutionExceptionBreakpoint

public SymbolicExecutionExceptionBreakpoint(Proof proof,
                                            java.lang.String exceptionName,
                                            boolean caught,
                                            boolean uncaught,
                                            boolean suspendOnSubclasses,
                                            boolean enabled,
                                            int hitCount)

Creates a new AbstractHitCountBreakpoint.

Parameters:

proof - the Proof that will be executed and should stop

exceptionName - the name of the exception to watch for

caught - flag to tell if caught exceptions lead to a stop

uncaught - flag to tell if uncaught exceptions lead to a stop

suspendOnSubclasses - flag to tell if the execution should suspend on subclasses of the exception aswell

enabled - flag if the Breakpoint is enabled

hitCount - the number of hits after which the execution should hold at this breakpoint

Method Detail

updateState

public void updateState(int maxApplications,
                        long timeout,
                        Proof proof,
                        long startTime,
                        int countApplied,
                        Goal goal)

This method is called from StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal) and can be used to update the state of the IBreakpoint.

Specified by:

updateState in interface IBreakpoint

Overrides:

updateState in class AbstractBreakpoint

Parameters:

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.

isParentNode

public boolean isParentNode(Node node,
                            Node parent)

Checks if the given node is a parent of the other given node.

Parameters:

node - The Node to start search in.

node - The Node that is thought to be the parent.

Returns:

true if the parent node is one of the nodes parents

isBreakpointHit

public boolean isBreakpointHit(SourceElement activeStatement,
                               RuleApp ruleApp,
                               Proof proof,
                               Node node)

Determines if the breakpoint represented by this BreakpointStopConition is triggered. Override this method in order to suspend execution when a breakpoint is hit.

Specified by:

isBreakpointHit in interface IBreakpoint

Overrides:

isBreakpointHit in class AbstractHitCountBreakpoint

Parameters:

activeStatement - the activeStatement of the node

ruleApp - the applied RuleApp

proof - the current proof

node - the current node

Returns:

true if execution should hold

isCaught

public boolean isCaught()

Returns:

the isCaught

setCaught

public void setCaught(boolean isCaught)

Parameters:

isCaught - the isCaught to set

isUncaught

public boolean isUncaught()

Returns:

the isUncaught

setUncaught

public void setUncaught(boolean isUncaught)

Parameters:

isUncaught - the isUncaught to set

isSuspendOnSubclasses

public boolean isSuspendOnSubclasses()

Returns:

the suspendOnSubclasses

setSuspendOnSubclasses

public void setSuspendOnSubclasses(boolean suspendOnSubclasses)

Parameters:

suspendOnSubclasses - the suspendOnSubclasses to set