edu.ucsb.ccs.jcontractor.transformation
Class ReplaceOldReferencesTransformation

java.lang.Object
  |
  +--edu.ucsb.ccs.jcontractor.transformation.Transformation
        |
        +--edu.ucsb.ccs.jcontractor.transformation.ContractTransformation
              |
              +--edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

public class ReplaceOldReferencesTransformation

extends ContractTransformation

Transformation to replace references to OLD in postconditions. The old state is saved on a stack in jContractorRuntime, so the postcondition needs to pop the saved state, and store it to a local variable (storing to the OLD instance variable wouldn't be thread safe). Each reference to the OLD instance variable needs to be changed to a reference to the local variable.

Version:

$Id: ReplaceOldReferencesTransformation.java,v 1.4 2002/05/12 00:09:17 parkera Exp $

Author:

Parker Abercrombie

See Also:

SaveOldStateTransformation

Constructor Summary

ReplaceOldReferencesTransformation()

Method Summary

boolean	acceptClass() Determine if the current class should be processed.
void	transformClass() Does nothing.
void	transformMethod(org.apache.bcel.generic.MethodGen mg) Replace references to OLD in a postcondition method.

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

ReplaceOldReferencesTransformation

public ReplaceOldReferencesTransformation()

Method Detail

acceptClass

public boolean acceptClass()

Determine if the current class should be processed. All classes in which contracts can be checked, and that declare an OLD intance variable, are processed.

Overrides:

acceptClass in class Transformation

Returns:

true if contracts are checkable in the current class.

transformMethod

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

Replace references to OLD in a postcondition method.

Overrides:

transformMethod in class Transformation

Parameters:

mg - a method to transform. No action is taken if `mg' is not a postcondition method.

transformClass

public void transformClass()

Does nothing. This transformation operates only on methods.

Overrides:

transformClass in class Transformation