Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.KeYlessConstraint
An implementation of
IExecutionConstraint which is independent
from KeY and provides such only children and default attributes. |
Modifier and Type | Method and Description |
---|---|
IExecutionConstraint[] |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getConstraints()
Returns all available
IExecutionConstraint s. |
IExecutionConstraint[] |
ExecutionNodeReader.KeYlessValue.getConstraints()
Returns all available
IExecutionConstraint s. |
protected IExecutionConstraint[] |
ExecutionVariableExtractor.ExtractedExecutionValue.getNodeConstraints()
Returns all available
IExecutionConstraint s of the IExecutionNode on which this IExecutionValue is part of. |
Modifier and Type | Method and Description |
---|---|
void |
ExecutionNodeReader.AbstractKeYlessExecutionNode.addConstraint(IExecutionConstraint constraint)
Adds the given
IExecutionConstraint . |
void |
ExecutionNodeReader.KeYlessValue.addConstraint(IExecutionConstraint constraint)
Adds the given
IExecutionConstraint . |
protected void |
ExecutionNodeWriter.appendConstraint(int level,
IExecutionConstraint constraint,
java.lang.StringBuffer sb)
Appends the given
IExecutionConstraint with its children to the given StringBuffer . |
Modifier and Type | Method and Description |
---|---|
IExecutionConstraint[] |
IExecutionValue.getConstraints()
Returns all available
IExecutionConstraint s. |
IExecutionConstraint[] |
IExecutionNode.getConstraints()
Returns all available
IExecutionConstraint s. |
Modifier and Type | Class and Description |
---|---|
class |
ExecutionConstraint
The default implementation of
IExecutionConstraint . |
Modifier and Type | Method and Description |
---|---|
IExecutionConstraint[] |
AbstractExecutionValue.getConstraints()
Returns all available
IExecutionConstraint s. |
IExecutionConstraint[] |
AbstractExecutionNode.getConstraints()
Returns all available
IExecutionConstraint s. |
protected IExecutionConstraint[] |
ExecutionValue.getNodeConstraints()
Returns all available
IExecutionConstraint s of the IExecutionNode on which this IExecutionValue is part of. |
protected abstract IExecutionConstraint[] |
AbstractExecutionValue.getNodeConstraints()
Returns all available
IExecutionConstraint s of the IExecutionNode on which this IExecutionValue is part of. |
protected IExecutionConstraint[] |
ExecutionMethodCall.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionLoopStatement.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionAuxiliaryContract.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionJoin.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionBranchStatement.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionLoopInvariant.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionOperationContract.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionLoopCondition.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionTermination.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionStart.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
AbstractExecutionValue.lazyComputeConstraints()
Computes the related constraints lazily when
AbstractExecutionValue.getConstraints() is called the first time. |
protected IExecutionConstraint[] |
ExecutionBranchCondition.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionExceptionalMethodReturn.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionMethodReturn.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected IExecutionConstraint[] |
ExecutionStatement.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
protected abstract IExecutionConstraint[] |
AbstractExecutionNode.lazyComputeConstraints()
Computes the constraints lazily when
AbstractExecutionNode.getConstraints() is
called the first time. |
Modifier and Type | Method and Description |
---|---|
static IExecutionConstraint[] |
SymbolicExecutionUtil.createExecutionConstraints(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
IExecutionConstraint s. |
Copyright © 2003-2019 The KeY-Project.