class InfFlowPOSnippetFactoryImpl extends java.lang.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 java.util.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(LoopSpecification 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 java.util.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(LoopSpecification 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 java.lang.UnsupportedOperationException
create
in interface InfFlowPOSnippetFactory
java.lang.UnsupportedOperationException