Class | Description |
---|---|
AbstractOrInterfaceType |
This variable condition checks if a given type denotes an abstract class or
interface type.
|
AlternativeVariableCondition |
disjoin two variable conditions
|
ApplyUpdateOnRigidCondition | |
ArrayComponentTypeCondition |
This variable condition checks if an array component is of reference type
|
ArrayLengthCondition | |
ArrayTypeCondition |
This variable condition checks if an instantiation is an array.
|
ConstantCondition |
This variable condition checks if an instantiation is a constant formula or term,
i.e. its arity is equal to zero.
|
ContainsAssignmentCondition |
This variable condition can be used to check whether an assignment expression
occurs as a subexpression of a schemavariable instantiation,
|
ContainsAssignmentCondition.ContainsAssignment |
Visitor iterating over an expression and returning true if an assignment statement has been found.
|
DifferentFields |
This variable condition checks if given two terms s, t both terms have a different
unique symbol as top level operator
|
DifferentInstantiationCondition | |
DropEffectlessElementariesCondition | |
DropEffectlessStoresCondition | |
EnumConstantCondition |
ensures that the given instantiation for the schemavariable denotes a
constant of an enum type.
|
EnumTypeCondition |
This variable condition checks if a type is an enum type.
|
EqualUniqueCondition | |
FieldTypeToSortCondition |
Variable condition that enforces a given generic sort to be instantiated with
the type of a field constant.
|
FinalReferenceCondition |
ensures that the given instantiation for the schema variable denotes a
final field
|
FreeLabelInVariableCondition | |
IsThisReference |
This variable condition checks if a given type denotes an abstract class or
interface type.
|
JavaTypeToSortCondition |
Variable condition that enforces a given generic sort to be instantiated with
the sort of a program expression a schema variable is instantiated with
|
LocalVariableCondition |
Ensures the given ProgramElement denotes a local variable
|
MetaDisjointCondition | |
NewJumpLabelCondition |
This variable condition ensures that no other label of the
same name exists in the context program or one of the schemavariable
instantiations.
|
ObserverCondition | |
SimplifyIfThenElseUpdateCondition | |
SimplifyIfThenElseUpdateCondition.ElementaryUpdateWrapper | |
StaticFieldCondition |
This variable condition checks if the instantiation of a schemavariable (of
type Field) refers to a Java field declared as "static".
|
StaticMethodCondition |
ensures that the given instantiation for the schemavariable denotes
a static method.
|
StaticReferenceCondition |
ensures that the given instantiation for the schemavariable denotes a
static field
|
SubFormulaCondition |
This variable condition checks if an instantiation for a formula has sub formulas
which are formulas.
|
TermLabelCondition |
This variable condition checks if an instantiation for term labels contains a specific
term label.
|
TypeComparisonCondition |
General varcond for checking relationships between types of schema variables.
|
TypeCondition |
This variable condition checks if a schemavariable is instantiated
with a reference or primitive type
|
TypeResolver |
Several variable conditions deal with types.
|
TypeResolver.ContainerTypeResolver | |
TypeResolver.ElementTypeResolverForSV | |
TypeResolver.GenericSortResolver | |
TypeResolver.NonGenericSortResolver |
Enum | Description |
---|---|
TypeComparisonCondition.Mode |