class InfFlowInputOutputRelationSnippet extends ReplaceAndRegisterMethod implements InfFlowFactoryMethod
Modifier and Type | Class and Description |
---|---|
private static class |
InfFlowInputOutputRelationSnippet.SearchVisitor |
Constructor and Description |
---|
InfFlowInputOutputRelationSnippet() |
Modifier and Type | Method and Description |
---|---|
private Term |
buildInputOutputRelation(BasicSnippetData d,
ProofObligationVars vs1,
ProofObligationVars vs2,
InfFlowSpec infFlowSpecAtPre1,
InfFlowSpec infFlowSpecAtPre2,
InfFlowSpec infFlowSpecAtPost1,
InfFlowSpec infFlowSpecAtPost2) |
private Term |
buildInputRelation(BasicSnippetData d,
ProofObligationVars vs1,
ProofObligationVars vs2,
InfFlowSpec infFlowSpec1,
InfFlowSpec infFlowSpec2) |
protected Term |
buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1,
InfFlowSpec infFlowSpec2,
BasicSnippetData d,
ProofObligationVars vs1,
ProofObligationVars vs2,
Term eqAtLocsTerm) |
private Term |
buildOutputRelation(BasicSnippetData d,
ProofObligationVars vs1,
ProofObligationVars vs2,
InfFlowSpec infFlowSpec1,
InfFlowSpec infFlowSpec2) |
Term |
produce(BasicSnippetData d,
ProofObligationVars poVars1,
ProofObligationVars poVars2) |
collectQuantifiableVariables, register, register, register, replace, replace, replace, replace, replace, replace, replaceQuantifiableVariables
public Term produce(BasicSnippetData d, ProofObligationVars poVars1, ProofObligationVars poVars2) throws java.lang.UnsupportedOperationException
produce
in interface InfFlowFactoryMethod
java.lang.UnsupportedOperationException
private Term buildInputOutputRelation(BasicSnippetData d, ProofObligationVars vs1, ProofObligationVars vs2, InfFlowSpec infFlowSpecAtPre1, InfFlowSpec infFlowSpecAtPre2, InfFlowSpec infFlowSpecAtPost1, InfFlowSpec infFlowSpecAtPost2)
private Term buildInputRelation(BasicSnippetData d, ProofObligationVars vs1, ProofObligationVars vs2, InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2)
private Term buildOutputRelation(BasicSnippetData d, ProofObligationVars vs1, ProofObligationVars vs2, InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2)
protected Term buildObjectSensitivePostRelation(InfFlowSpec infFlowSpec1, InfFlowSpec infFlowSpec2, BasicSnippetData d, ProofObligationVars vs1, ProofObligationVars vs2, Term eqAtLocsTerm)