public class InfFlowContractPO extends AbstractInfFlowPO implements ContractPO, InfFlowLeavePO
IPersistablePO.LoadedPOContainer
Modifier and Type | Field and Description |
---|---|
private InformationFlowContract |
contract |
private IFProofObligationVars |
ifVars |
private InfFlowProofSymbols |
infFlowSymbols
For saving and loading Information-Flow proofs, we need to remember the
according taclets, program variables, functions and such.
|
private ProofObligationVars |
symbExecVars |
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 |
---|
InfFlowContractPO(InitConfig initConfig,
InformationFlowContract contract) |
createProof, createProofObject
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFreePre, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, generateParamsOK, generateParamsOK2, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit
assignPOTerms, collectClassAxioms, getName, getPO, name, register, register, register, selectClassAxioms
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getPO, name
private final InformationFlowContract contract
private final ProofObligationVars symbExecVars
private final IFProofObligationVars ifVars
private InfFlowProofSymbols infFlowSymbols
public InfFlowContractPO(InitConfig initConfig, InformationFlowContract contract)
public void readProblem() throws ProofInputException
AbstractOperationPO
readProblem
in interface ProofOblInput
readProblem
in class AbstractOperationPO
ProofInputException
public boolean implies(ProofOblInput po)
ProofOblInput
implies
in interface ProofOblInput
implies
in class AbstractPO
public Term getMbyAtPre()
getMbyAtPre
in interface ContractPO
protected String buildPOName(boolean transactionFlag)
Proof
based on the given transaction flag.buildPOName
in class AbstractOperationPO
transactionFlag
- The transaction flag.protected IProgramMethod getProgramMethod()
IProgramMethod
to call.getProgramMethod
in class AbstractOperationPO
IProgramMethod
to call.protected boolean isTransactionApplicable()
isTransactionApplicable
in class AbstractOperationPO
protected KeYJavaType getCalleeKeYJavaType()
KeYJavaType
which contains AbstractOperationPO.getProgramMethod()
.getCalleeKeYJavaType
in class AbstractOperationPO
KeYJavaType
which contains AbstractOperationPO.getProgramMethod()
.protected Modality getTerminationMarker()
Modality
to use as termination marker.getTerminationMarker
in class AbstractOperationPO
public InformationFlowContract getContract()
getContract
in interface ContractPO
public IFProofObligationVars getIFVars()
public void fillSaveProperties(Properties properties) throws IOException
ProofSaver
to store the proof
specific settings in the given Properties
. The stored settings
have to contain all information required to instantiate the proof
obligation again and this instance should create the same Sequent
(if code and specifications are unchanged).fillSaveProperties
in interface IPersistablePO
fillSaveProperties
in class AbstractOperationPO
properties
- The Properties
to fill with the proof obligation specific settings.IOException
- Occurred Exception.public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, Properties properties)
initConfig
- The already load InitConfig
.properties
- The settings of the proof obligation to instantiate.public InfFlowProofSymbols getIFSymbols()
getIFSymbols
in interface InfFlowPO
public final void addIFSymbol(Term t)
addIFSymbol
in interface InfFlowPO
public void addIFSymbol(Named n)
addIFSymbol
in interface InfFlowPO
public void addLabeledIFSymbol(Term t)
addLabeledIFSymbol
in interface InfFlowPO
public void addLabeledIFSymbol(Named n)
addLabeledIFSymbol
in interface InfFlowPO
public void unionLabeledIFSymbols(InfFlowProofSymbols symbols)
unionLabeledIFSymbols
in interface InfFlowPO
protected Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm, ImmutableList<Term> paramTerms, Services services)
getGlobalDefs
in class AbstractOperationPO
public IFProofObligationVars getLeaveIFVars()
getLeaveIFVars
in interface InfFlowPO
@Deprecated protected ImmutableList<StatementBlock> buildOperationBlocks(ImmutableList<LocationVariable> formalParVars, ProgramVariable selfVar, ProgramVariable resultVar, Services services)
AbstractOperationPO
buildOperationBlocks
in class AbstractOperationPO
formalParVars
- Arguments from formal parameters for method call.selfVar
- The self variable.resultVar
- The result variable.services
- TODO@Deprecated protected Term getPre(List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Map<LocationVariable,LocationVariable> atPreVars, Services services)
AbstractOperationPO
getPre
in class AbstractOperationPO
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.atPreVars
- Mapping of LocationVariable
to the LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the precondition.@Deprecated protected Term getPost(List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, Map<LocationVariable,LocationVariable> atPreVars, Services services)
AbstractOperationPO
getPost
in class AbstractOperationPO
modHeaps
- The heaps.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.resultVar
- The result variable.exceptionVar
- The exception variable.atPreVars
- Mapping of LocationVariable
to the LocationVariable
which contains the initial value.services
- The Services
to use.Term
representing the postcondition.@Deprecated protected Term buildFrameClause(List<LocationVariable> modHeaps, Map<Term,Term> heapToAtPre, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
AbstractOperationPO
buildFrameClause
in class AbstractOperationPO
modHeaps
- The heaps.heapToAtPre
- The previous heap before execution.selfVar
- The self variable.paramVars
- The parameters ProgramVariable
s.services
- TODOTerm
representing the frame clause.@Deprecated protected Term generateMbyAtPreDef(ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, Services services)
generateMbyAtPreDef
in class AbstractOperationPO
public KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.getContainerType
in interface ProofOblInput
getContainerType
in class AbstractPO
KeYJavaType
in which the proven element is contained in or null
if not available.