public class InfFlowContractPO extends AbstractInfFlowPO implements ContractPO, InfFlowLeafPO
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
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 |
---|
InfFlowContractPO(InitConfig initConfig,
InformationFlowContract contract) |
Modifier and Type | Method and Description |
---|---|
void |
addIFSymbol(Named n) |
void |
addIFSymbol(Term t) |
void |
addLabeledIFSymbol(Named n) |
void |
addLabeledIFSymbol(Term t) |
protected Term |
buildFrameClause(java.util.List<LocationVariable> modHeaps,
java.util.Map<Term,Term> heapToAtPre,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected ImmutableList<StatementBlock> |
buildOperationBlocks(ImmutableList<LocationVariable> formalParVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
Services services)
Deprecated.
|
protected java.lang.String |
buildPOName(boolean transactionFlag)
Returns the name of the
Proof based on the given transaction flag. |
void |
fillSaveProperties(java.util.Properties properties)
This method is called by a
ProofSaver to store the proof
specific settings in the given Properties . |
protected Term |
generateMbyAtPreDef(ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
Services services)
Deprecated.
|
protected KeYJavaType |
getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
KeYJavaType |
getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
InformationFlowContract |
getContract() |
protected Term |
getGlobalDefs(LocationVariable heap,
Term heapTerm,
Term selfTerm,
ImmutableList<Term> paramTerms,
Services services) |
InfFlowProofSymbols |
getIFSymbols() |
IFProofObligationVars |
getIFVars() |
IFProofObligationVars |
getLeafIFVars()
Get the information flow proof obligation variables (set of four sets of
proof obligation variables necessary for information flow proofs) for
the "leaf" (i.e., child of child of ..) information flow proof
obligation.
|
Term |
getMbyAtPre() |
protected Term |
getPost(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable exceptionVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected Term |
getPre(java.util.List<LocationVariable> modHeaps,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
Services services)
Deprecated.
|
protected IProgramMethod |
getProgramMethod()
Returns the
IProgramMethod to call. |
protected Modality |
getTerminationMarker()
Returns the
Modality to use as termination marker. |
boolean |
implies(ProofOblInput po)
If true, then this PO implies the passed one.
|
protected boolean |
isTransactionApplicable()
Checks if transactions are applicable.
|
static IPersistablePO.LoadedPOContainer |
loadFrom(InitConfig initConfig,
java.util.Properties properties)
Instantiates a new proof obligation with the given settings.
|
void |
readProblem() |
void |
unionLabeledIFSymbols(InfFlowProofSymbols symbols) |
createProof, createProofObject
addAdditionalUninterpretedPredicateIfRequired, addUninterpretedPredicateIfRequired, buildFreePre, buildJavaBlock, buildProgramTerm, buildUpdate, createUninterpretedPredicate, ensureUninterpretedPredicateExists, generateParamsOK, generateParamsOK2, getAdditionalUninterpretedPredicates, getAdditionalUninterpretedPredicates, getBaseHeap, getCreatedInitConfigForSingleProof, getInitialTaclets, getSavedHeap, getUninterpretedPredicate, getUninterpretedPredicate, getUninterpretedPredicateName, isAddSymbolicExecutionLabel, isAddSymbolicExecutionLabel, isAddUninterpretedPredicate, isAddUninterpretedPredicate, isCopyOfMethodArgumentsUsed, isMakeNamesUnique, modifyPostTerm, newAdditionalUninterpretedPredicate, postInit
assignPOTerms, collectClassAxioms, generateSelfCreated, generateSelfExactType, generateSelfExactType, generateSelfNotNull, 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 java.lang.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
Modality
to use as termination marker.public InformationFlowContract getContract()
getContract
in interface ContractPO
public IFProofObligationVars getIFVars()
public void fillSaveProperties(java.util.Properties properties) throws java.io.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.java.io.IOException
- Occurred Exception.public static IPersistablePO.LoadedPOContainer loadFrom(InitConfig initConfig, java.util.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 getLeafIFVars()
InfFlowPO
getLeafIFVars
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
- services instance@Deprecated protected Term getPre(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.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(java.util.List<LocationVariable> modHeaps, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable exceptionVar, java.util.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(java.util.List<LocationVariable> modHeaps, java.util.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
- services instanceTerm
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.