ReplaceOldReferencesTransformation

Overview

Package

Class

Use

Deprecated

Index

Home >> All >> edu >> ucsb >> ccs >> jcontractor >> [ transformation overview ]

PREV CLASS NEXT CLASS

SUMMARY:

JAVADOC |

Sourc code of edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

SOURCE |

Download edu.ucsb.ccs.jcontractor.transformation.ReplaceOldReferencesTransformation

DOWNLOAD | NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

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 $

Field Summary

protected org.apache.bcel.generic.ObjectType currentType
          The type of instances of the current class.

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

ReplaceOldReferencesTransformation()


Method Summary

boolean acceptClass()
          Determine if the current class should be processed.

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


protected void processPostcondition(org.apache.bcel.generic.MethodGen postcondition)
          Transform a postcondition to check old references correctly.

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()
          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

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

currentType

protected org.apache.bcel.generic.ObjectType currentType

The type of instances of the current class.

oldIndex

protected int oldIndex

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

Constructor Detail