Taclets.
See: Description
| Class | Description | 
|---|---|
| AddCast | |
| ArrayBaseInstanceOf | 
 Creates an Type::instance(..) 
 | 
| ArrayLength | |
| ArrayPostDecl | 
 Replaces a local variable declaration  
 #t #v[];  with
 #t[] #v; | 
| BreakToBeReplaced | |
| 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(...) | 
| CreateObject | 
 If an allocation expression  
new Class(...) | 
| 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. 
 | 
| PostWork | 
 creates an assignment instantiationOf(#newObjectsV). 
 | 
| ProgramTransformer | 
 ProgramTransformers are used to describe schematic transformations 
 that cannot be expressed by the taclet language itself. 
 | 
| 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. 
 | 
Taclets.
Last modified: Tue Nov 26 08:54:55 MET 2002