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

Class KeYWatchpoint

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.AbstractConditionalBreakpoint

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

All Implemented Interfaces:

IBreakpoint

public class KeYWatchpoint
extends AbstractConditionalBreakpoint

ThisKeYWatchpoint represents a KeY watchpoint and is responsible to tell the debugger to stop execution when the respective watchpoint evaluates its condition to true.

Author:

Marco Drebing

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	suspendOnTrue a flag to tell whether the condition should evaluate to true or just be satisfiable

Constructor Summary

Constructors

Constructor and Description
KeYWatchpoint(int hitCount, Proof proof, java.lang.String condition, boolean enabled, boolean conditionEnabled, KeYJavaType containerType, boolean suspendOnTrue) Creates a new AbstractConditionalBreakpoint.

Method Summary

Modifier and Type	Method and Description
protected boolean	conditionMet(RuleApp ruleApp, Proof proof, Node node) Checks if the condition, that was given by the user, evaluates to true with the current of the proof
protected StatementBlock	getStatementBlock(StatementContainer statementContainer) For a given StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself.
boolean	isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node) Determines if the breakpoint represented by this BreakpointStopConition is triggered.
protected boolean	isInScope(Node node) Checks if the statement of a given Node is in the scope of this breakpoint.
protected boolean	isInScopeForCondition(Node node) Checks if the statement of a given Node is in the scope of this breakpoint.
boolean	isSuspendOnTrue()
void	setSuspendOnTrue(boolean suspendOnTrue)

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

getCondition, getConditionString, getPm, getSelfVar, getToKeep, getVariableNamingMap, getVarsForCondition, isConditionEnabled, refreshVarMaps, setCondition, setConditionEnabled, setPm, setSelfVar, setVariableNamingMap, setVarsForCondition, updateState

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

suspendOnTrue

private boolean suspendOnTrue

a flag to tell whether the condition should evaluate to true or just be satisfiable

Constructor Detail

KeYWatchpoint

public KeYWatchpoint(int hitCount,
                     Proof proof,
                     java.lang.String condition,
                     boolean enabled,
                     boolean conditionEnabled,
                     KeYJavaType containerType,
                     boolean suspendOnTrue)
              throws SLTranslationException

Creates a new AbstractConditionalBreakpoint. Call setCondition immediately after calling the constructor!

Parameters:

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

pm - the IProgramMethod representing the Method which the Breakpoint is located at

proof - the Proof that will be executed and should stop

condition - the condition as given by the user

enabled - flag if the Breakpoint is enabled

conditionEnabled - flag if the condition is enabled

containerType - the type of the element containing the breakpoint

suspendOnTrue - the flag if the condition needs to evaluate to true or just be satisfiable

Throws:

SLTranslationException - if the condition could not be parsed to a valid Term

Method Detail

getStatementBlock

protected StatementBlock getStatementBlock(StatementContainer statementContainer)

Description copied from class: AbstractConditionalBreakpoint

For a given StatementContainer this method computes the StatementBlock that contains all lines before the line the Breakpoint is at, including the line itself.

Specified by:

getStatementBlock in class AbstractConditionalBreakpoint

Parameters:

statementContainer - the StatementContainer to build the block from

Returns:

the StatementBlock representing the container without the line below the Breakpoint

isInScope

protected boolean isInScope(Node node)

Description copied from class: AbstractConditionalBreakpoint

Checks if the statement of a given Node is in the scope of this breakpoint.

Specified by:

isInScope in class AbstractConditionalBreakpoint

Parameters:

node - the Node to be checked

Returns:

true if the node represents a statement in the scope of this breakpoint.

isInScopeForCondition

protected boolean isInScopeForCondition(Node node)

Description copied from class: AbstractConditionalBreakpoint

Checks if the statement of a given Node is in the scope of this breakpoint.

Specified by:

isInScopeForCondition in class AbstractConditionalBreakpoint

Parameters:

node - the Node to be checked

Returns:

true if the node represents a statement in the scope of this breakpoint.

conditionMet

protected boolean conditionMet(RuleApp ruleApp,
                               Proof proof,
                               Node node)

Description copied from class: AbstractConditionalBreakpoint

Checks if the condition, that was given by the user, evaluates to true with the current of the proof

Overrides:

conditionMet in class AbstractConditionalBreakpoint

Parameters:

ruleApp - the RuleApp to be executed next

proof - the current Proof

node - the current Node

Returns:

true if the condition evaluates to true

isSuspendOnTrue

public boolean isSuspendOnTrue()

setSuspendOnTrue

public void setSuspendOnTrue(boolean suspendOnTrue)

isBreakpointHit

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

Description copied from class: AbstractConditionalBreakpoint

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 AbstractConditionalBreakpoint

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