Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl |
Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.KeYlessValue
An implementation of
IExecutionValue which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionVariableExtractor.ExtractedExecutionValue
The
IExecutionValue instantiated by the ExecutionVariableExtractor . |
Modifier and Type | Method and Description |
---|---|
IExecutionValue |
ExecutionNodeReader.KeYlessVariable.getParentValue()
Returns the parent
IExecutionValue if available. |
IExecutionValue[] |
ExecutionNodeReader.KeYlessVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
IExecutionValue[] |
ExecutionVariableExtractor.ExtractedExecutionVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
Modifier and Type | Method and Description |
---|---|
void |
ExecutionNodeReader.KeYlessVariable.addValue(IExecutionValue variable)
Adds the given child
IExecutionValue . |
protected void |
ExecutionNodeWriter.appendConstraints(int level,
IExecutionValue value,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionConstraint s to the given StringBuffer . |
protected void |
ExecutionNodeWriter.appendValue(int level,
IExecutionValue value,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the given
IExecutionValue with its children to the given StringBuffer . |
protected ExecutionNodeReader.KeYlessVariable |
ExecutionNodeReader.createVariable(IExecutionValue parentValue,
java.lang.String uri,
java.lang.String localName,
java.lang.String qName,
org.xml.sax.Attributes attributes)
Creates a new
IExecutionVariable with the given content. |
Modifier and Type | Method and Description |
---|---|
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 |
---|
KeYlessVariable(IExecutionValue parentValue,
boolean isArrayIndex,
java.lang.String arrayIndexString,
java.lang.String name)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IExecutionValue |
IExecutionVariable.getParentValue()
Returns the parent
IExecutionValue if available. |
IExecutionValue[] |
IExecutionVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
Modifier and Type | Class and Description |
---|---|
class |
AbstractExecutionValue
Provides a basic implementation of
IExecutionValue . |
class |
ExecutionValue
The default implementation of
IExecutionValue . |
Modifier and Type | Method and Description |
---|---|
IExecutionValue |
AbstractExecutionVariable.getParentValue()
Returns the parent
IExecutionValue if available. |
Constructor and Description |
---|
AbstractExecutionVariable(ITreeSettings settings,
Node proofNode,
IProgramVariable programVariable,
IExecutionValue parentValue,
Term arrayIndex,
Term additionalCondition,
PosInOccurrence modalityPIO)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.