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

Class FieldWatchpoint

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

All Implemented Interfaces:

IBreakpoint

public class FieldWatchpoint
extends AbstractHitCountBreakpoint

ThisFieldWatchpoint represents a Java watchpoint and is responsible to tell the debugger to stop execution when the respective variable is accessed or modified.

Author:

Marco Drebing

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	fullFieldName
private boolean	isAccess
private boolean	isModification

Constructor Summary

Constructors

Constructor and Description
FieldWatchpoint(boolean enabled, int hitCount, java.lang.String fieldName, boolean isAcces, boolean isModification, KeYJavaType containerKJT, Proof proof) Creates a new FieldWatchpoint.

Method Summary

Modifier and Type	Method and Description
private boolean	checkChildrenOfSourceElement(SourceElement sourceElement)
boolean	isAccess()
boolean	isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, Proof proof, Node node) Determines if the breakpoint represented by this BreakpointStopConition is triggered.
boolean	isModification()
void	setAccess(boolean isAccess)
void	setModification(boolean isModification)

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

isAccess

private boolean isAccess

isModification

private boolean isModification

fullFieldName

private java.lang.String fullFieldName

Constructor Detail

FieldWatchpoint

public FieldWatchpoint(boolean enabled,
                       int hitCount,
                       java.lang.String fieldName,
                       boolean isAcces,
                       boolean isModification,
                       KeYJavaType containerKJT,
                       Proof proof)

Creates a new FieldWatchpoint.

Parameters:

enabled - flag if the Breakpoint is enabled

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

fieldName - the field to watch

isAcces - flag to watch for accesses

isModification - flag to watch for modifications

containerType - the type of the element containing the breakpoint

proof - the Proof that will be executed and should stop

Method Detail

isBreakpointHit

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

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 AbstractHitCountBreakpoint

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

checkChildrenOfSourceElement

private boolean checkChildrenOfSourceElement(SourceElement sourceElement)

isAccess

public boolean isAccess()

Returns:

the isAccess

setAccess

public void setAccess(boolean isAccess)

Parameters:

isAccess - the isAccess to set

isModification

public boolean isModification()

Returns:

the isModification

setModification

public void setModification(boolean isModification)

Parameters:

isModification - the isModification to set