Taclet
s.See: Description
Class | Description |
---|---|
AddCast | |
ArrayBaseInstanceOf |
Creates an Type::instance(..) term for the component type of the
array.
|
ArrayLength | |
ArrayPostDecl |
Replaces a local variable declaration
#t #v[]; with
#t[] #v; |
ConstantValue |
Replace a program variable that is a compile-time constant with the
value of the initializer
|
ConstructorCall |
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
CreateBeforeLoopUpdate |
Initializes the "before loop" update needed for the assignable clause.
|
CreateFrameCond |
Creates the frame condition (aka "assignable clause") for the given loop.
|
CreateHeapAnonUpdate |
Creates the anonymizing update for the heap.
|
CreateLocalAnonUpdate |
Expects a loop body and creates the anonymizing update
out_1:=anon_1||...||out_n:=anon_n , where anon_1, ..., anon_n are
the written variables in the loop body visible to the outside. |
CreateObject |
If an allocation expression
new Class(...) occurs, a new object
has to be created, in KeY this is quite similar to take it out of a list of
objects and setting the implicit flag <created> to
true as well as setting all fields of the object to their
default values. |
CreateWellformedCond |
Creates the wellformedness condition for the given anonymizing heap terms if
they apply for the current profile and modality type.
|
DoBreak |
This class performs a labeled break.
|
EnhancedForElimination |
This class defines a meta operator to resolve an enhanced for loop - by transformation to a
"normal" loop.
|
EnumConstantValue |
resolve a program variable to an integer literal.
|
EvaluateArgs |
TODO
|
ExpandMethodBody |
Replaces the MethodBodyStatement shortcut with the full body, performs prefix
adjustments in the body (execution context).
|
ExpandQueriesMetaConstruct |
Uses the class
QueryExpand in order to insert query expansions in the term that the
meta construct is applied on. |
ForInitUnfoldTransformer |
Pulls the initializor out of a for-loop.
|
ForToWhile |
converts a for-loop to a while loop.
|
ForToWhileTransformation |
This transformation is used to transform a for-loop into a while-loop.
|
InitArray |
Split an array creation expression with explicit array initializer,
creating a creation expression with dimension expression and a list
of assignments (-> Java language specification, 15.10)
|
InitArrayCreation |
Split an array creation expression with explicit array initializer, creating
a creation expression with dimension expression and a list of assignments (->
Java language specification, 15.10)
This meta construct delivers the creation expression
|
IntroAtPreDefsOp | |
IsStatic |
Creates a true or false literal if the given program element is or is not a
static variable reference.
|
MemberPVToField | |
MethodCall |
Symbolically executes a method invocation
|
MultipleVarDecl |
Replaces a declaration of multiple variables by two variable declarations
where the first one declares a single variable and the second one the
remaining variables.
|
ObserverEqualityMetaConstruct |
This meta contruct allows one to prove equality (equivalence) of two
observer terms if they belong to the same observer function symbol.
|
PostWork |
creates an assignment instantiationOf(#newObjectsV).
|
ProgramTransformer |
ProgramTransformers are used to describe schematic transformations
that cannot be expressed by the taclet language itself.
|
ReattachLoopInvariant |
Construct for re-attaching a loop invariant that otherwise would get lost
after a transformation, for instance, the loop scope-based unwinding rule.
|
ReplaceWhileLoop |
This visitor is used to identify and replace the while loop
in invariant rule.
|
SpecialConstructorCall |
The constructor call meta construct is used to handle a allocation expression
like
new Class(...) . |
StaticInitialisation | |
SwitchToIf |
This class is used to perform program transformations needed for the symbolic
execution of a switch-case statement.
|
TypeOf | |
Unpack | |
UnwindLoop |
This class is used to perform program transformations needed for the symbolic
execution of a loop.
|
WhileInvariantTransformation |
Walks through a java AST in depth-left-fist-order.
|
WhileInvariantTransformer | |
WhileLoopTransformation |
Walks through a java AST in depth-left-fist-order.
|
Taclet
s.
Last modified: Tue Nov 26 08:54:55 MET 2002
Copyright © 2003-2019 The KeY-Project.