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 $

Author:

Parker Abercrombie

See Also:

ReplaceOldReferencesTransformation

Constructor Summary

SaveOldStateTransformation()

Method Summary

boolean	acceptClass() Determine if the current class should be processed.
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

canCheckEntryInvariant, canCheckExitInvariant, canCheckPostcondition, canCheckPrecondition, canHaveInvariant, canHavePostcondition, canHavePrecondition, canReferenceOld, contractsCheckable, getContractClassName, getContractClassName, getInvariantMethodName, getInvariantMethodSignature, getPostconditionMethodName, getPostconditionMethodSignature, getPreconditionMethodName, getPreconditionMethodSignature, isContractClass, isContractMethod, isInvariantMethod, isPostconditionMethod, isPreconditionMethod

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

getTransformer, setTransformer, transform

Methods inherited from class java.lang.Object

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

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".

Overrides:

acceptClass in class Transformation

Returns:

true if the class should be processed, based on the criteria above.

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.

Overrides:

transformClass in class Transformation

Throws:

AbortTransformationException - if the signature of the OLD field is invalid, or if the class does not implement Cloneable, a requirement for classes that use OLD.

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.

Overrides:

transformMethod in class Transformation

Parameters:

mg - a method to transform.