public abstract class AbstractInfFlowPO extends AbstractOperationPO implements InfFlowPO
AbstractPO
and AbstractOperationPO
.IPersistablePO.LoadedPOContainer
proofConfig
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets, tb
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
AbstractInfFlowPO(InitConfig initConfig,
java.lang.String name) |
Modifier and Type | Method and Description |
---|---|
Proof |
createProof(java.lang.String proofName,
Term poTerm,
InitConfig proofConfig)
Creates a Proof (helper for getPO()).
|
InfFlowProof |
createProofObject(java.lang.String proofName,
java.lang.String proofHeader,
Term poTerm,
InitConfig proofConfig) |
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFrameClause, buildFreePre, buildJavaBlock, buildOperationBlocks, buildPOName, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, fillSaveProperties, generateMbyAtPreDef, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCalleeKeYJavaType, getCreatedInitConfigForSingleProof, getGlobalDefs, getInitialTaclets, getPost, getPre, getProgramMethod, getSavedHeap, getTerminationMarker, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, isTransactionApplicable, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit, readProblem
assignPOTerms, collectClassAxioms, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getContainerType, getName, getPO, implies, name, register, register, register, selectClassAxioms
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
addIFSymbol, addIFSymbol, addLabeledIFSymbol, addLabeledIFSymbol, getIFSymbols, getLeafIFVars, unionLabeledIFSymbols
getContainerType, getPO, implies, name, readProblem
public AbstractInfFlowPO(InitConfig initConfig, java.lang.String name)
public Proof createProof(java.lang.String proofName, Term poTerm, InitConfig proofConfig)
AbstractPO
createProof
in class AbstractPO
proofName
- name of the proofpoTerm
- term of the proof obligationproofConfig
- the proof configurationpublic InfFlowProof createProofObject(java.lang.String proofName, java.lang.String proofHeader, Term poTerm, InitConfig proofConfig)
createProofObject
in class AbstractPO