public interface IExecutionOperationContract extends IExecutionNode<SourceElement>
A node in the symbolic execution tree which represents a use operation contract application.
The default implementation is ExecutionOperationContract
which
is instantiated via a SymbolicExecutionTreeBuilder
instance.
SymbolicExecutionTreeBuilder
,
ExecutionOperationContract
INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START
Modifier and Type | Method and Description |
---|---|
Contract |
getContract()
Returns the applied
Contract . |
ImmutableList<Term> |
getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
IProgramMethod |
getContractProgramMethod()
Returns the
IProgramMethod of the applied Contract . |
Term |
getExceptionTerm()
|
java.lang.String |
getFormatedContractParams()
Returns the human readable parameters of the called method for which a
Contract is applied. |
java.lang.String |
getFormatedExceptionTerm()
|
java.lang.String |
getFormatedResultTerm()
|
java.lang.String |
getFormatedSelfTerm()
|
Term |
getResultTerm()
|
Term |
getSelfTerm()
|
boolean |
hasNotNullCheck()
Checks if a not null check is available (instance method) or not (static method or constructor).
|
boolean |
isNotNullCheckComplied()
Checks if the not null check is complied.
|
boolean |
isPreconditionComplied()
Checks if the precondition is complied.
|
getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged
getAppliedRuleApp, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed
IProgramMethod getContractProgramMethod()
IProgramMethod
of the applied Contract
.IProgramMethod
of the applied Contract
.boolean isPreconditionComplied()
true
precondition complied, false
precondition not complied.boolean hasNotNullCheck()
true
not null check available, false
not null check is not available.boolean isNotNullCheckComplied()
true
not null check complied, false
not null check not complied.Term getResultTerm() throws ProofInputException
Term
in which the result of the applied Contract
is stored.ProofInputException
- Occurred Exception.Term getExceptionTerm() throws ProofInputException
Term
in which a by the Contract
thrown Exception
is stored.ProofInputException
- Occurred Exception.Term getSelfTerm() throws ProofInputException
Term
or null
if not available.ProofInputException
- Occurred Exception.ImmutableList<Term> getContractParams() throws ProofInputException
Contract
is applied.Contract
is applied.ProofInputException
- Occurred Exception.java.lang.String getFormatedResultTerm() throws ProofInputException
Term
in which the result of the applied Contract
is stored.ProofInputException
- Occurred Exception.java.lang.String getFormatedExceptionTerm() throws ProofInputException
Term
in which a by the Contract
thrown Exception
is stored.ProofInputException
- Occurred Exception.java.lang.String getFormatedSelfTerm() throws ProofInputException
Term
or null
if not available.ProofInputException
- Occurred Exception.java.lang.String getFormatedContractParams() throws ProofInputException
Contract
is applied.Contract
is applied.ProofInputException
- Occurred Exception.