class InfFlowPOSnippetFactoryImpl extends Object implements InfFlowPOSnippetFactory
InfFlowPOSnippetFactory.Snippet
Modifier and Type | Field and Description |
---|---|
(package private) BasicSnippetData |
data
Collection of data important for the production of snippets.
|
private EnumMap<InfFlowPOSnippetFactory.Snippet,InfFlowFactoryMethod> |
factoryMethods
Registered snippet factory methods.
|
(package private) ProofObligationVars |
poVars1
The first copy of the proof obligation variables.
|
(package private) ProofObligationVars |
poVars2
The second copy of the proof obligation variables.
|
Constructor and Description |
---|
InfFlowPOSnippetFactoryImpl(BasicSnippetData d,
ProofObligationVars vars1,
ProofObligationVars vars2) |
InfFlowPOSnippetFactoryImpl(BlockContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Services services) |
InfFlowPOSnippetFactoryImpl(InformationFlowContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
Services services) |
InfFlowPOSnippetFactoryImpl(LoopInvariant invariant,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Term guardTerm,
Services services) |
Modifier and Type | Method and Description |
---|---|
Term |
create(InfFlowPOSnippetFactory.Snippet snippet) |
private void |
registerFactoryMethods() |
final BasicSnippetData data
final ProofObligationVars poVars1
final ProofObligationVars poVars2
private final EnumMap<InfFlowPOSnippetFactory.Snippet,InfFlowFactoryMethod> factoryMethods
InfFlowPOSnippetFactoryImpl(InformationFlowContract contract, ProofObligationVars vars1, ProofObligationVars vars2, Services services)
InfFlowPOSnippetFactoryImpl(BlockContract contract, ProofObligationVars vars1, ProofObligationVars vars2, ExecutionContext context, Services services)
InfFlowPOSnippetFactoryImpl(LoopInvariant invariant, ProofObligationVars vars1, ProofObligationVars vars2, ExecutionContext context, Term guardTerm, Services services)
InfFlowPOSnippetFactoryImpl(BasicSnippetData d, ProofObligationVars vars1, ProofObligationVars vars2)
private void registerFactoryMethods()
public Term create(InfFlowPOSnippetFactory.Snippet snippet) throws UnsupportedOperationException
create
in interface InfFlowPOSnippetFactory
UnsupportedOperationException