de.uka.ilkd.key.symbolic_execution.object_model.impl

Class SymbolicAssociation

java.lang.Object

de.uka.ilkd.key.symbolic_execution.object_model.impl.AbstractElement

de.uka.ilkd.key.symbolic_execution.object_model.impl.SymbolicAssociation

All Implemented Interfaces:

ISymbolicAssociation, ISymbolicElement

public class SymbolicAssociation
extends AbstractElement
implements ISymbolicAssociation

Default implementation of ISymbolicAssociation.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	arrayEndIndex The array end index or null if not used.
private Term	arrayIndex The array index.
private Term	arrayStartIndex The array start index or null if not used.
private Term	condition The optional condition under which this association is valid.
private IProgramVariable	programVariable The IProgramVariable.
private Services	services The Services to use.
private ISymbolicObject	target The target ISymbolicObject.

Constructor Summary

Constructors

Constructor and Description
SymbolicAssociation(Services services, IProgramVariable programVariable, ISymbolicObject target, Term condition, IModelSettings settings) Constructor.
SymbolicAssociation(Services services, Term arrayIndex, ISymbolicObject target, Term condition, IModelSettings settings) Constructor.
SymbolicAssociation(Services services, Term arrayIndex, Term arrayStartIndex, Term arrayEndIndex, ISymbolicObject target, Term condition, IModelSettings settings) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	getArrayEndIndex() Returns the array end index.
java.lang.String	getArrayEndIndexString() Returns the human readable array end index.
Term	getArrayIndex() Returns the represented array index or null if a program variable is represented..
java.lang.String	getArrayIndexString() Returns the human readable array index or null if a program variable is represented..
Term	getArrayStartIndex() Returns the array start index.
java.lang.String	getArrayStartIndexString() Returns the human readable array start index.
Term	getCondition() Returns the optional condition under which this association is valid.
java.lang.String	getConditionString() Returns the optional condition under which this association is valid as human readable String.
java.lang.String	getName() Returns a human readable name.
IProgramVariable	getProgramVariable() Returns the represented IProgramVariable.
java.lang.String	getProgramVariableString() Returns the represented IProgramVariable as human readable String.
ISymbolicObject	getTarget() Returns the target ISymbolicObject.
boolean	isArrayIndex() Checks if an array index is represented.
boolean	isArrayRange() Checks if an array range is represented.
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.symbolic_execution.object_model.impl.AbstractElement

formatTerm, getSettings

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicElement

getSettings

Field Detail

services

private final Services services

The Services to use.

arrayIndex

private final Term arrayIndex

The array index.

arrayStartIndex

private final Term arrayStartIndex

The array start index or null if not used.

arrayEndIndex

private final Term arrayEndIndex

The array end index or null if not used.

programVariable

private final IProgramVariable programVariable

The IProgramVariable.

target

private final ISymbolicObject target

The target ISymbolicObject.

condition

private final Term condition

The optional condition under which this association is valid.

Constructor Detail

SymbolicAssociation

public SymbolicAssociation(Services services,
                           Term arrayIndex,
                           ISymbolicObject target,
                           Term condition,
                           IModelSettings settings)

Constructor.

Parameters:

services - The Services to use.

arrayIndex - The array index.

target - The target ISymbolicObject.

condition - The optional condition under which this association is valid.

settings - The IModelSettings to use.

SymbolicAssociation

public SymbolicAssociation(Services services,
                           Term arrayIndex,
                           Term arrayStartIndex,
                           Term arrayEndIndex,
                           ISymbolicObject target,
                           Term condition,
                           IModelSettings settings)

Constructor.

Parameters:

services - The Services to use.

arrayIndex - The array index.

arrayStartIndex - The array start index or null if not used.

arrayEndIndex - The array end index or null if not used.

target - The target ISymbolicObject.

condition - The optional condition under which this association is valid.

settings - The IModelSettings to use.

SymbolicAssociation

public SymbolicAssociation(Services services,
                           IProgramVariable programVariable,
                           ISymbolicObject target,
                           Term condition,
                           IModelSettings settings)

Constructor.

Parameters:

services - The Services to use.

programVariable - The IProgramVariable.

target - The target ISymbolicObject.

condition - The optional condition under which this association is valid.

settings - The IModelSettings to use.

Method Detail

getName

public java.lang.String getName()

Returns a human readable name.

Specified by:

getName in interface ISymbolicAssociation

Returns:

A human readable name.

isArrayIndex

public boolean isArrayIndex()

Checks if an array index is represented.

Specified by:

isArrayIndex in interface ISymbolicAssociation

Returns:

true is array index, false is something else.

isArrayRange

public boolean isArrayRange()

Checks if an array range is represented.

Returns:

true is array range, false is something else.

getArrayIndex

public Term getArrayIndex()

Returns the represented array index or null if a program variable is represented..

Specified by:

getArrayIndex in interface ISymbolicAssociation

Returns:

The represented array index or null if a program variable is represented..

getProgramVariable

public IProgramVariable getProgramVariable()

Returns the represented IProgramVariable.

Specified by:

getProgramVariable in interface ISymbolicAssociation

Returns:

The represented IProgramVariable.

getProgramVariableString

public java.lang.String getProgramVariableString()

Returns the represented IProgramVariable as human readable String.

Specified by:

getProgramVariableString in interface ISymbolicAssociation

Returns:

The represented IProgramVariable as human readable String.

getTarget

public ISymbolicObject getTarget()

Returns the target ISymbolicObject.

Specified by:

getTarget in interface ISymbolicAssociation

Returns:

The target ISymbolicObject.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getCondition

public Term getCondition()

Returns the optional condition under which this association is valid.

The condition should be null by default. Only in rare cases, e.g. path condition is not strong enough to describe the path completely, is a condition is provided.

Specified by:

getCondition in interface ISymbolicAssociation

Returns:

The optional condition under which this association is valid.

getConditionString

public java.lang.String getConditionString()

Returns the optional condition under which this association is valid as human readable String.

The condition should be null by default. Only in rare cases, e.g. path condition is not strong enough to describe the path completely, is a condition is provided.

Specified by:

getConditionString in interface ISymbolicAssociation

Returns:

The optional condition under which this association is valid as human readable String.

getArrayIndexString

public java.lang.String getArrayIndexString()

Returns the human readable array index or null if a program variable is represented..

Specified by:

getArrayIndexString in interface ISymbolicAssociation

Returns:

The human readable array index or null if a program variable is represented..

getArrayStartIndex

public Term getArrayStartIndex()

Returns the array start index.

Returns:

The array start index.

getArrayStartIndexString

public java.lang.String getArrayStartIndexString()

Returns the human readable array start index.

Returns:

The human readable array start index.

getArrayEndIndex

public Term getArrayEndIndex()

Returns the array end index.

Returns:

The array end index.

getArrayEndIndexString

public java.lang.String getArrayEndIndexString()

Returns the human readable array end index.

Returns:

The human readable array end index.