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