java.lang.Object
edu.ucsb.ccs.jcontractor.transformation.Transformation
edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
- Direct Known Subclasses:
- AppendReturnTransformation, ContractCheckTransformation, ContractMethodTransformation, LoadContractClassTransformation, LockCloneTransformation, RemoveContractMethodsTransformation, ReplaceOldReferencesTransformation, ReplaceReturnInstructionsTransformation, SaveOldStateTransformation
- public abstract class ContractTransformation
- extends Transformation
Abstract super class for contract transformations. This class
defines methods that determine the names and signatures of contract
methods, and defines the rules about which methods may have which
sorts of contracts, and when contracts are checked. Logic about
the naming conventions used by jContractor, and about the rules of
when contracts can be checked is encapsulated in this class.
This class also defines several utility methods that are useful
for working with InstructionLists.
- Version:
- $Id: ContractTransformation.java,v 1.18 2002/07/14 07:47:00 parkera Exp $
|
Method Summary |
protected void |
append(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList il)
Append an instruction list to the body of a method. |
boolean |
canCheckEntryInvariant(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a invariant
check at its entry point. |
protected boolean |
canCheckExitInvariant_Precondition(org.apache.bcel.generic.MethodGen mg)
|
boolean |
canCheckExitInvariant(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a invariant
check at its exit point. |
boolean |
canCheckPostcondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a postcondition
check. |
boolean |
canCheckPrecondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method should have a precondition
check. |
protected boolean |
canHaveInheritedContract_Precondition(org.apache.bcel.generic.MethodGen mg)
|
protected boolean |
canHaveInheritedContract(org.apache.bcel.generic.MethodGen mg)
Determine if a method is allowed to have an inherited contract. |
protected boolean |
canHaveInvariant_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
|
boolean |
canHaveInvariant(org.apache.bcel.classfile.JavaClass javaclass)
Determine whether or not a class can have an invariant. |
protected boolean |
canHavePostcondition_Precondition(org.apache.bcel.generic.MethodGen mg)
|
boolean |
canHavePostcondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method can have a postcondition,
taking instrumentation level into account. |
protected boolean |
canHavePrecondition_Precondition(org.apache.bcel.generic.MethodGen mg)
|
boolean |
canHavePrecondition(org.apache.bcel.generic.MethodGen mg)
Determine whether or not this method can have a precondition,
taking instrumentation level into account. |
protected boolean |
canReferenceOld_Precondition(org.apache.bcel.generic.MethodGen m)
|
boolean |
canReferenceOld(org.apache.bcel.generic.MethodGen mg)
Determine if the postcondition for a non-contract method can
refer to OLD. |
protected boolean |
contractsCheckable_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
|
boolean |
contractsCheckable(org.apache.bcel.classfile.JavaClass javaclass)
Determine whether or not contracts should be checked on the
methods in a class. |
protected boolean |
createLoadArguments_Postcondition(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList RESULT)
|
protected boolean |
createLoadArguments_Precondition(org.apache.bcel.generic.MethodGen mg)
|
protected org.apache.bcel.generic.InstructionList |
createLoadArguments(org.apache.bcel.generic.MethodGen mg)
Build an instruction list to load a method's arguments onto the
stack. |
protected boolean |
entryInvariantCheckable_Precondition(org.apache.bcel.generic.MethodGen mg)
|
protected org.apache.bcel.classfile.Method |
findMethod(java.lang.String methodName,
java.lang.String methodSignature,
org.apache.bcel.classfile.JavaClass javaclass)
Find a method in a given class. |
protected org.apache.bcel.classfile.Method |
findMethod(java.lang.String methodName,
java.lang.String methodSignature,
org.apache.bcel.classfile.JavaClass javaclass,
org.apache.bcel.generic.ConstantPoolGen cpg)
Find a method in a given class, and add a reference to it to the
constant pool. |
protected int |
findMethodIndex(java.lang.String methodName,
java.lang.String methodSignature,
org.apache.bcel.classfile.JavaClass javaclass,
org.apache.bcel.generic.ConstantPoolGen cpg)
Find the index of a method. |
protected boolean |
getContractClassName_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String RESULT)
|
protected boolean |
getContractClassName_Postcondition(java.lang.String classname,
java.lang.String RESULT)
|
protected boolean |
getContractClassName_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
|
protected boolean |
getContractClassName_Precondition(java.lang.String classname)
|
java.lang.String |
getContractClassName(org.apache.bcel.classfile.JavaClass javaclass)
Get the name of the external contract class that cooresponds to
the given class. |
java.lang.String |
getContractClassName(java.lang.String classname)
Get the name of the external contract class that cooresponds to
the given class name. |
protected boolean |
getInvariantMethodName_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String RESULT)
|
protected boolean |
getInvariantMethodName_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
|
java.lang.String |
getInvariantMethodName(org.apache.bcel.classfile.JavaClass javaclass)
Get the name of the invariant method for a class. |
protected boolean |
getInvariantMethodSignature_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String RESULT)
|
protected boolean |
getInvariantMethodSignature_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
|
java.lang.String |
getInvariantMethodSignature(org.apache.bcel.classfile.JavaClass javaclass)
Get the signature of the invariant method for a class. |
protected boolean |
getPostconditionMethodName_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
|
protected boolean |
getPostconditionMethodName_Precondition(org.apache.bcel.generic.MethodGen m)
|
java.lang.String |
getPostconditionMethodName(org.apache.bcel.generic.MethodGen m)
Get the name of the postcondition method for a non-contract
method. |
protected boolean |
getPostconditionMethodSignature_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
|
protected boolean |
getPostconditionMethodSignature_Precondition(org.apache.bcel.generic.MethodGen m)
|
java.lang.String |
getPostconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
Get the signature of the method that defines the postcondition for
a non-contract method. |
protected boolean |
getPreconditionMethodName_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
|
protected boolean |
getPreconditionMethodName_Precondition(org.apache.bcel.generic.MethodGen m)
|
java.lang.String |
getPreconditionMethodName(org.apache.bcel.generic.MethodGen method)
Get the name of the precondition method for a non-contract
method. |
protected boolean |
getPreconditionMethodSignature_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
|
protected boolean |
getPreconditionMethodSignature_Precondition(org.apache.bcel.generic.MethodGen m)
|
java.lang.String |
getPreconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
Get the signature of the method that defines the precondition for
a non-contract method. |
protected boolean |
hasExternalContract(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String contractMethodName,
java.lang.String contractMethodSignature)
Determine if a class gets a particular contract from a separate
contract class. |
protected boolean |
hasInterfaceContract(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String contractMethodName,
java.lang.String contractMethodSignature)
Determine if a class gets a particular contract from an interface. |
protected boolean |
hasSuperClassContract(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String contractMethodName,
java.lang.String contractMethodSignature)
Determine if a class inherits a particular contract. |
protected boolean |
isContractClass_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
boolean RESULT)
|
protected boolean |
isContractClass_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
|
boolean |
isContractClass(org.apache.bcel.classfile.JavaClass javaclass)
Determine if a class defines contracts for another class. |
protected boolean |
isContractMethod_Postcondition(org.apache.bcel.generic.MethodGen m,
boolean RESULT)
|
protected boolean |
isContractMethod_Precondition(org.apache.bcel.generic.MethodGen m)
|
boolean |
isContractMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a contract (precondition,
postcondition, or invariant). |
protected boolean |
isInvariantMethod_Precondition(org.apache.bcel.generic.MethodGen m)
|
boolean |
isInvariantMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a class invariant. |
protected boolean |
isPostconditionMethod_Postcondition(org.apache.bcel.generic.MethodGen m,
boolean RESULT)
|
boolean |
isPostconditionMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a postcondition. |
protected boolean |
isPreconditionMethod_Precondition(org.apache.bcel.generic.MethodGen m)
|
boolean |
isPreconditionMethod(org.apache.bcel.generic.MethodGen m)
Determine if a method defines a precondition. |
protected boolean |
postconditionCheckable_Precondition(org.apache.bcel.generic.MethodGen mg)
|
protected boolean |
preconditionCheckable_Precondition(org.apache.bcel.generic.MethodGen mg)
|
protected void |
prepend(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList il)
Prepend an instruction list to the body of a method. |
protected boolean |
prependToConstructor_Precondition(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList il)
|
protected void |
prependToConstructor(org.apache.bcel.generic.MethodGen constructor,
org.apache.bcel.generic.InstructionList newInstructions)
Use prepend(MethodGen, InstructionList) instead. |
protected void |
replaceInstruction(org.apache.bcel.generic.InstructionList il,
org.apache.bcel.generic.InstructionHandle ih,
org.apache.bcel.generic.Instruction newInstruction)
Replace an instruction in an instruction list. |
protected void |
replaceInstruction(org.apache.bcel.generic.InstructionList il,
org.apache.bcel.generic.InstructionHandle ih,
org.apache.bcel.generic.InstructionList newInstructions)
Replace an instruction in an instruction list with an instruction
list. |
protected boolean |
replaceReturnInstructions_Precondition(org.apache.bcel.generic.InstructionList il)
|
protected void |
replaceReturnInstructions(org.apache.bcel.generic.InstructionList il)
Replace all the return instructions in an InstructionList with
code to jump to the end of the list. |
| Methods inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation |
acceptClass_Precondition, acceptClass, getTransformer_Postcondition, getTransformer, setTransformer_Postcondition, setTransformer_Precondition, setTransformer, transform_Precondition, transform, transformClass_Precondition, transformClass, transformMethod_Precondition, transformMethod |
| Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
ContractTransformation
public ContractTransformation()
hasSuperClassContract
protected boolean hasSuperClassContract(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String contractMethodName,
java.lang.String contractMethodSignature)
- Determine if a class inherits a particular contract. This method
checks only superclasses, not interfaces or external contract
classes.
hasExternalContract
protected boolean hasExternalContract(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String contractMethodName,
java.lang.String contractMethodSignature)
- Determine if a class gets a particular contract from a separate
contract class.
hasInterfaceContract
protected boolean hasInterfaceContract(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String contractMethodName,
java.lang.String contractMethodSignature)
- Determine if a class gets a particular contract from an interface.
canHavePrecondition
public boolean canHavePrecondition(org.apache.bcel.generic.MethodGen mg)
- Determine whether or not this method can have a precondition,
taking instrumentation level into account. All methods in
classes that are instrumented to the InstrumentationFilter.PRE
level or greater can have preconditions except:
- Contract methods.
- Native methods. (Not implemented yet.)
- Class initialization methods ().
- The
main (String args) method.
Note that their is a subtle difference between a method that can
have a precondition, and a method on which a precondition can be
checked. The difference arises in abstract methods, which can
have preconditions, but the contracts can only be checked in
implementation classes.
canCheckPrecondition(MethodGen) answers the
checkabilty question.
canHavePrecondition_Precondition
protected boolean canHavePrecondition_Precondition(org.apache.bcel.generic.MethodGen mg)
canHavePostcondition
public boolean canHavePostcondition(org.apache.bcel.generic.MethodGen mg)
- Determine whether or not this method can have a postcondition,
taking instrumentation level into account. All methods in
classes that are instrumented to the InstrumentationFilter.POST
level or greater can have postconditions except:
- Contract methods.
- Native methods. (Not implemented yet.)
- Class initialization methods ().
Note that their is a subtle difference between a method that can
have a postcondition, and a method on which a postcondition can be
checked. The difference arises in abstract methods, which can
have contracts, but the contracts can only be checked in
implementation classes.
canCheckPostcondition(MethodGen) answers the
checkabilty question.
canHavePostcondition_Precondition
protected boolean canHavePostcondition_Precondition(org.apache.bcel.generic.MethodGen mg)
canHaveInvariant
public boolean canHaveInvariant(org.apache.bcel.classfile.JavaClass javaclass)
- Determine whether or not a class can have an invariant. Only
classes that that are instrumented to the InstrumentationFilter.ALL
level can have invariant checks.
canHaveInvariant_Precondition
protected boolean canHaveInvariant_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
canHaveInheritedContract
protected boolean canHaveInheritedContract(org.apache.bcel.generic.MethodGen mg)
- Determine if a method is allowed to have an inherited contract.
Inherited contracts include those inherited from the super class,
and those inherited from interfaces. All methods are allowed to
inherit contracts, except for:
- Constructors.
- Private methods.
- Static methods.
canHaveInheritedContract_Precondition
protected boolean canHaveInheritedContract_Precondition(org.apache.bcel.generic.MethodGen mg)
contractsCheckable
public boolean contractsCheckable(org.apache.bcel.classfile.JavaClass javaclass)
- Determine whether or not contracts should be checked on the
methods in a class. This check is independent of the methods
defined in the class. Contracts are checkable in all classes
except:
- Interfaces (no code to execute, so nothing to check).
- Contract classes (classes with names ending in
"_CONTRACT"). Such classes define only contract methods.
- The edu.ucsb.ccs.jcontractor.jContractorRuntime
class. This class is used by jContractor at runtime to aid
in contract checking. Checking its contracts would result
in infinite recursion.
contractsCheckable_Precondition
protected boolean contractsCheckable_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
canCheckPrecondition
public boolean canCheckPrecondition(org.apache.bcel.generic.MethodGen mg)
- Determine whether or not this method should have a precondition
check. Preconditions may be checked for all methods except:
- Contract methods.
- Abstract methods.
- Native methods. (Not implemented yet.)
- Class initialization methods ().
Note that abstract methods may have preconditions, but the
conditions can only be checked when the method is implemented in
a subclass.
preconditionCheckable_Precondition
protected boolean preconditionCheckable_Precondition(org.apache.bcel.generic.MethodGen mg)
canCheckPostcondition
public boolean canCheckPostcondition(org.apache.bcel.generic.MethodGen mg)
- Determine whether or not this method should have a postcondition
check. Postconditions should be checked on all methods that have
postconditions, except:
- Contract methods.
- Abstract methods.
- Native methods. (Not implemented yet.)
- Class initialization methods (). (Not implemented
yet).
Note that abstract methods may have postconditions, but the
conditions can only be checked when the method is implemented in
a subclass.
postconditionCheckable_Precondition
protected boolean postconditionCheckable_Precondition(org.apache.bcel.generic.MethodGen mg)
canCheckEntryInvariant
public boolean canCheckEntryInvariant(org.apache.bcel.generic.MethodGen mg)
- Determine whether or not this method should have a invariant
check at its entry point. Entry invariants may be checked for
all methods except:
- Contract methods.
- Constructors.
- Non-public methods.
- Abstract methods.
- Static methods.
- Native methods. (Not implemented yet.)
- Class initialization methods ().
entryInvariantCheckable_Precondition
protected boolean entryInvariantCheckable_Precondition(org.apache.bcel.generic.MethodGen mg)
canCheckExitInvariant
public boolean canCheckExitInvariant(org.apache.bcel.generic.MethodGen mg)
- Determine whether or not this method should have a invariant
check at its exit point. Exit invariants may be checked for
all methods except:
- Contract methods.
- Non-public methods.
- Abstract methods.
- Static methods.
- Native methods. (Not implemented yet.)
- Class initialization methods ().
canCheckExitInvariant_Precondition
protected boolean canCheckExitInvariant_Precondition(org.apache.bcel.generic.MethodGen mg)
canReferenceOld
public boolean canReferenceOld(org.apache.bcel.generic.MethodGen mg)
- Determine if the postcondition for a non-contract method can
refer to OLD. All postconditions are allowed to refer to the old
state, except postconditions on:
- Static methods.
- Constructors.
- the
clone().*
* The state is saved by calling clone()
to make a copy of the object. Given this implementation,
clone() itself if unable to refer to the old state.
canReferenceOld_Precondition
protected boolean canReferenceOld_Precondition(org.apache.bcel.generic.MethodGen m)
isContractClass
public boolean isContractClass(org.apache.bcel.classfile.JavaClass javaclass)
- Determine if a class defines contracts for another class. Such
classes have names that end with "_CONTRACT" as in
"MyClass_CONTRACT".
isContractClass_Precondition
protected boolean isContractClass_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
isContractClass_Postcondition
protected boolean isContractClass_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
boolean RESULT)
isContractMethod
public boolean isContractMethod(org.apache.bcel.generic.MethodGen m)
- Determine if a method defines a contract (precondition,
postcondition, or invariant).
isContractMethod_Precondition
protected boolean isContractMethod_Precondition(org.apache.bcel.generic.MethodGen m)
isContractMethod_Postcondition
protected boolean isContractMethod_Postcondition(org.apache.bcel.generic.MethodGen m,
boolean RESULT)
isPreconditionMethod
public boolean isPreconditionMethod(org.apache.bcel.generic.MethodGen m)
- Determine if a method defines a precondition.
isPreconditionMethod_Precondition
protected boolean isPreconditionMethod_Precondition(org.apache.bcel.generic.MethodGen m)
isPostconditionMethod
public boolean isPostconditionMethod(org.apache.bcel.generic.MethodGen m)
- Determine if a method defines a postcondition.
isPostconditionMethod_Postcondition
protected boolean isPostconditionMethod_Postcondition(org.apache.bcel.generic.MethodGen m,
boolean RESULT)
isInvariantMethod
public boolean isInvariantMethod(org.apache.bcel.generic.MethodGen m)
- Determine if a method defines a class invariant.
isInvariantMethod_Precondition
protected boolean isInvariantMethod_Precondition(org.apache.bcel.generic.MethodGen m)
getPreconditionMethodName
public java.lang.String getPreconditionMethodName(org.apache.bcel.generic.MethodGen method)
- Get the name of the precondition method for a non-contract
method. The precondition method name is determined by appending
"_Precondition" to the method name. Constructors are a special
case, because they are all named "". The precondition for
a constructor is the class name with a "_Precondition" suffix.
Examples:
public class MyClass () {
MyClass () { ... }
boolean MyClass_Precondition () { ... }
void foo () { ... }
boolean foo_Precondition () { ... }
}
getPreconditionMethodName_Precondition
protected boolean getPreconditionMethodName_Precondition(org.apache.bcel.generic.MethodGen m)
getPreconditionMethodName_Postcondition
protected boolean getPreconditionMethodName_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
getPreconditionMethodSignature
public java.lang.String getPreconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
- Get the signature of the method that defines the precondition for
a non-contract method. The argument list is same as the
for the non-contract method, and the return type of the
postcondition is boolean.
Examples:
public class MyClass () {
MyClass () { ... }
boolean MyClass_Precondition () { ... }
MyClass (int x) { ... }
boolean MyClass_Precondition (int x) { ... }
void foo (Object o1, Object o2) { ... }
boolean foo_Precondition (Object o1, Object o2) { ... }
}
Signatures are returned in the format used by BCEL.
Examples:
getPreconditionMethodSignature("MyClass()") --> "()Z"
getPreconditionMethodSignature("MyClass(int)") --> "(I)Z"
getPreconditionMethodSignature("foo(Object, Object")) -->
"(Ljava/lang/Object;Ljava/lang/Object;)Z"
getPreconditionMethodSignature_Precondition
protected boolean getPreconditionMethodSignature_Precondition(org.apache.bcel.generic.MethodGen m)
getPreconditionMethodSignature_Postcondition
protected boolean getPreconditionMethodSignature_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
getPostconditionMethodName
public java.lang.String getPostconditionMethodName(org.apache.bcel.generic.MethodGen m)
- Get the name of the postcondition method for a non-contract
method. The postcondition method name is determined by appending
"_Postcondition" to the method name. Constructors are a special
case, because they are all named "". The postcondition for
a constructor is the class name with a "_Precondition" suffix.
Examples:
public class MyClass () {
MyClass () { ... }
boolean MyClass_Postcondition (Void RESULT) { ... }
int foo () { ... }
boolean foo_Postcondition (int RESULT) { ... }
}
getPostconditionMethodName_Precondition
protected boolean getPostconditionMethodName_Precondition(org.apache.bcel.generic.MethodGen m)
getPostconditionMethodName_Postcondition
protected boolean getPostconditionMethodName_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
getPostconditionMethodSignature
public java.lang.String getPostconditionMethodSignature(org.apache.bcel.generic.MethodGen m)
- Get the signature of the method that defines the postcondition for
a non-contract method. The argument list for the postcondition
method begins the same as the argument list for the non-contract
method, but adds an argument of the method's return type to the
end of the list. If the method returns void or is a constructor,
then the last argument should be of type java.lang.Void. The
return type of the postcondition is boolean.
Examples:
public class MyClass () {
MyClass () { ... }
boolean MyClass_Postcondition (Void RESULT) { ... }
MyClass (int x) { ... }
boolean MyClass_Postcondition (int x, Void RESULT) { ... }
int foo (Object o1, Object o2) { ... }
boolean foo_Precondition (Object o1, Object o2, int RESULT) { ... }
}
Signatures are returned in the format used by BCEL.
Examples:
getPostconditionMethodSignature("MyClass()") --> "(Ljava/lang/Void;)Z"
getPostconditionMethodSignature("MyClass(int)") --> "(ILjava/lang/Void;)Z"
getPostconditionMethodSignature("foo(Object, Object")) --gt;
"(Ljava/lang/Object;Ljava/lang/Object;I)Z"
getPostconditionMethodSignature_Precondition
protected boolean getPostconditionMethodSignature_Precondition(org.apache.bcel.generic.MethodGen m)
getPostconditionMethodSignature_Postcondition
protected boolean getPostconditionMethodSignature_Postcondition(org.apache.bcel.generic.MethodGen m,
java.lang.String RESULT)
getInvariantMethodName
public java.lang.String getInvariantMethodName(org.apache.bcel.classfile.JavaClass javaclass)
- Get the name of the invariant method for a class. The invariant
method is always called "_Invariant".
getInvariantMethodName_Precondition
protected boolean getInvariantMethodName_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
getInvariantMethodName_Postcondition
protected boolean getInvariantMethodName_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String RESULT)
getInvariantMethodSignature
public java.lang.String getInvariantMethodSignature(org.apache.bcel.classfile.JavaClass javaclass)
- Get the signature of the invariant method for a class. The
signature is that of a method that takes no arguments and returns
a boolean.
getInvariantMethodSignature_Precondition
protected boolean getInvariantMethodSignature_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
getInvariantMethodSignature_Postcondition
protected boolean getInvariantMethodSignature_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String RESULT)
getContractClassName
public java.lang.String getContractClassName(org.apache.bcel.classfile.JavaClass javaclass)
- Get the name of the external contract class that cooresponds to
the given class. The contract class has the same name as the
non-contract class, with a "_CONTRACT" suffix.
Examples:
class MyClass { ... }
class MyClass_CONTRACT { ... }
class Foo extends MyClass { ... }
class Foo_CONTRACT { ... }
getContractClassName_Precondition
protected boolean getContractClassName_Precondition(org.apache.bcel.classfile.JavaClass javaclass)
getContractClassName_Postcondition
protected boolean getContractClassName_Postcondition(org.apache.bcel.classfile.JavaClass javaclass,
java.lang.String RESULT)
getContractClassName
public java.lang.String getContractClassName(java.lang.String classname)
- Get the name of the external contract class that cooresponds to
the given class name. The contract class has the same name as
the non-contract class, with a "_CONTRACT" suffix.
Examples:
class MyClass { ... }
class MyClass_CONTRACT { ... }
class Foo extends MyClass { ... }
class Foo_CONTRACT { ... }
getContractClassName_Precondition
protected boolean getContractClassName_Precondition(java.lang.String classname)
getContractClassName_Postcondition
protected boolean getContractClassName_Postcondition(java.lang.String classname,
java.lang.String RESULT)
findMethod
protected org.apache.bcel.classfile.Method findMethod(java.lang.String methodName,
java.lang.String methodSignature,
org.apache.bcel.classfile.JavaClass javaclass)
- Find a method in a given class. This method will search through
all the methods in
javaclass, looking for one that
matches the name defined by methodName, and the
signature defined by methodSignature.
findMethod
protected org.apache.bcel.classfile.Method findMethod(java.lang.String methodName,
java.lang.String methodSignature,
org.apache.bcel.classfile.JavaClass javaclass,
org.apache.bcel.generic.ConstantPoolGen cpg)
- Find a method in a given class, and add a reference to it to the
constant pool. This method will search through all the methods
in
javaclass, looking for one that matches the name
defined by methodName, and the signature defined by
methodSignature.
findMethodIndex
protected int findMethodIndex(java.lang.String methodName,
java.lang.String methodSignature,
org.apache.bcel.classfile.JavaClass javaclass,
org.apache.bcel.generic.ConstantPoolGen cpg)
- Find the index of a method. This method will search through all
the methods in
javaclass, looking for one that
matches the name defined by methodName, and the
signature defined by methodSignature.
prepend
protected void prepend(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList il)
- Prepend an instruction list to the body of a method. If the
method is a constructor, the new instructions are inserted after
the call to the superclass constructor.
prependToConstructor
protected void prependToConstructor(org.apache.bcel.generic.MethodGen constructor,
org.apache.bcel.generic.InstructionList newInstructions)
- Use
prepend(MethodGen, InstructionList) instead. This
method is only called from that method.
Insert an instruction list into a constructor at the first
possible location (after the call to the superclass constructor).
No instructions are allowed before this.
prependToConstructor_Precondition
protected boolean prependToConstructor_Precondition(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList il)
append
protected void append(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList il)
- Append an instruction list to the body of a method.
replaceInstruction
protected void replaceInstruction(org.apache.bcel.generic.InstructionList il,
org.apache.bcel.generic.InstructionHandle ih,
org.apache.bcel.generic.Instruction newInstruction)
- Replace an instruction in an instruction list. All references to
the old instruction are retargeted to the new.
replaceInstruction
protected void replaceInstruction(org.apache.bcel.generic.InstructionList il,
org.apache.bcel.generic.InstructionHandle ih,
org.apache.bcel.generic.InstructionList newInstructions)
- Replace an instruction in an instruction list with an instruction
list. All references to the old instruction are retargeted to
the start of the new list.
replaceReturnInstructions
protected void replaceReturnInstructions(org.apache.bcel.generic.InstructionList il)
- Replace all the return instructions in an InstructionList with
code to jump to the end of the list.
Here's an example of some bytecode processed by this
method:
Before: After:
----------- --------------
0: iload_0 0: iload_0
1: ifeq #4 1: ifeq #4
2: iconst_0 2: iconst_0
3: return 3: goto #6
4: iconst_1 4: iconst_1
5: return 5: goto #6
6: nop
replaceReturnInstructions_Precondition
protected boolean replaceReturnInstructions_Precondition(org.apache.bcel.generic.InstructionList il)
createLoadArguments
protected org.apache.bcel.generic.InstructionList createLoadArguments(org.apache.bcel.generic.MethodGen mg)
- Build an instruction list to load a method's arguments onto the
stack. This needs to be done before calling preconditions and
postconditions.
createLoadArguments_Precondition
protected boolean createLoadArguments_Precondition(org.apache.bcel.generic.MethodGen mg)
createLoadArguments_Postcondition
protected boolean createLoadArguments_Postcondition(org.apache.bcel.generic.MethodGen mg,
org.apache.bcel.generic.InstructionList RESULT)
JAVADOC | 
SOURCE | 
DOWNLOAD | NESTED | FIELD | CONSTR | METHOD