public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBreakpoint
Modifier and Type | Field and Description |
---|---|
private Term |
condition
The condition for this Breakpoint (set by user).
|
private boolean |
conditionEnabled
The flag if the the condition for the associated Breakpoint is enabled
|
private java.lang.String |
conditionString
The condition of the associated breakpoint saved as a String
|
private KeYJavaType |
containerType
The KeYJavaType of the container of the element associated with the breakpoint.
|
private java.util.Set<LocationVariable> |
paramVars
The list of parameter variables of the method that contains the associated breakpoint
|
private IProgramMethod |
pm
The
IProgramMethod this Breakpoint lies within |
private ProgramVariable |
selfVar
A
ProgramVariable representing the instance the class KeY is working on |
private java.util.Set<LocationVariable> |
toKeep
A list of variables KeY has to hold to evaluate the condition
|
private java.util.Map<SVSubstitute,SVSubstitute> |
variableNamingMap
A
Map mapping from relevant variables for the condition to their runtime equivalent in KeY |
private ImmutableList<ProgramVariable> |
varsForCondition
A list of
ProgramVariable s containing all variables that were parsed and have to be possibly replaced during runtime. |
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 |
---|---|
private Term |
computeTermForCondition(java.lang.String condition)
Computes the Term that can be evaluated, from the user given condition
|
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
|
private void |
freeVariablesAfterReturn(Node node,
RuleApp ruleApp,
boolean inScope)
removes all stored parameters in to Keep when the ruleApp on the current node would induce a method return
|
Term |
getCondition()
Returns the condition of the associated Breakpoint.
|
java.lang.String |
getConditionString()
Returns the condition represented as a String.
|
private java.util.Map<SVSubstitute,SVSubstitute> |
getOldMap()
Returns a map containing the same entries as the variableNamingMap changes in one map do not effect the other map
|
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. |
private void |
putValuesFromGlobalVars(ProgramVariable varForCondition,
Node node,
boolean inScope)
put values in toKeep and variableNamingMap that can be found in the global variables of the node
|
private void |
putValuesFromRenamings(ProgramVariable varForCondition,
Node node,
boolean inScope,
java.util.Map<SVSubstitute,SVSubstitute> oldMap,
RuleApp ruleApp)
put relevant values from the current nodes renamings in toKeep and variableNamingMap
|
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
|
private ImmutableList<ProgramVariable> |
saveAddVariable(LocationVariable x,
ImmutableList<ProgramVariable> varsForCondition) |
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
private Term condition
private boolean conditionEnabled
private java.lang.String conditionString
private ImmutableList<ProgramVariable> varsForCondition
ProgramVariable
s containing all variables that were parsed and have to be possibly replaced during runtime.private KeYJavaType containerType
private java.util.Set<LocationVariable> toKeep
private java.util.Map<SVSubstitute,SVSubstitute> variableNamingMap
Map
mapping from relevant variables for the condition to their runtime equivalent in KeYprivate java.util.Set<LocationVariable> paramVars
private ProgramVariable selfVar
ProgramVariable
representing the instance the class KeY is working onprivate IProgramMethod pm
IProgramMethod
this Breakpoint lies withinpublic 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.private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node, boolean inScope)
varForCondition
- node
- inScope
- private java.util.Map<SVSubstitute,SVSubstitute> getOldMap()
private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScope)
node
- ruleApp
- inScope
- private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope, java.util.Map<SVSubstitute,SVSubstitute> oldMap, RuleApp ruleApp)
varForCondition
- the variable that might be relevant for the conditionnode
- the currentinScope
- the flag to determine if the current statement is in the scope of the breakpointoldMap
- the oldMap variableNamingsprotected void refreshVarMaps(RuleApp ruleApp, Node node)
ruleApp
- the applied rule appnodethe
- current nodeprivate Term computeTermForCondition(java.lang.String condition) throws SLTranslationException
condition
- the condition given by the userTerm
that represents the conditionSLTranslationException
- if the Term could not be parsedprotected 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 checkedprivate ImmutableList<ProgramVariable> saveAddVariable(LocationVariable x, ImmutableList<ProgramVariable> varsForCondition)
public 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 set