class InfFlowContractAppInOutRelationSnippet extends InfFlowInputOutputRelationSnippet
Constructor and Description |
---|
InfFlowContractAppInOutRelationSnippet() |
Modifier and Type | Method and Description |
---|---|
protected Term |
buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
InfFlowSpec infFlowSpec2,
BasicSnippetData d,
ProofObligationVars vs1,
ProofObligationVars vs2,
Term eqAtLocsTerm) |
produce
collectQuantifiableVariables, register, register, register, replace, replace, replace, replace, replace, replace, replaceQuantifiableVariables
protected Term buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1, ProofObligationVars vs2, Term eqAtLocsTerm)
buildObjectSensitivePostRelation
in class InfFlowInputOutputRelationSnippet