de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessOperationContract

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessOperationContract

All Implemented Interfaces:

IExecutionElement, IExecutionNode<SourceElement>, IExecutionOperationContract

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessOperationContract
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>
implements IExecutionOperationContract

An implementation of IExecutionOperationContract which is independent from KeY and provides such only children and default attributes.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	formatedContractParams The formated contract parameters.
private java.lang.String	formatedExceptionTerm The formated exception term.
private java.lang.String	formatedResultTerm The formated result term.
private java.lang.String	formatedSelfTerm The formated self term.
private boolean	hasNotNullCheck Has not null check?
private boolean	notNullCheckComplied Is not null check complied?
private boolean	preconditionComplied Is precondition complied?

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
KeYlessOperationContract(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean preconditionComplied, boolean hasNotNullCheck, boolean notNullCheckComplied, java.lang.String formatedResultTerm, java.lang.String formatedExceptionTerm, java.lang.String formatedSelfTerm, java.lang.String formatedContractParams) Constructor.

Method Summary

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.
java.lang.String	getElementType() Returns a human readable element type name.
Term	getExceptionTerm() Returns the exception Term in which a by the Contract thrown Exception is stored.
java.lang.String	getFormatedContractParams() Returns the human readable parameters of the called method for which a Contract is applied.
java.lang.String	getFormatedExceptionTerm() Returns the human readable exception Term in which a by the Contract thrown Exception is stored.
java.lang.String	getFormatedResultTerm() Returns the human readable result Term in which the result of the applied Contract is stored.
java.lang.String	getFormatedSelfTerm() Returns the human readable self Term of the called method for which a Contract is applied.
Term	getResultTerm() Returns the result Term in which the result of the applied Contract is stored.
Term	getSelfTerm() Returns the self Term of the called method for which a Contract is applied.
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.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode

addCallStackEntry, addChild, addCompletedBlock, addConstraint, addIncomingLink, addOutgoingLink, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

preconditionComplied

private final boolean preconditionComplied

Is precondition complied?

hasNotNullCheck

private final boolean hasNotNullCheck

Has not null check?

notNullCheckComplied

private final boolean notNullCheckComplied

Is not null check complied?

formatedResultTerm

private final java.lang.String formatedResultTerm

The formated result term.

formatedExceptionTerm

private final java.lang.String formatedExceptionTerm

The formated exception term.

formatedSelfTerm

private final java.lang.String formatedSelfTerm

The formated self term.

formatedContractParams

private final java.lang.String formatedContractParams

The formated contract parameters.

Constructor Detail

KeYlessOperationContract

public KeYlessOperationContract(IExecutionNode<?> parent,
                                java.lang.String name,
                                java.lang.String formatedPathCondition,
                                boolean pathConditionChanged,
                                boolean preconditionComplied,
                                boolean hasNotNullCheck,
                                boolean notNullCheckComplied,
                                java.lang.String formatedResultTerm,
                                java.lang.String formatedExceptionTerm,
                                java.lang.String formatedSelfTerm,
                                java.lang.String formatedContractParams)

Constructor.

Parameters:

parent - The parent IExecutionNode.

name - The name of this node.

pathConditionChanged - Is the path condition changed compared to parent?

formatedPathCondition - The formated path condition.

preconditionComplied - Is precondition complied?

hasNotNullCheck - Has not null check?

notNullCheckComplied - Is not null check complied?

formatedResultTerm - The formated result term.

formatedExceptionTerm - The formated exception term.

formatedSelfTerm - The formated self term.

formatedContractParams - The formated contract parameters.

Method Detail

getElementType

public java.lang.String getElementType()

Returns a human readable element type name.

Specified by:

getElementType in interface IExecutionElement

Returns:

The human readable element type.

getContract

public Contract getContract()

Returns the applied Contract.

Specified by:

getContract in interface IExecutionOperationContract

Returns:

The applied Contract.

getContractProgramMethod

public IProgramMethod getContractProgramMethod()

Returns the IProgramMethod of the applied Contract.

Specified by:

getContractProgramMethod in interface IExecutionOperationContract

Returns:

The IProgramMethod of the applied Contract.

isPreconditionComplied

public boolean isPreconditionComplied()

Checks if the precondition is complied.

Specified by:

isPreconditionComplied in interface IExecutionOperationContract

Returns:

true precondition complied, false precondition not complied.

hasNotNullCheck

public boolean hasNotNullCheck()

Checks if a not null check is available (instance method) or not (static method or constructor).

Specified by:

hasNotNullCheck in interface IExecutionOperationContract

Returns:

true not null check available, false not null check is not available.

isNotNullCheckComplied

public boolean isNotNullCheckComplied()

Checks if the not null check is complied.

Specified by:

isNotNullCheckComplied in interface IExecutionOperationContract

Returns:

true not null check complied, false not null check not complied.

getResultTerm

public Term getResultTerm()
                   throws ProofInputException

Returns the result Term in which the result of the applied Contract is stored.

Specified by:

getResultTerm in interface IExecutionOperationContract

Returns:

The result Term in which the result of the applied Contract is stored.

Throws:

ProofInputException - Occurred Exception.

getExceptionTerm

public Term getExceptionTerm()
                      throws ProofInputException

Returns the exception Term in which a by the Contract thrown Exception is stored.

Specified by:

getExceptionTerm in interface IExecutionOperationContract

Returns:

The exception Term in which a by the Contract thrown Exception is stored.

Throws:

ProofInputException - Occurred Exception.

getFormatedResultTerm

public java.lang.String getFormatedResultTerm()
                                       throws ProofInputException

Returns the human readable result Term in which the result of the applied Contract is stored.

Specified by:

getFormatedResultTerm in interface IExecutionOperationContract

Returns:

The human readable result Term in which the result of the applied Contract is stored.

Throws:

ProofInputException - Occurred Exception.

getFormatedExceptionTerm

public java.lang.String getFormatedExceptionTerm()
                                          throws ProofInputException

Returns the human readable exception Term in which a by the Contract thrown Exception is stored.

Specified by:

getFormatedExceptionTerm in interface IExecutionOperationContract

Returns:

The human readable exception Term in which a by the Contract thrown Exception is stored.

Throws:

ProofInputException - Occurred Exception.

getSelfTerm

public Term getSelfTerm()
                 throws ProofInputException

Returns the self Term of the called method for which a Contract is applied.

Specified by:

getSelfTerm in interface IExecutionOperationContract

Returns:

The self Term or null if not available.

Throws:

ProofInputException - Occurred Exception.

getContractParams

public ImmutableList<Term> getContractParams()
                                      throws ProofInputException

Returns the parameters of the called method for which a Contract is applied.

Specified by:

getContractParams in interface IExecutionOperationContract

Returns:

The parameters of the called method for which a Contract is applied.

Throws:

ProofInputException - Occurred Exception.

getFormatedSelfTerm

public java.lang.String getFormatedSelfTerm()
                                     throws ProofInputException

Returns the human readable self Term of the called method for which a Contract is applied.

Specified by:

getFormatedSelfTerm in interface IExecutionOperationContract

Returns:

The human readable self Term or null if not available.

Throws:

ProofInputException - Occurred Exception.

getFormatedContractParams

public java.lang.String getFormatedContractParams()
                                           throws ProofInputException

Returns the human readable parameters of the called method for which a Contract is applied.

Specified by:

getFormatedContractParams in interface IExecutionOperationContract

Returns:

The human readable parameters of the called method for which a Contract is applied.

Throws:

ProofInputException - Occurred Exception.