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

Class BasicBlockExecutionWithPreconditionSnippet

java.lang.Object

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

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

All Implemented Interfaces:

FactoryMethod

class BasicBlockExecutionWithPreconditionSnippet
extends ReplaceAndRegisterMethod
implements FactoryMethod

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
BasicBlockExecutionWithPreconditionSnippet()

Method Summary

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

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

BasicBlockExecutionWithPreconditionSnippet

BasicBlockExecutionWithPreconditionSnippet()

Method Detail

produce

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

Specified by:

produce in interface FactoryMethod

Throws:

java.lang.UnsupportedOperationException