public class KeYWatchpoint extends AbstractConditionalBreakpoint
KeYWatchpoint
represents a KeY watchpoint and is responsible to tell the debugger to stop execution when the respective
watchpoint evaluates its condition to true.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 and Description |
---|
KeYWatchpoint(int hitCount,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
KeYJavaType containerType,
boolean suspendOnTrue)
Creates a new
AbstractConditionalBreakpoint . |
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) |
getCondition, getConditionString, getPm, getSelfVar, getToKeep, getVariableNamingMap, getVarsForCondition, isConditionEnabled, refreshVarMaps, setCondition, setConditionEnabled, setPm, setSelfVar, setVariableNamingMap, setVarsForCondition, updateState
getHitCount, hitcountExceeded, setHitCount
getProof, isEnabled, setEnabled
private boolean suspendOnTrue
public KeYWatchpoint(int hitCount, Proof proof, java.lang.String condition, boolean enabled, boolean conditionEnabled, KeYJavaType containerType, boolean suspendOnTrue) throws SLTranslationException
AbstractConditionalBreakpoint
. Call setCondition immediately after calling the constructor!hitCount
- the number of hits after which the execution should hold at this breakpointpm
- the IProgramMethod
representing the Method which the Breakpoint is located atproof
- the Proof
that will be executed and should stopcondition
- the condition as given by the userenabled
- flag if the Breakpoint is enabledconditionEnabled
- flag if the condition is enabledcontainerType
- the type of the element containing the breakpointsuspendOnTrue
- the flag if the condition needs to evaluate to true or just be satisfiableSLTranslationException
- if the condition could not be parsed to a valid Termprotected StatementBlock getStatementBlock(StatementContainer statementContainer)
AbstractConditionalBreakpoint
StatementContainer
this method computes the StatementBlock
that contains all lines before the line the Breakpoint is at, including the line itself.getStatementBlock
in class AbstractConditionalBreakpoint
statementContainer
- the StatementContainer
to build the block fromStatementBlock
representing the container without the line below the Breakpointprotected boolean isInScope(Node node)
AbstractConditionalBreakpoint
Node
is in the scope of this breakpoint.isInScope
in class AbstractConditionalBreakpoint
node
- the Node
to be checkedprotected boolean isInScopeForCondition(Node node)
AbstractConditionalBreakpoint
Node
is in the scope of this breakpoint.isInScopeForCondition
in class AbstractConditionalBreakpoint
node
- the Node
to be checkedprotected boolean conditionMet(RuleApp ruleApp, Proof proof, Node node)
AbstractConditionalBreakpoint
conditionMet
in class AbstractConditionalBreakpoint
ruleApp
- the RuleApp
to be executed nextproof
- the current Proof
node
- the current Node
public boolean isSuspendOnTrue()
public void setSuspendOnTrue(boolean suspendOnTrue)
public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node)
AbstractConditionalBreakpoint
isBreakpointHit
in interface IBreakpoint
isBreakpointHit
in class AbstractConditionalBreakpoint
activeStatement
- the activeStatement of the noderuleApp
- the applied RuleApp
proof
- the current proofnode
- the current node