public abstract class AbstractInfFlowPO extends AbstractOperationPO implements InfFlowPO
AbstractPO
and AbstractOperationPO
.IPersistablePO.LoadedPOContainer
proofConfig, tb
environmentConfig, environmentServices, heapLDT, javaInfo, name, poNames, poTerms, specRepos, taclets
PROPERTY_ADD_SYMBOLIC_EXECUTION_LABEL, PROPERTY_ADD_UNINTERPRETED_PREDICATE, PROPERTY_CLASS, PROPERTY_FILENAME, PROPERTY_NAME
Constructor and Description |
---|
AbstractInfFlowPO(InitConfig initConfig,
String name) |
Modifier and Type | Method and Description |
---|---|
Proof |
createProof(String proofName,
Term poTerm,
InitConfig proofConfig)
Creates a Proof (helper for getPO()).
|
InfFlowProof |
createProofObject(String proofName,
String proofHeader,
Term poTerm,
InitConfig proofConfig) |
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFrameClause, buildFreePre, buildJavaBlock, buildOperationBlocks, buildPOName, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, fillSaveProperties, generateMbyAtPreDef, generateParamsOK, generateParamsOK2, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, 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, 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, getLeaveIFVars, unionLabeledIFSymbols
getContainerType, getPO, implies, name, readProblem
public AbstractInfFlowPO(InitConfig initConfig, String name)
public Proof createProof(String proofName, Term poTerm, InitConfig proofConfig)
AbstractPO
createProof
in class AbstractPO
public InfFlowProof createProofObject(String proofName, String proofHeader, Term poTerm, InitConfig proofConfig)
createProofObject
in class AbstractPO