public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBreakpoint
Constructor and Description |
---|
AbstractConditionalBreakpoint(int hitCount,
IProgramMethod pm,
Proof proof,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd,
KeYJavaType containerType)
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
|
Term |
getCondition()
Returns the condition of the associated Breakpoint.
|
java.lang.String |
getConditionString()
Returns the condition represented as a String.
|
IProgramMethod |
getPm() |
ProgramVariable |
getSelfVar() |
protected abstract 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. |
java.util.Set<LocationVariable> |
getToKeep()
Returns the variables KeY should keep to evaluate the condition.
|
java.util.Map<SVSubstitute,SVSubstitute> |
getVariableNamingMap() |
ImmutableList<ProgramVariable> |
getVarsForCondition() |
boolean |
isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
isConditionEnabled()
Checks if the condition for the associated Breakpoint is enabled.
|
protected abstract boolean |
isInScope(Node node)
Checks if the statement of a given
Node is in the scope of this breakpoint. |
protected abstract boolean |
isInScopeForCondition(Node node)
Checks if the statement of a given
Node is in the scope of this breakpoint. |
protected void |
refreshVarMaps(RuleApp ruleApp,
Node node)
Modifies toKeep and variableNamingMap to hold the correct parameters after execution of the given ruleApp on the given node
|
void |
setCondition(java.lang.String condition)
Sets the condition to the Term that is parsed from the given String.
|
void |
setConditionEnabled(boolean conditionEnabled)
Sets the new conditionEnabled value.
|
void |
setPm(IProgramMethod pm) |
void |
setSelfVar(ProgramVariable selfVar) |
void |
setVariableNamingMap(java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap) |
void |
setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition) |
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 . |
getHitCount, hitcountExceeded, setHitCount
getProof, isEnabled, setEnabled
public AbstractConditionalBreakpoint(int hitCount, IProgramMethod pm, Proof proof, boolean enabled, boolean conditionEnabled, int methodStart, int methodEnd, KeYJavaType containerType)
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 stopenabled
- flag if the Breakpoint is enabledconditionEnabled
- flag if the condition is enabledmethodStart
- the line the containing method of this breakpoint starts atmethodEnd
- the line the containing method of this breakpoint ends atcontainerType
- the type of the element containing the breakpointpublic void updateState(int maxApplications, long timeout, Proof proof, long startTime, int countApplied, Goal goal)
StopCondition.isGoalAllowed(int, long, Proof, long, int, Goal)
and can be used to update the state of the IBreakpoint
.updateState
in interface IBreakpoint
updateState
in class AbstractBreakpoint
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.protected void refreshVarMaps(RuleApp ruleApp, Node node)
ruleApp
- the applied rule appnodethe
- current nodeprotected boolean conditionMet(RuleApp ruleApp, Proof proof, Node node)
public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node)
isBreakpointHit
in interface IBreakpoint
isBreakpointHit
in class AbstractHitCountBreakpoint
activeStatement
- the activeStatement of the noderuleApp
- the applied RuleApp
proof
- the current proofnode
- the current nodeprotected abstract StatementBlock getStatementBlock(StatementContainer statementContainer)
StatementContainer
this method computes the StatementBlock
that contains all lines before the line the Breakpoint is at, including the line itself.statementContainer
- the StatementContainer
to build the block fromStatementBlock
representing the container without the line below the Breakpointprotected abstract boolean isInScope(Node node)
Node
is in the scope of this breakpoint.node
- the Node
to be checkedprotected abstract boolean isInScopeForCondition(Node node)
Node
is in the scope of this breakpoint.node
- the Node
to be checkedpublic void setConditionEnabled(boolean conditionEnabled)
conditionEnabled
- the new valuepublic Term getCondition()
public boolean isConditionEnabled()
conditionEnabled
- true if the condition for the associated Breakpoint is enabledpublic void setCondition(java.lang.String condition) throws SLTranslationException
condition
- the String to be parsedSLTranslationException
- if the parsing failedpublic java.lang.String getConditionString()
public java.util.Set<LocationVariable> getToKeep()
public java.util.Map<SVSubstitute,SVSubstitute> getVariableNamingMap()
public void setVariableNamingMap(java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap)
variableNamingMap
- the variableNamingMap to setpublic ProgramVariable getSelfVar()
public void setSelfVar(ProgramVariable selfVar)
selfVar
- the selfVar to setpublic ImmutableList<ProgramVariable> getVarsForCondition()
public void setVarsForCondition(ImmutableList<ProgramVariable> varsForCondition)
varsForCondition
- the varsForCondition to setpublic IProgramMethod getPm()
public void setPm(IProgramMethod pm)
pm
- the pm to setCopyright © 2003-2019 The KeY-Project.