See: Description
| Interface | Description |
|---|---|
| Sort |
| Class | Description |
|---|---|
| AbstractSort |
Abstract base class for implementations of the Sort interface.
|
| ArraySort |
The objects of this class represent array sorts (in the sense of *Java*
arrays).
|
| ArraySort.SortKey | |
| GenericSort |
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
| NullSort |
There is one instance of this class per proof, representing the sort "Null".
|
| ProgramSVSort |
Special "sorts" used for schema variables matching program constructs
(class ProgramSV).
|
| ProgramSVSort.ArrayInitializerSVSort |
This sort represents a type of program schema variables that
match only on Array Initializers.
|
| ProgramSVSort.ArrayLengthSort | |
| ProgramSVSort.ArrayPostDeclarationSort | |
| ProgramSVSort.CatchSort |
This sort represents a type of program schema variables that
match only on catch branches of try-catch-finally blocks
|
| ProgramSVSort.ConstantProgramVariableSort | |
| ProgramSVSort.ExecutionContextSort | |
| ProgramSVSort.ExpressionSort |
This sort represents a type of program schema variables that match on
all expressions only.
|
| ProgramSVSort.ExpressionSpecialPrimitiveTypeSort |
This sort represents a type of program schema variables that match
on simple expressions which have a special primitive type.
|
| ProgramSVSort.ForLoopSort | |
| ProgramSVSort.ForUpdatesSort | |
| ProgramSVSort.GuardSort | |
| ProgramSVSort.LabelSort |
This sort represents a type of program schema variables that match
on labels.
|
| ProgramSVSort.LeftHandSideSort |
This sort represents a type of program schema variables that match
only on program variables or static field references with
a prefix that consists of a program variable followed by a
sequence of attribute accesses or of a type reference followed by
a sequence of attribute accesses
|
| ProgramSVSort.LocalVariableSort | |
| ProgramSVSort.LoopInitSort | |
| ProgramSVSort.MetaClassReferenceSort |
This sort represents a type of program schema variables that
match only on meta class references.
|
| ProgramSVSort.MethodBodySort |
This sort represents a type of program schema variables that
match only on method body statements
|
| ProgramSVSort.MethodNameSort |
This sort represents a type of program schema variables that match
on names of method references, i.e. the "m" of o.m(p1,pn).
|
| ProgramSVSort.MultipleVariableDeclarationSort | |
| ProgramSVSort.NewArraySVSort |
This sort represents a type of program schema variables that match
only on Array Creation Expressions, new A[]
|
| ProgramSVSort.NonModelMethodBodySort |
This sort represents a type of program schema variables that
match only on method body statements for nonmodel methods for which
an implementation is present.
|
| ProgramSVSort.NonSimpleExpressionNoClassReferenceSort | |
| ProgramSVSort.NonSimpleExpressionSort |
This sort represents a type of program schema variables that match
only on all expressions which are not matched by simple expression
SVs.
|
| ProgramSVSort.NonSimpleMethodReferenceSort |
This sort represents a type of program schema variables that
match on a method call with SIMPLE PREFIX and AT LEAST a
NONSIMPLE expression in the ARGUMENTS.
|
| ProgramSVSort.NonSimpleNewSVSort |
This sort represents a type of program schema variables that match
only on Class Instance Creation Expressions, new C(), where at
least one argument is a non-simple expression
|
| ProgramSVSort.NonStringLiteralSort |
This sort represents a type of program schema variables that match
only on non-string literals
|
| ProgramSVSort.ProgramMethodSort |
This sort represents a type of program schema variables that
match only on program methods
|
| ProgramSVSort.ProgramVariableSort |
This sort represents a type of program schema variables that match
only on program variables or static field references with
a prefix that consists of a program variable followed by a
sequence of attribute accesses or of a type reference followed by
a sequence of attribute accesses.
|
| ProgramSVSort.SimpleExpressionNonStringObjectSort | |
| ProgramSVSort.SimpleExpressionSort |
This sort represents a type of program schema variables that match
only on program variables or static field references with
a prefix that consists of a program variable followed by a
sequence of attribute accesses or of a type reference followed by
a sequence of attribute accesses (negated) literal
expressions or instanceof expressions v instanceof T with an
expression v that matches on a program variable SV
|
| ProgramSVSort.SimpleExpressionSpecialPrimitiveTypeSort |
This sort represents a type of program schema variables that match
on simple expressions which have a special primitive type.
|
| ProgramSVSort.SimpleExpressionStringSort |
This sort represents a type of program schema variables that match
on string literals and string variables.
|
| ProgramSVSort.SimpleNewSVSort |
This sort represents a type of program schema variables that match
only on Class Instance Creation Expressions, new C(), where all
arguments are simple expressions.
|
| ProgramSVSort.SpecialConstructorReferenceSort |
This sort represents a type of program schema variables that
match only on Special Constructor References.
|
| ProgramSVSort.StatementSort |
This sort represents a type of program schema variables that
match only on statements
|
| ProgramSVSort.StaticVariableSort | |
| ProgramSVSort.StringLiteralSort |
This sort represents a type of program schema variables that match
only string literals, e.g.
|
| ProgramSVSort.SwitchSVSort | |
| ProgramSVSort.TypeReferenceNotPrimitiveSort |
This sort represents a type of program schema variables that
match anything except byte, char, short, int, and long.
|
| ProgramSVSort.TypeReferenceSort |
This sort represents a type of program schema variables that
match only on type references.
|
| ProxySort | |
| SortImpl |
Standard implementation of the Sort interface.
|
| Exception | Description |
|---|---|
| GenericSupersortException |
this exception is thrown if a generic sort has been declared with
an illegal supersort
|