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

Class InfFlowContractAppInOutRelationSnippet

java.lang.Object

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

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

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

All Implemented Interfaces:

InfFlowFactoryMethod

class InfFlowContractAppInOutRelationSnippet
extends InfFlowInputOutputRelationSnippet

Author:

christoph

Constructor Summary

Constructors

Constructor and Description
InfFlowContractAppInOutRelationSnippet()

Method Summary

Modifier and Type	Method and Description
protected Term	buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1, ProofObligationVars vs2, Term eqAtLocsTerm)

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

produce

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

InfFlowContractAppInOutRelationSnippet

InfFlowContractAppInOutRelationSnippet()

Method Detail

buildObjectSensitivePostRelation

protected Term buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
                                                InfFlowSpec infFlowSpec2,
                                                BasicSnippetData d,
                                                ProofObligationVars vs1,
                                                ProofObligationVars vs2,
                                                Term eqAtLocsTerm)

Overrides:

buildObjectSensitivePostRelation in class InfFlowInputOutputRelationSnippet