Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.KeYlessVariable
An implementation of
IExecutionVariable which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionVariableExtractor.ExtractedExecutionVariable
The
IExecutionVariable instantiated by the ExecutionVariableExtractor . |
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
ExecutionVariableExtractor.analyse()
Extracts the current state and represents it as
IExecutionVariable s. |
protected IExecutionVariable |
ExecutionVariableExtractor.createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue,
ImmutableList<Term> alreadyVisitedObjects)
Creates an
IExecutionVariable for the given ExecutionVariableValuePair s. |
IExecutionVariable[] |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode.getCallStateVariables()
Returns the variable value pairs of the state when the method has been called.
|
IExecutionVariable[] |
ExecutionNodeReader.KeYlessValue.getChildVariables()
Returns contained child variables which forms complex data types.
|
IExecutionVariable |
ExecutionNodeReader.KeYlessValue.getVariable()
Returns the parent
IExecutionVariable . |
IExecutionVariable[] |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getVariables()
Returns the variable value pairs of the current state.
|
IExecutionVariable[] |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getVariables(Term condition)
Returns the variable value pairs of the current state under the given condition.
|
Modifier and Type | Method and Description |
---|---|
void |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode.addCallStateVariable(IExecutionVariable variable)
Adds the given
IExecutionVariable . |
void |
ExecutionNodeReader.KeYlessValue.addChildVariable(IExecutionVariable variable)
Adds the given child
IExecutionVariable . |
void |
ExecutionNodeReader.AbstractKeYlessExecutionNode.addVariable(IExecutionVariable variable)
Adds the given
IExecutionVariable . |
protected void |
ExecutionNodeWriter.appendValues(int level,
IExecutionVariable variable,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionValue s to the given StringBuffer . |
protected void |
ExecutionNodeWriter.appendVariable(int level,
IExecutionVariable variable,
boolean saveConstraints,
java.lang.String tagName,
java.lang.StringBuffer sb)
Appends the given
IExecutionVariable with its children to the given StringBuffer . |
protected ExecutionNodeReader.KeYlessValue |
ExecutionNodeReader.createValue(IExecutionVariable parentVariable,
java.lang.String uri,
java.lang.String localName,
java.lang.String qName,
org.xml.sax.Attributes attributes)
Creates a new
IExecutionValue with the given content. |
protected void |
ExecutionVariableExtractor.createValues(IExecutionVariable variable,
java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
AbstractUpdateExtractor.ExecutionVariableValuePair firstPair,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
java.util.List<IExecutionValue> valueListToFill,
ImmutableList<Term> alreadyVisitedObjects)
Creates the
IExecutionValue s of the given IExecutionVariable . |
Constructor and Description |
---|
ExtractedExecutionValue(IExecutionNode<?> parentNode,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
KeYlessValue(IExecutionVariable variable,
java.lang.String typeString,
java.lang.String valueString,
java.lang.String name,
boolean valueUnknown,
boolean valueAnObject,
java.lang.String conditionString)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
IExecutionBaseMethodReturn.getCallStateVariables()
Returns the variable value pairs of the state when the method has been called.
|
IExecutionVariable[] |
IExecutionValue.getChildVariables()
Returns contained child variables which forms complex data types.
|
IExecutionVariable |
IExecutionValue.getVariable()
Returns the parent
IExecutionVariable . |
IExecutionVariable[] |
IExecutionNode.getVariables()
Returns the variable value pairs of the current state.
|
IExecutionVariable[] |
IExecutionNode.getVariables(Term condition)
Returns the variable value pairs of the current state under the given condition.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractExecutionVariable
Provides a basic implementation of
IExecutionVariable s. |
class |
ExecutionAllArrayIndicesVariable
An implementation of
IExecutionVariable used to query
all array indices at the same time. |
class |
ExecutionVariable
The default implementation of
IExecutionVariable . |
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
AbstractExecutionMethodReturn.getCallStateVariables()
Returns the variable value pairs of the state when the method has been called.
|
IExecutionVariable[] |
ExecutionValue.getChildVariables()
Returns contained child variables which forms complex data types.
|
IExecutionVariable |
AbstractExecutionValue.getVariable()
Returns the parent
IExecutionVariable . |
IExecutionVariable[] |
AbstractExecutionNode.getVariables()
Returns the variable value pairs of the current state.
|
IExecutionVariable[] |
AbstractExecutionNode.getVariables(Term condition)
Returns the variable value pairs of the current state under the given condition.
|
protected IExecutionVariable[] |
AbstractExecutionMethodReturn.lazyComputeCallStateVariables()
Computes the variables lazily when
AbstractExecutionMethodReturn.getCallStateVariables() is
called the first time. |
protected IExecutionVariable[] |
ExecutionValue.lazyComputeChildVariables()
Computes the contained child variables lazily when
ExecutionValue.getChildVariables() is called the first time. |
protected IExecutionVariable[] |
AbstractExecutionNode.lazyComputeVariables()
Computes the variables lazily when
AbstractExecutionNode.getVariables() is
called the first time. |
protected IExecutionVariable[] |
AbstractExecutionNode.lazyComputeVariables(Term condition)
Computes the variables lazily when
AbstractExecutionNode.getVariables(Term) is
called the first time. |
Constructor and Description |
---|
AbstractExecutionValue(ITreeSettings settings,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static IExecutionVariable[] |
SymbolicExecutionUtil.createAllExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
Modifier and Type | Method and Description |
---|---|
static Term |
SymbolicExecutionUtil.createSelectTerm(IExecutionVariable variable)
Creates recursive a term which can be used to determine the value
of
#getProgramVariable() . |
Copyright © 2003-2019 The KeY-Project.