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

Class LineBreakpoint

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

All Implemented Interfaces:

IBreakpoint

public class LineBreakpoint
extends AbstractConditionalBreakpoint

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	classPath The path of the class this LineBreakpoint is associated with.
private int	lineNumber The line of the Breakpoint in the respective class.
protected int	methodEnd The end of the method containing the associated Breakpoint
protected int	methodStart The start of the method containing the associated Breakpoint

Constructor Summary

Constructors

Constructor and Description
LineBreakpoint(java.lang.String classPath, int lineNumber, int hitCount, IProgramMethod pm, Proof proof, java.lang.String condition, boolean enabled, boolean conditionEnabled, int methodStart, int methodEnd) Creates a new LineBreakpoint.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getClassPath()
int	getLineNumber() Returns the line number of the associated Breakpoint.
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.
private boolean	isInLine(SourceElement activeStatement)
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.
void	setClassPath(java.lang.String classPath)
protected boolean	shouldStopInLine(int line, java.lang.String path) Checks if the execution should stop in the given line for the given class.

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

conditionMet, 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

classPath

private java.lang.String classPath

The path of the class this LineBreakpoint is associated with.

lineNumber

private int lineNumber

The line of the Breakpoint in the respective class.

methodStart

protected int methodStart

The start of the method containing the associated Breakpoint

methodEnd

protected int methodEnd

The end of the method containing the associated Breakpoint

Constructor Detail

LineBreakpoint

public LineBreakpoint(java.lang.String classPath,
                      int lineNumber,
                      int hitCount,
                      IProgramMethod pm,
                      Proof proof,
                      java.lang.String condition,
                      boolean enabled,
                      boolean conditionEnabled,
                      int methodStart,
                      int methodEnd)
               throws SLTranslationException

Creates a new LineBreakpoint.

Parameters:

classPath - the path of the class the associated Breakpoint lies within

lineNumber - the line where the associated Breakpoint is located in the class

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

methodStart - the line the containing method of this breakpoint starts at

methodEnd - the line the containing method of this breakpoint ends at

Throws:

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

Method Detail

getStatementBlock

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.

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

shouldStopInLine

protected boolean shouldStopInLine(int line,
                                   java.lang.String path)

Checks if the execution should stop in the given line for the given class.

Parameters:

line - The current line of code, that the auto mode is evaluating

path - The path of the Class, that contains the currently evaluated code

Returns:

true if a JavaLineBreakpoint is in the given line and the condition evaluates to true and the Hitcount is exceeded, false otherwise

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

isInLine

private boolean isInLine(SourceElement activeStatement)

getLineNumber

public int getLineNumber()

Returns the line number of the associated Breakpoint.

Returns:

the line number of the associated 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.

getClassPath

public java.lang.String getClassPath()

Returns:

the classPath

setClassPath

public void setClassPath(java.lang.String classPath)

Parameters:

classPath - the classPath to set