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.
|
ContainsAssignmentCondition |
This variable condition can be used to check whether an assignment expression
occurs as a subexpression of a schemavariable instantiation,
|
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 | |
HasLoopInvariantCondition |
Checks whether a loop has an invariant (either normal or "free").
|
IsLabeledCondition |
Checks whether the given statement is labeled, i.e., actual a
LabeledStatement.
|
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
|
LoopFreeInvariantCondition |
Extracts the free loop invariants for the given loop term.
|
LoopInvariantCondition |
Extracts the loop invariants for a loop term (for all applicable heap
contexts).
|
LoopVariantCondition |
Extracts the variant for a loop term.
|
MayExpandMethodCondition |
ensures that the given instantiation for the schemavariable denotes
a method whose body may be expanded.
|
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 | |
SameObserverCondition |
A variable condition that is satisfied if the two arguments are
schema variables,
their instantiations are terms of observer functions,
with the same function,
which as exactly one heap argument
and has got a dependency contract
,
|
SimplifyIfThenElseUpdateCondition | |
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
|
StoreStmtInCondition |
Stores the given
Statement , after substitution of
SchemaVariable s, into the given ProgramSV for later use in
other conditions and transformers. |
StoreTermInCondition |
Stores the given
Term , after substitution of SchemaVariable s,
into the given SchemaVariable for later use in other conditions and
transformers. |
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 |
Copyright © 2003-2019 The KeY-Project.