public class PostWork extends ProgramTransformer
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
POST_WORK |
private boolean |
schema
Whether this transformer is used schematically (i.e., in taclets).
|
Constructor and Description |
---|
PostWork(ProgramVariable pv)
Used to create this Java statement programmatically.
|
PostWork(SchemaVariable newObjectSV) |
Modifier and Type | Method and Description |
---|---|
ProgramElement[] |
transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program
transformation
|
body, getChildAt, getChildCount, getDimensions, getExpressionAt, getExpressionCount, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getName, getPackageReference, getProgramElementName, getReferencePrefix, getStatementAt, getStatementCount, getTypeReferenceAt, getTypeReferenceCount, name, neededInstantiations, needs, prettyPrint, setReferencePrefix, toString, visit
compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren
getComments, hashCode, prettyPrintMain, reuseSignature
getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
private static final java.lang.String POST_WORK
private final boolean schema
public PostWork(SchemaVariable newObjectSV)
public PostWork(ProgramVariable pv)
pv
- The ProgramVariable
public ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
transform
in class ProgramTransformer
pe
- the ProgramElement on which the execution is performedservices
- the Services with all necessary information
about the java programssvInst
- the instantiations of the schemavariables