java.lang.Object
edu.ucsb.ccs.jcontractor.transformation.Transformation
edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
edu.ucsb.ccs.jcontractor.transformation.AppendReturnTransformation
- public class AppendReturnTransformation
- extends ContractTransformation
A transformation to append code to load the method's result from a
local variable, and return. This must be done after processing
with ReplaceReturnInstructionTransformation. This transformation
requires that ReplaceReturnInstructionTransformation has saved the
method's return value to a local variable, and placed the index of
this variable into the shared data table.
This transformation is only required where
ReplaceReturnInstructionTransformation is required, so it
transforms only methods for which either the postcondition or
exit invariant is checkable.
Before: After:
----------- --------------
0: iload_0 0: iload_0
1: ifeq 1: ifeq
2: iconst_0 2: iconst_0
3: goto #6 3: goto #6
4: iconst_1 4: iconst_1
5: goto #6 5: goto #6
6: nop 6: nop
7: [check exit condition] 7: [check exit condition]
8: iload_2
9: ireturn
- Version:
- $Id: AppendReturnTransformation.java,v 1.7 2002/05/12 00:09:16 parkera Exp $
| Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.ContractTransformation |
append, canCheckEntryInvariant, canCheckExitInvariant_Precondition, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInheritedContract_Precondition, canHaveInheritedContract, canHaveInvariant_Precondition, canHaveInvariant, canHavePostcondition_Precondition, canHavePostcondition, canHavePrecondition_Precondition, canHavePrecondition, canReferenceOld_Precondition, canReferenceOld, contractsCheckable_Precondition, contractsCheckable, createLoadArguments_Postcondition, createLoadArguments_Precondition, createLoadArguments, entryInvariantCheckable_Precondition, findMethod, findMethod, findMethodIndex, getContractClassName_Postcondition, getContractClassName_Postcondition, getContractClassName_Precondition, getContractClassName_Precondition, getContractClassName, getContractClassName, getInvariantMethodName_Postcondition, getInvariantMethodName_Precondition, getInvariantMethodName, getInvariantMethodSignature_Postcondition, getInvariantMethodSignature_Precondition, getInvariantMethodSignature, getPostconditionMethodName_Postcondition, getPostconditionMethodName_Precondition, getPostconditionMethodName, getPostconditionMethodSignature_Postcondition, getPostconditionMethodSignature_Precondition, getPostconditionMethodSignature, getPreconditionMethodName_Postcondition, getPreconditionMethodName_Precondition, getPreconditionMethodName, getPreconditionMethodSignature_Postcondition, getPreconditionMethodSignature_Precondition, getPreconditionMethodSignature, hasExternalContract, hasInterfaceContract, hasSuperClassContract, isContractClass_Postcondition, isContractClass_Precondition, isContractClass, isContractMethod_Postcondition, isContractMethod_Precondition, isContractMethod, isInvariantMethod_Precondition, isInvariantMethod, isPostconditionMethod_Postcondition, isPostconditionMethod, isPreconditionMethod_Precondition, isPreconditionMethod, postconditionCheckable_Precondition, preconditionCheckable_Precondition, prepend, prependToConstructor_Precondition, prependToConstructor, replaceInstruction, replaceInstruction, replaceReturnInstructions_Precondition, replaceReturnInstructions |
| Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
AppendReturnTransformation
public AppendReturnTransformation()
acceptClass
public boolean acceptClass()
- Determine if the current class should be processed. All classes
in which contracts are checkable are processed.
- Specified by:
acceptClass in class Transformation
transformMethod
public void transformMethod(org.apache.bcel.generic.MethodGen mg)
- Append code to load the method's return value from a local
variable and return. This transformation is only required where
ReplaceReturnInstructionTransformation is required, so it
transforms only methods for which either the postcondition or
exit invariant is checkable. The index of the local variable
that holds the return value is saved in the shared data table as
ReplaceReturnInstructionTransformation
.SHARED_INFO_RESULT_INDEX_KEY + mg.getName()
+ mg.getSignature().
- Specified by:
transformMethod in class Transformation
transformClass
public void transformClass()
- Does nothing. This transformation operates only on methods.
- Specified by:
transformClass in class Transformation
JAVADOC | 
SOURCE | 
DOWNLOAD | NESTED | FIELD | CONSTR | METHOD