public class ObserverFunction extends Function implements IObserverFunction
Modifier and Type | Field and Description |
---|---|
private KeYJavaType |
container |
private int |
heapCount |
private boolean |
isStatic |
private ImmutableArray<KeYJavaType> |
paramTypes |
private int |
stateCount |
private KeYJavaType |
type |
Constructor and Description |
---|
ObserverFunction(java.lang.String baseName,
Sort sort,
KeYJavaType type,
Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
Modifier and Type | Method and Description |
---|---|
static ProgramElementName |
createName(java.lang.String baseName,
KeYJavaType container) |
private static Sort[] |
getArgSorts(Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
KeYJavaType |
getContainerType()
Returns the container type of this symbol; for non-static observer
symbols, this corresponds to the sort of its second argument.
|
int |
getHeapCount(Services services)
Check the heap count of the declaration, e.g. the base heap and extra heap.
|
int |
getNumParams()
Gives the number of parameters of the observer symbol.
|
KeYJavaType |
getParamType(int i)
Gives the type of the i-th parameter of this observer symbol.
|
ImmutableArray<KeYJavaType> |
getParamTypes()
Returns the parameter types of this observer symbol.
|
int |
getStateCount()
Check the state count of the declaration (no_state = 0, two_state = 2, 1 otherwise).
|
KeYJavaType |
getType()
Returns the result type of this symbol.
|
boolean |
isStatic()
Tells whether the observer symbol is static.
|
isSkolemConstant, isUnique, proofToString, rename, toString
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel
private final KeYJavaType container
private final boolean isStatic
private final ImmutableArray<KeYJavaType> paramTypes
private final KeYJavaType type
private final int heapCount
private final int stateCount
public ObserverFunction(java.lang.String baseName, Sort sort, KeYJavaType type, Sort heapSort, KeYJavaType container, boolean isStatic, ImmutableArray<KeYJavaType> paramTypes, int heapCount, int stateCount)
public static ProgramElementName createName(java.lang.String baseName, KeYJavaType container)
private static Sort[] getArgSorts(Sort heapSort, KeYJavaType container, boolean isStatic, ImmutableArray<KeYJavaType> paramTypes, int heapCount, int stateCount)
public final KeYJavaType getType()
IObserverFunction
getType
in interface IObserverFunction
public final KeYJavaType getContainerType()
IObserverFunction
getContainerType
in interface IObserverFunction
public final boolean isStatic()
IObserverFunction
isStatic
in interface IObserverFunction
public int getStateCount()
IObserverFunction
getStateCount
in interface IObserverFunction
public int getHeapCount(Services services)
IObserverFunction
getHeapCount
in interface IObserverFunction
public final int getNumParams()
IObserverFunction
getNumParams
in interface IObserverFunction
public final KeYJavaType getParamType(int i)
IObserverFunction
getParamType
in interface IObserverFunction
public final ImmutableArray<KeYJavaType> getParamTypes()
IObserverFunction
getParamTypes
in interface IObserverFunction