All Methods Static Methods Concrete Methods
Modifier and Type |
Method and Description |
(package private) static BasicPOSnippetFactory |
getBasicFactory(BasicSnippetData data,
ProofObligationVars poVars) |
static BasicPOSnippetFactory |
getBasicFactory(BlockContract contract,
ProofObligationVars vars,
ExecutionContext context,
Services services) |
static BasicPOSnippetFactory |
getBasicFactory(FunctionalOperationContract contract,
ProofObligationVars vars,
Services services) |
static BasicPOSnippetFactory |
getBasicFactory(InformationFlowContract contract,
ProofObligationVars vars,
Services services) |
static BasicPOSnippetFactory |
getBasicFactory(LoopSpecification invariant,
ProofObligationVars vars,
ExecutionContext context,
Term guardTerm,
Services services) |
(package private) static InfFlowPOSnippetFactory |
getInfFlowFactory(BasicSnippetData data,
ProofObligationVars vars1,
ProofObligationVars vars2) |
static InfFlowPOSnippetFactory |
getInfFlowFactory(BlockContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Services services) |
static InfFlowPOSnippetFactory |
getInfFlowFactory(InformationFlowContract contract,
ProofObligationVars vars1,
ProofObligationVars vars2,
Services services) |
static InfFlowPOSnippetFactory |
getInfFlowFactory(LoopSpecification invariant,
ProofObligationVars vars1,
ProofObligationVars vars2,
ExecutionContext context,
Term guardTerm,
Services services) |