Overview  Package   Class  Use  Deprecated  Index
Home >> All >> edu >> ucsb >> ccs >> jcontractor >> [ transformation overview ]	PREV CLASS  NEXT CLASS
SUMMARY:  JAVADOC |  SOURCE |  DOWNLOAD | NESTED | FIELD | CONSTR | METHOD	DETAIL: FIELD | CONSTR | METHOD

---

edu.ucsb.ccs.jcontractor.transformation
Class SaveOldStateTransformation  

java.lang.Object
  edu.ucsb.ccs.jcontractor.transformation.Transformation
      edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
          edu.ucsb.ccs.jcontractor.transformation.SaveOldStateTransformation

---

public class SaveOldStateTransformation

extends ContractTransformation

This transformation adds code to postconditions that refer to old to call to clone an object, and push the clone onto the stack of saved instances in jContractorRuntime.

Version:

$Id: SaveOldStateTransformation.java,v 1.14 2003/01/26 10:53:05 parkera Exp $

---

Field Summary
protected  int	oldIndex           The index of the OLD field in the current class.

 

Fields inherited from class edu.ucsb.ccs.jcontractor.transformation.Transformation

transformer

 

Constructor Summary

SaveOldStateTransformation()

 

Method Summary
boolean	acceptClass()           Determine if the current class should be processed.
protected  void	checkValidity(org.apache.bcel.classfile.Field oldField)           Determine if the OLD field is valid, and also if the current class is allowed to refer to OLD.
protected  org.apache.bcel.classfile.Field	findField(java.lang.String fieldname, org.apache.bcel.classfile.JavaClass javaclass)           Find a field by name.
protected  boolean	getField_Postcondition(int index, org.apache.bcel.classfile.Field RESULT)
protected  boolean	getField_Precondition(int index)
protected  org.apache.bcel.classfile.Field	getField(int index)           Find a field in the current class.
protected  boolean	handleInheritedOld_Precondition(org.apache.bcel.generic.MethodGen postcondition)
protected  void	handleInheritedOld(org.apache.bcel.generic.MethodGen postcondition)           Insert code to push a copy of the object onto the saved instances stack before calling a superclass postcondition that refers to OLD.
(package private)  boolean	inheritsOldReference(org.apache.bcel.classfile.JavaClass javaclass)           Determine if any superclass of a class in which postconditions are checked declares an OLD instance variable.
protected  boolean	inheritsOldReference(org.apache.bcel.generic.MethodGen postcondition)           Determine if a postcondition in any superclass contains a reference to OLD.
protected  boolean	insertSaveStateCall_Precondition(org.apache.bcel.generic.MethodGen mg)
protected  void	insertSaveStateCall(org.apache.bcel.generic.MethodGen mg)           Add jContractorRuntime.pushState(clone()) at the beginning of the postcondition that cooresponds to mg.
protected  boolean	refersToOld_Precondition(org.apache.bcel.generic.MethodGen postcondition)
protected  boolean	refersToOld(org.apache.bcel.generic.MethodGen postcondition)           Determine if a method refers to the OLD field.
void	transformClass()           Make sure that the class is valid, as regards it's OLD field.
void	transformMethod(org.apache.bcel.generic.MethodGen mg)           Add jContractorRuntime.pushState(clone()) at the beginning of the postcondition that cooresponds to mg.

 

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 edu.ucsb.ccs.jcontractor.transformation.Transformation

acceptClass_Precondition, getTransformer_Postcondition, getTransformer, setTransformer_Postcondition, setTransformer_Precondition, setTransformer, transform_Precondition, transform, transformClass_Precondition, transformMethod_Precondition

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

oldIndex

protected int oldIndex

The index of the OLD field in the current class. Set by acceptClass().

Constructor Detail

SaveOldStateTransformation

public SaveOldStateTransformation()

Method Detail

acceptClass

public boolean acceptClass()

Determine if the current class should be processed. Only classes that declare an "OLD" instance variable, or that inherit from a class that declares "OLD".

Specified by:

acceptClass in class Transformation

---

transformClass

public void transformClass()
                    throws AbortTransformationException

Make sure that the class is valid, as regards it's OLD field. If an OLD field is present, it must be private and of the same type as the class, and the class must implement Cloneable.

Specified by:

transformClass in class Transformation

---

transformMethod

public void transformMethod(org.apache.bcel.generic.MethodGen mg)

Add jContractorRuntime.pushState(clone()) at the beginning of the postcondition that cooresponds to mg. The call is added only if the postcondition refers to OLD.

Specified by:

transformMethod in class Transformation

---

insertSaveStateCall

protected void insertSaveStateCall(org.apache.bcel.generic.MethodGen mg)

Add jContractorRuntime.pushState(clone()) at the beginning of the postcondition that cooresponds to mg. The call is added only if the postcondition refers to OLD.

---

insertSaveStateCall_Precondition

protected boolean insertSaveStateCall_Precondition(org.apache.bcel.generic.MethodGen mg)

---

handleInheritedOld

protected void handleInheritedOld(org.apache.bcel.generic.MethodGen postcondition)

Insert code to push a copy of the object onto the saved instances stack before calling a superclass postcondition that refers to OLD. If the superclass contract refers to OLD, it will need to pop an object off of the stack.

---

handleInheritedOld_Precondition

protected boolean handleInheritedOld_Precondition(org.apache.bcel.generic.MethodGen postcondition)

---

checkValidity

protected void checkValidity(org.apache.bcel.classfile.Field oldField)
                      throws AbortTransformationException

Determine if the OLD field is valid, and also if the current class is allowed to refer to OLD. The field and class are considered valid if they meets the following constraints:

1. OLD may not be static. OLD refers to the old state of a specific instance, not the class as a whole.
2. OLD must be private. OLD is required to have the same type as the class that contains it, so it doesn't make sense for the field to inherit. If subclasses need access to OLD, they will declare their own copy, of the appropriate subclass type.
3. A class that contains OLD must implement Cloneable. The clone() method is used to save the state.

---

getField

protected org.apache.bcel.classfile.Field getField(int index)

Find a field in the current class.

---

getField_Precondition

protected boolean getField_Precondition(int index)

---

getField_Postcondition

protected boolean getField_Postcondition(int index,
                                         org.apache.bcel.classfile.Field RESULT)

---

findField

protected org.apache.bcel.classfile.Field findField(java.lang.String fieldname,
                                                    org.apache.bcel.classfile.JavaClass javaclass)

Find a field by name.

---

inheritsOldReference

protected boolean inheritsOldReference(org.apache.bcel.generic.MethodGen postcondition)

Determine if a postcondition in any superclass contains a reference to OLD.

---

inheritsOldReference

boolean inheritsOldReference(org.apache.bcel.classfile.JavaClass javaclass)

Determine if any superclass of a class in which postconditions are checked declares an OLD instance variable. If so, the "$saveState" method will need to call the superclass. Postconditions may be checked if the superclass is instrumented to at least the InstrumentationFilter.POST level.

---

refersToOld

protected boolean refersToOld(org.apache.bcel.generic.MethodGen postcondition)

Determine if a method refers to the OLD field.

---

refersToOld_Precondition

protected boolean refersToOld_Precondition(org.apache.bcel.generic.MethodGen postcondition)

---

Overview  Package   Class  Use  Deprecated  Index
Home >> All >> edu >> ucsb >> ccs >> jcontractor >> [ transformation overview ]	PREV CLASS  NEXT CLASS
SUMMARY:  JAVADOC |  SOURCE |  DOWNLOAD | NESTED | FIELD | CONSTR | METHOD	DETAIL: FIELD | CONSTR | METHOD

---