de.uka.ilkd.key.informationflow.po.snippet

Class InfFlowContractAppSnippet

java.lang.Object

de.uka.ilkd.key.informationflow.po.snippet.ReplaceAndRegisterMethod

de.uka.ilkd.key.informationflow.po.snippet.InfFlowContractAppSnippet

All Implemented Interfaces:

InfFlowFactoryMethod

class InfFlowContractAppSnippet
extends ReplaceAndRegisterMethod
implements InfFlowFactoryMethod

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
InfFlowContractAppSnippet()

Method Summary

Modifier and Type	Method and Description
Term	produce(BasicSnippetData d, ProofObligationVars poVars1, ProofObligationVars poVars2)

Methods inherited from class de.uka.ilkd.key.informationflow.po.snippet.ReplaceAndRegisterMethod

collectQuantifiableVariables, register, register, register, replace, replace, replace, replace, replace, replace, replaceQuantifiableVariables

Methods inherited from class java.lang.Object

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

Constructor Detail

InfFlowContractAppSnippet

InfFlowContractAppSnippet()

Method Detail

produce

public Term produce(BasicSnippetData d,
                    ProofObligationVars poVars1,
                    ProofObligationVars poVars2)
             throws java.lang.UnsupportedOperationException

Specified by:

produce in interface InfFlowFactoryMethod

Throws:

java.lang.UnsupportedOperationException