Modifier and Type | Method and Description |
---|---|
ProofApi |
ProofManagementApi.startProof(Contract contract) |
ProofApi |
ProofManagementApi.startProof(ProofOblInput contract) |
Modifier and Type | Method and Description |
---|---|
Proof |
AbstractUserInterfaceControl.createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
Proof |
UserInterfaceControl.createProof(InitConfig initConfig,
ProofOblInput input)
Instantiates a new
Proof in this UserInterfaceControl for the given
ProofOblInput based on the InitConfig . |
Proof |
KeYEnvironment.createProof(ProofOblInput input)
Creates a new
Proof with help of the UserInterfaceControl . |
Modifier and Type | Method and Description |
---|---|
void |
LemmataHandler.start() |
Modifier and Type | Method and Description |
---|---|
void |
LoopInvExecutionPO.readProblem() |
void |
InfFlowContractPO.readProblem() |
void |
BlockExecutionPO.readProblem() |
void |
SymbolicExecutionPO.readProblem() |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
KeYUserProblemFile.getPO() |
ProofAggregate |
ProofOblInput.getPO()
Returns the proof obligation term as result of the proof obligation
input.
|
InitConfig |
ProblemInitializer.prepare(EnvInput envInput)
Creates an initConfig / a proof environment and reads an EnvInput into it
|
ImmutableSet<PositionedString> |
KeYUserProblemFile.read() |
void |
ProblemInitializer.readEnvInput(EnvInput envInput,
InitConfig initConfig) |
void |
DependencyContractPO.readProblem() |
void |
FunctionalBlockContractPO.readProblem() |
void |
KeYUserProblemFile.readProblem() |
void |
WellDefinednessPO.readProblem() |
void |
ProofOblInput.readProblem() |
void |
FunctionalLoopContractPO.readProblem() |
void |
AbstractOperationPO.readProblem() |
Triple<java.lang.String,java.lang.Integer,java.lang.Integer> |
KeYUserProblemFile.readProofScript() |
ProofAggregate |
ProblemInitializer.startProver(EnvInput envInput,
ProofOblInput po) |
ProofAggregate |
ProblemInitializer.startProver(InitConfig initConfig,
ProofOblInput po) |
void |
ProblemInitializer.tryReadProof(IProofFileParser pfp,
KeYUserProblemFile kupf) |
Modifier and Type | Method and Description |
---|---|
protected InitConfig |
AbstractProblemLoader.createInitConfig()
Creates the
InitConfig . |
protected ProofAggregate |
AbstractProblemLoader.createProof(IPersistablePO.LoadedPOContainer poContainer)
Creates a
Proof for the given IPersistablePO.LoadedPOContainer and
tries to apply rules again. |
default java.lang.String |
EnvInput.getJavaFile()
Returns the file path to specific requested Java file.
|
protected ProofSettings |
KeYFile.getPreferences() |
void |
AbstractProblemLoader.load()
Executes the loading process and tries to instantiate a proof
and to re-apply rules on it if possible.
|
protected void |
AbstractProblemLoader.loadEnvironment()
Loads and initialized the proof environment.
|
protected void |
AbstractProblemLoader.loadSelectedProof(IPersistablePO.LoadedPOContainer poContainer,
ProofAggregate proofList)
Loads a proof from the proof list.
|
ImmutableSet<PositionedString> |
LDTInput.read()
reads all LDTs, i.e., all associated .key files with respect to
the given modification strategy.
|
ImmutableSet<PositionedString> |
KeYFile.read() |
ImmutableSet<PositionedString> |
EnvInput.read()
Reads the input using the given modification strategy, i.e.,
parts of the input do not modify the initial configuration while
others do.
|
java.util.List<java.io.File> |
AbstractEnvInput.readClassPath() |
java.util.List<java.io.File> |
LDTInput.readClassPath() |
java.util.List<java.io.File> |
EnvInput.readClassPath()
gets the classpath elements to be considered here.
|
void |
KeYFile.readFuncAndPred()
reads the functions and predicates declared in the .key file only,
modifying the function namespaces of the respective taclet options.
|
Includes |
AbstractEnvInput.readIncludes() |
Includes |
LDTInput.readIncludes() |
Includes |
KeYFile.readIncludes() |
Includes |
EnvInput.readIncludes()
Reads the include section and returns an Includes object.
|
java.lang.String |
AbstractEnvInput.readJavaPath() |
java.lang.String |
LDTInput.readJavaPath() |
java.lang.String |
KeYFile.readJavaPath() |
java.lang.String |
EnvInput.readJavaPath()
Reads the Java path.
|
ProofSettings |
KeYFile.readPreferences() |
Pair<java.lang.String,Location> |
AbstractProblemLoader.readProofScript() |
void |
KeYFile.readRules()
reads the rules and problems declared in the .key file only,
modifying the set of rules
of the initial configuration
|
void |
KeYFile.readSorts()
reads the sorts declaration of the .key file only,
modifying the sort namespace
of the initial configuration
|
Modifier and Type | Method and Description |
---|---|
protected abstract Proof |
AbstractCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected Proof |
AbstractSideProofCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
void |
AbstractCounterExampleGenerator.searchCounterExample(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent)
Searches a counter example for the given
Sequent . |
Modifier and Type | Method and Description |
---|---|
protected Proof |
AbstractTestGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
java.lang.String newName,
Sequent newSequent) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<PositionedString> |
SLEnvInput.read() |
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
DLSpecFactory.createDLClassInvariant(java.lang.String name,
java.lang.String displayName,
ParsableVariable selfVar,
Term inv)
Creates a class invariant from a formula and a designated "self".
|
FunctionalOperationContract |
DLSpecFactory.createDLOperationContract(java.lang.String name,
Term fma,
Term modifies)
Creates an operation contract from an implication formula of the form
"pre -> {heapAtPre := heap}
[#catchAll(java.lang.Throwable exc){m();}]post",
(where the update and/or the #catchAll may be omitted) and a modifies
clause.
|
Modifier and Type | Class and Description |
---|---|
class |
SLTranslationException |
class |
SLWarningException |
Modifier and Type | Method and Description |
---|---|
void |
SymbolicLayoutExtractor.analyse()
Computes the possible memory layouts.
|
IExecutionVariable[] |
ExecutionVariableExtractor.analyse()
Extracts the current state and represents it as
IExecutionVariable s. |
protected void |
ExecutionNodeWriter.appendBlockCompletions(int level,
IExecutionBlockStartNode<?> node,
java.lang.StringBuffer sb)
Appends the block completion entries to the given
StringBuffer . |
protected void |
ExecutionNodeWriter.appendCallStateVariables(int level,
IExecutionBaseMethodReturn<?> node,
boolean saveVariables,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionVariable s to the given StringBuffer . |
protected void |
ExecutionNodeWriter.appendChildren(int childLevel,
IExecutionNode<?> parent,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the child nodes to the given
StringBuffer . |
protected void |
ExecutionNodeWriter.appendCompletedBlocks(int level,
IExecutionNode<?> node,
java.lang.StringBuffer sb)
Appends the completed block entries to the given
StringBuffer . |
protected void |
ExecutionNodeWriter.appendConstraint(int level,
IExecutionConstraint constraint,
java.lang.StringBuffer sb)
Appends the given
IExecutionConstraint with its children to the given StringBuffer . |
protected void |
ExecutionNodeWriter.appendConstraints(int level,
IExecutionNode<?> node,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionConstraint s to the given StringBuffer . |
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.appendExecutionBlockContract(int level,
IExecutionAuxiliaryContract node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionAuxiliaryContract into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionBranchCondition(int level,
IExecutionBranchCondition node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionBranchCondition into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionBranchStatement(int level,
IExecutionBranchStatement node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionLoopCondition into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionExceptionalMethodReturn(int level,
IExecutionExceptionalMethodReturn node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionExceptionalMethodReturn into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionJoin(int level,
IExecutionJoin node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionJoin into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionLoopCondition(int level,
IExecutionLoopCondition node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionLoopCondition into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionLoopInvariant(int level,
IExecutionLoopInvariant node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionLoopInvariant into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionLoopStatement(int level,
IExecutionLoopStatement node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionLoopStatement into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionMethodCall(int level,
IExecutionMethodCall node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionMethodCall into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionMethodReturn(int level,
IExecutionMethodReturn node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionMethodReturn into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionMethodReturnValue(int level,
IExecutionMethodReturnValue returnValue,
java.lang.StringBuffer sb)
Converts the given
IExecutionMethodReturnValue into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionNode(int level,
IExecutionNode<?> node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionNode into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionOperationContract(int level,
IExecutionOperationContract node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionOperationContract into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionStart(int level,
IExecutionStart node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionStart into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionStatement(int level,
IExecutionStatement node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionStatement into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionTermination(int level,
IExecutionTermination node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionTermination into XML and appends it to the 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 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 void |
ExecutionNodeWriter.appendVariables(int level,
IExecutionNode<?> node,
boolean saveVariables,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionVariable s to the given StringBuffer . |
protected void |
AbstractUpdateExtractor.collectLocationsFromHeapTerms(Term selectTerm,
Term variableTerm,
HeapLDT heapLDT,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
java.util.Set<Term> objectsToIgnore)
Collects the
AbstractUpdateExtractor.ExtractLocationParameter location from the heap Term s. |
protected void |
AbstractUpdateExtractor.collectLocationsFromHeapUpdate(Term term,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill)
|
protected void |
AbstractUpdateExtractor.collectLocationsFromTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
Term term,
java.util.Set<Term> objectsToIgnore)
Utility method of
AbstractUpdateExtractor.extractLocationsFromTerm(Term, Set) which
recursively extracts the locations. |
protected void |
AbstractUpdateExtractor.collectLocationsFromTerm(Term updateTerm,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill,
java.util.Set<Term> objectsToIgnore)
|
protected void |
AbstractUpdateExtractor.collectLocationsFromUpdates(Sequent sequent,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<Term> |
SymbolicLayoutExtractor.collectObjectsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
Collects all objects which are used in the conditions of the
Sequent . |
protected java.util.Set<Term> |
SymbolicLayoutExtractor.collectSymbolicObjectsFromTerm(Term term,
java.util.Set<Term> objectsToIgnore)
Collects all objects which are used in the given
Term . |
protected Term |
AbstractUpdateExtractor.computeBranchCondition(Node node,
java.util.Map<Node,Term> branchConditionCache,
boolean simplifyConditions)
Computes the branch condition if not already present in the cache
and stores it in the cache.
|
protected java.util.Map<Goal,Term> |
AbstractUpdateExtractor.computeValueConditions(java.util.Set<Goal> valueGoals,
java.util.Map<Node,Term> branchConditionCache,
boolean simplifyConditions)
This method computes for all given
Goal s representing the same
value their path conditions. |
protected java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> |
AbstractUpdateExtractor.computeVariableValuePairs(Term layoutCondition,
Term layoutTerm,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
boolean currentLayout,
boolean simplifyConditions)
The method starts a side proof with the given arguments to compute
the values and objects of the requested memory layout.
|
protected ISymbolicLayout |
SymbolicLayoutExtractor.createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.lang.String stateName)
Creates an
ISymbolicLayout which shows the objects,
values and associations defined by the given ExecutionVariableValuePair s. |
protected LocationVariable |
AbstractUpdateExtractor.ExtractLocationParameter.createLocationVariable(java.lang.String name,
Sort sort)
Creates a new
LocationVariable with the given name and Sort . |
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 . |
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. |
static TruthValueTracingUtil.TruthValueTracingResult |
TruthValueTracingUtil.evaluate(Node node,
Name termLabelName,
boolean useUnicode,
boolean usePrettyPrinting)
|
protected static void |
TruthValueTracingUtil.evaluateNode(Node evaluationNode,
boolean useUnicode,
boolean usePrettyPrinting,
Node child,
int childIndexOnParent,
Name termLabelName,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> nodeResult,
TruthValueTracingUtil.TruthValueTracingResult result,
Services services)
|
protected java.util.List<ImmutableSet<Term>> |
SymbolicLayoutExtractor.extractAppliedCutsFromGoals(Proof proof)
Extracts the possible memory layouts from the given side proof.
|
protected ImmutableSet<Term> |
SymbolicLayoutExtractor.extractAppliedCutsSet(Node goalnode,
Node root)
Extracts the applied cut rules in the given
Node . |
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
AbstractUpdateExtractor.extractLocationsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
AbstractUpdateExtractor.extractLocationsFromTerm(Term term,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<Term> |
SymbolicLayoutExtractor.filterOutObjectsToIgnore(java.util.Set<Term> objectsToFilter,
java.util.Set<Term> objectsToIgnore)
Filters out the objects from the second
Set in the first Set . |
Term |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
IExecutionVariable[] |
ExecutionNodeReader.KeYlessValue.getChildVariables()
Returns contained child variables which forms complex data types.
|
ExecutionVariableExtractor.ExtractedExecutionVariable[] |
ExecutionVariableExtractor.ExtractedExecutionValue.getChildVariables()
Returns contained child variables which forms complex data types.
|
Term |
ExecutionNodeReader.KeYlessMethodReturnValue.getCondition()
Returns the optional condition under which the return value is valid.
|
Term |
ExecutionNodeReader.KeYlessValue.getCondition()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value. |
java.lang.String |
ExecutionNodeReader.KeYlessMethodReturnValue.getConditionString()
Returns the optional condition under which the return value is valid
as human readable
String . |
java.lang.String |
ExecutionNodeReader.KeYlessValue.getConditionString()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value as human readable String . |
java.lang.String |
ExecutionVariableExtractor.ExtractedExecutionValue.getConditionString()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value as human readable String . |
IExecutionConstraint[] |
ExecutionNodeReader.KeYlessValue.getConstraints()
Returns all available
IExecutionConstraint s. |
ImmutableList<Term> |
ExecutionNodeReader.KeYlessOperationContract.getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
ISymbolicLayout |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getCurrentLayout(int configurationIndex)
Returns the current memory layout which shows the memory
structure before the current node in the symbolic execution tree is executed.
|
ISymbolicLayout |
SymbolicLayoutExtractor.getCurrentLayout(int layoutIndex)
Returns the current memory layout at the given index.
|
Term |
ExecutionNodeReader.KeYlessOperationContract.getExceptionTerm()
|
java.lang.String |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
ExecutionNodeReader.KeYlessOperationContract.getFormatedContractParams()
Returns the human readable parameters of the called method for which a
Contract is applied. |
java.lang.String |
ExecutionNodeReader.KeYlessOperationContract.getFormatedExceptionTerm()
|
java.lang.String |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode.getFormatedMethodReturnCondition()
Returns the human readable condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
java.lang.String |
ExecutionNodeReader.KeYlessOperationContract.getFormatedResultTerm()
|
java.lang.String |
ExecutionNodeReader.KeYlessOperationContract.getFormatedSelfTerm()
|
ISymbolicLayout |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getInitialLayout(int configurationIndex)
Returns the initial memory layout before the method was executed.
|
ISymbolicLayout |
SymbolicLayoutExtractor.getInitialLayout(int layoutIndex)
Returns the initial memory layout at the given index.
|
protected ISymbolicLayout |
SymbolicLayoutExtractor.getLayout(java.util.Map<java.lang.Integer,ISymbolicLayout> confiurationsMap,
int layoutIndex,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
java.lang.String stateName,
boolean currentLayout)
Helper method of
SymbolicLayoutExtractor.getInitialLayout(int) and
SymbolicLayoutExtractor.getCurrentLayout(int) to lazily compute and get a memory layout. |
int |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getLayoutsCount()
Returns the number of memory layouts.
|
ImmutableList<ISymbolicEquivalenceClass> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getLayoutsEquivalenceClasses(int configurationIndex)
Returns the equivalence classes of the memory layout with the given index.
|
Term[] |
ExecutionNodeReader.KeYlessBranchCondition.getMergedBranchCondtions()
Returns the branch condition
Term s. |
Term |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode.getMethodReturnCondition()
Returns the condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
ExecutionNodeReader.KeYlessMethodReturn.getNameIncludingReturnValue()
Returns the human readable node name including the return value (
IExecutionMethodReturn.getReturnValues() ). |
Term |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getPathCondition()
Returns the path condition to reach this node as
Term . |
Term |
ExecutionNodeReader.KeYlessOperationContract.getResultTerm()
|
Term |
ExecutionNodeReader.KeYlessMethodReturnValue.getReturnValue()
Returns the return value.
|
IExecutionMethodReturnValue[] |
ExecutionNodeReader.KeYlessMethodReturn.getReturnValues()
Returns the possible return values.
|
java.lang.String |
ExecutionNodeReader.KeYlessMethodReturnValue.getReturnValueString()
Returns the return value as human readable
String . |
Term |
ExecutionNodeReader.KeYlessOperationContract.getSelfTerm()
|
java.lang.String |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode.getSignature()
Returns a human readable signature which describes this element.
|
java.lang.String |
ExecutionNodeReader.KeYlessMethodReturn.getSignatureIncludingReturnValue()
Returns the human readable signature including the return value (
IExecutionMethodReturn.getReturnValues() ). |
java.lang.String |
ExecutionVariableExtractor.ExtractedExecutionValue.getTypeString()
Returns the type of the variable as human readable string.
|
Term |
ExecutionNodeReader.KeYlessValue.getValue()
Returns the value of the variable.
|
IExecutionValue[] |
ExecutionVariableExtractor.ExtractedExecutionVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
java.lang.String |
ExecutionNodeReader.KeYlessValue.getValueString()
Returns the value of the variable as human readable string representation.
|
java.lang.String |
ExecutionVariableExtractor.ExtractedExecutionValue.getValueString()
Returns the value of the variable as human readable string representation.
|
boolean |
ExecutionNodeReader.KeYlessMethodReturnValue.hasCondition()
Checks if a condition is available via
IExecutionMethodReturnValue.getCondition()
under which this return value is returned. |
boolean |
ExecutionNodeReader.KeYlessValue.isValueAnObject()
Checks if the value represents an object or an attribute of the object
defined by the parent
IExecutionValue . |
boolean |
ExecutionNodeReader.KeYlessValue.isValueUnknown()
Checks if the value is unknown.
|
boolean |
ExecutionVariableExtractor.ExtractedExecutionValue.isValueUnknown()
Checks if the value is unknown.
|
protected ISymbolicLayout |
SymbolicLayoutExtractor.lazyComputeLayout(ImmutableSet<Term> layout,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.lang.String stateName,
boolean currentLayout)
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean) . |
protected java.lang.String |
ExecutionVariableExtractor.ExtractedExecutionVariable.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
java.lang.String |
ExecutionNodeWriter.toXML(IExecutionNode<?> node,
java.lang.String encoding,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints)
Converts the given
IExecutionNode into XML. |
void |
ExecutionNodeWriter.write(IExecutionNode<?> node,
java.lang.String encoding,
java.io.File file,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints)
Writes the given
IExecutionNode as XML file. |
void |
ExecutionNodeWriter.write(IExecutionNode<?> node,
java.lang.String encoding,
java.io.OutputStream out,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints)
Writes the given
IExecutionNode into the OutputStream . |
Constructor and Description |
---|
ExecutionVariableExtractor(Node node,
PosInOccurrence modalityPio,
IExecutionNode<?> executionNode,
Term condition,
boolean simplifyConditions)
Constructor.
|
ExtractLocationParameter(ProgramVariable programVariable,
boolean stateMember)
Constructor.
|
ExtractLocationParameter(ProgramVariable programVariable,
Term parentTerm)
Constructor.
|
ExtractLocationParameter(ProgramVariable programVariable,
Term parentTerm,
boolean stateMember)
Constructor.
|
ExtractLocationParameter(Term arrayIndex,
Term parentTerm)
Constructor.
|
ExtractLocationParameter(Term arrayStartIndex,
Term arrayEndIndex,
Term parentTerm)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Term |
IExecutionNode.getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
Term |
IExecutionBranchCondition.getBranchCondition()
Returns the branch condition as
Term . |
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.
|
Term |
IExecutionValue.getCondition()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value. |
Term |
IExecutionMethodReturnValue.getCondition()
Returns the optional condition under which the return value is valid.
|
java.lang.String |
IExecutionValue.getConditionString()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value as human readable String . |
java.lang.String |
IExecutionMethodReturnValue.getConditionString()
Returns the optional condition under which the return value is valid
as human readable
String . |
IExecutionConstraint[] |
IExecutionValue.getConstraints()
Returns all available
IExecutionConstraint s. |
ImmutableList<Term> |
IExecutionOperationContract.getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
ISymbolicLayout |
IExecutionNode.getCurrentLayout(int layoutIndex)
Returns the current memory layout which shows the memory
structure before the current node in the symbolic execution tree is executed.
|
Term |
IExecutionOperationContract.getExceptionTerm()
|
java.lang.String |
IExecutionNode.getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
IExecutionBranchCondition.getFormatedBranchCondition()
Returns the human readable branch condition as string.
|
java.lang.String |
IExecutionOperationContract.getFormatedContractParams()
Returns the human readable parameters of the called method for which a
Contract is applied. |
java.lang.String |
IExecutionOperationContract.getFormatedExceptionTerm()
|
java.lang.String |
IExecutionBaseMethodReturn.getFormatedMethodReturnCondition()
Returns the human readable condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
IExecutionNode.getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
java.lang.String |
IExecutionOperationContract.getFormatedResultTerm()
|
java.lang.String |
IExecutionOperationContract.getFormatedSelfTerm()
|
ISymbolicLayout |
IExecutionNode.getInitialLayout(int layoutIndex)
Returns the initial memory layout before the method was executed.
|
int |
IExecutionNode.getLayoutsCount()
Returns the number of memory layouts.
|
ImmutableList<ISymbolicEquivalenceClass> |
IExecutionNode.getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
Term[] |
IExecutionBranchCondition.getMergedBranchCondtions()
Returns the branch condition
Term s. |
Term |
IExecutionBaseMethodReturn.getMethodReturnCondition()
Returns the condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
IExecutionElement.getName()
Returns a human readable name which describes this element.
|
java.lang.String |
IExecutionMethodReturn.getNameIncludingReturnValue()
Returns the human readable node name including the return value (
IExecutionMethodReturn.getReturnValues() ). |
Term |
IExecutionNode.getPathCondition()
Returns the path condition to reach this node as
Term . |
Term |
IExecutionOperationContract.getResultTerm()
|
Term |
IExecutionMethodReturnValue.getReturnValue()
Returns the return value.
|
IExecutionMethodReturnValue[] |
IExecutionMethodReturn.getReturnValues()
Returns the possible return values.
|
java.lang.String |
IExecutionMethodReturnValue.getReturnValueString()
Returns the return value as human readable
String . |
Term |
IExecutionOperationContract.getSelfTerm()
|
java.lang.String |
IExecutionBaseMethodReturn.getSignature()
Returns a human readable signature which describes this element.
|
java.lang.String |
IExecutionMethodReturn.getSignatureIncludingReturnValue()
Returns the human readable signature including the return value (
IExecutionMethodReturn.getReturnValues() ). |
java.lang.String |
IExecutionValue.getTypeString()
Returns the type of the variable as human readable string.
|
Term |
IExecutionValue.getValue()
Returns the value of the variable.
|
IExecutionValue[] |
IExecutionVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
java.lang.String |
IExecutionValue.getValueString()
Returns the value of the variable as human readable string representation.
|
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.
|
boolean |
IExecutionMethodReturnValue.hasCondition()
Checks if a condition is available via
IExecutionMethodReturnValue.getCondition()
under which this return value is returned. |
boolean |
IExecutionValue.isValueAnObject()
Checks if the value represents an object or an attribute of the object
defined by the parent
IExecutionValue . |
boolean |
IExecutionValue.isValueUnknown()
Checks if the value is unknown.
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.String |
ExecutionMethodReturn.computeCalledMethodSignature()
Computes the signature of the called method.
|
protected Term |
ExecutionVariable.computeValueCondition(TermBuilder tb,
java.util.List<Goal> valueGoals,
InitConfig initConfig)
|
Term |
AbstractExecutionNode.getBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
Term |
ExecutionBranchCondition.getBranchCondition()
Returns the branch condition as
Term . |
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.
|
Term |
ExecutionMethodReturnValue.getCondition()
Returns the optional condition under which the return value is valid.
|
Term |
AbstractExecutionValue.getCondition()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value. |
java.lang.String |
ExecutionValue.getConditionString()
Returns the condition under which the variable (
IExecutionValue.getVariable() )
has this value as human readable String . |
java.lang.String |
ExecutionMethodReturnValue.getConditionString()
Returns the optional condition under which the return value is valid
as human readable
String . |
IExecutionConstraint[] |
AbstractExecutionValue.getConstraints()
Returns all available
IExecutionConstraint s. |
ImmutableList<Term> |
ExecutionOperationContract.getContractParams()
Returns the parameters of the called method for which a
Contract is applied. |
ISymbolicLayout |
AbstractExecutionNode.getCurrentLayout(int layoutIndex)
Returns the current memory layout which shows the memory
structure before the current node in the symbolic execution tree is executed.
|
Term |
ExecutionOperationContract.getExceptionTerm()
|
java.lang.String |
AbstractExecutionNode.getFormatedBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode)
Returns the human readable condition under which this node completes the code block of the given
IExecutionBlockStartNode . |
java.lang.String |
ExecutionBranchCondition.getFormatedBranchCondition()
Returns the human readable branch condition as string.
|
java.lang.String |
ExecutionOperationContract.getFormatedContractParams()
Returns the human readable parameters of the called method for which a
Contract is applied. |
java.lang.String |
ExecutionOperationContract.getFormatedExceptionTerm()
|
java.lang.String |
AbstractExecutionMethodReturn.getFormatedMethodReturnCondition()
Returns the human readable condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
ExecutionBranchCondition.getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
java.lang.String |
AbstractExecutionNode.getFormatedPathCondition()
Returns the human readable path condition to reach this node as string.
|
java.lang.String |
ExecutionOperationContract.getFormatedResultTerm()
|
java.lang.String |
ExecutionOperationContract.getFormatedSelfTerm()
|
ISymbolicLayout |
AbstractExecutionNode.getInitialLayout(int layoutIndex)
Returns the initial memory layout before the method was executed.
|
ExecutionNodeSymbolicLayoutExtractor |
AbstractExecutionNode.getLayoutExtractor()
Returns the used
ExecutionNodeSymbolicLayoutExtractor . |
int |
AbstractExecutionNode.getLayoutsCount()
Returns the number of memory layouts.
|
ImmutableList<ISymbolicEquivalenceClass> |
AbstractExecutionNode.getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
Term[] |
ExecutionBranchCondition.getMergedBranchCondtions()
Returns the branch condition
Term s. |
Term |
AbstractExecutionMethodReturn.getMethodReturnCondition()
Returns the condition under which this method return is reached from
the calling
IExecutionMethodCall . |
java.lang.String |
AbstractExecutionElement.getName()
Returns a human readable name which describes this element.
|
java.lang.String |
ExecutionMethodReturn.getNameIncludingReturnValue()
Returns the human readable node name including the return value (
IExecutionMethodReturn.getReturnValues() ). |
Term |
ExecutionBranchCondition.getPathCondition()
Returns the path condition to reach this node as
Term . |
Term |
AbstractExecutionNode.getPathCondition()
Returns the path condition to reach this node as
Term . |
Term |
ExecutionOperationContract.getResultTerm()
|
Term |
ExecutionMethodReturnValue.getReturnValue()
Returns the return value.
|
IExecutionMethodReturnValue[] |
ExecutionMethodReturn.getReturnValues()
Returns the possible return values.
|
java.lang.String |
ExecutionMethodReturnValue.getReturnValueString()
Returns the return value as human readable
String . |
Term |
ExecutionOperationContract.getSelfTerm()
|
java.lang.String |
AbstractExecutionMethodReturn.getSignature()
Returns a human readable signature which describes this element.
|
java.lang.String |
ExecutionMethodReturn.getSignatureIncludingReturnValue()
Returns the human readable signature including the return value (
IExecutionMethodReturn.getReturnValues() ). |
java.lang.String |
ExecutionValue.getTypeString()
Returns the type of the variable as human readable string.
|
Term |
AbstractExecutionValue.getValue()
Returns the value of the variable.
|
ExecutionValue[] |
ExecutionVariable.getValues()
Returns the possible values of this
IExecutionVariable . |
java.lang.String |
ExecutionValue.getValueString()
Returns the value of the variable as human readable string representation.
|
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 void |
ExecutionVariable.groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
boolean |
ExecutionMethodReturnValue.hasCondition()
Checks if a condition is available via
IExecutionMethodReturnValue.getCondition()
under which this return value is returned. |
protected ExecutionValue[] |
ExecutionVariable.instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
boolean |
AbstractExecutionValue.isValueAnObject()
Checks if the value represents an object or an attribute of the object
defined by the parent
IExecutionValue . |
boolean |
ExecutionValue.isValueUnknown()
Checks if the value is unknown.
|
protected java.lang.Object |
AbstractExecutionNode.lazyComputeBlockCompletionCondition(IExecutionBlockStartNode<?> completedNode,
boolean returnFormatedCondition)
Computes the condition lazily when
#getBlockCompletionCondition(IExecutionNode)
or #getFormatedBlockCompletionCondition(IExecutionNode) is called the first time. |
protected void |
ExecutionBranchCondition.lazyComputeBranchCondition()
Computes the branch condition lazily when
ExecutionBranchCondition.getBranchCondition()
or ExecutionBranchCondition.getFormatedBranchCondition() is called the first time. |
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 java.lang.String |
ExecutionMethodReturnValue.lazyComputeConditionString()
Computes the human readable return value of this node lazily when
ExecutionMethodReturnValue.getConditionString()
is called the first time. |
protected IExecutionConstraint[] |
AbstractExecutionValue.lazyComputeConstraints()
Computes the related constraints lazily when
AbstractExecutionValue.getConstraints() is called the first time. |
protected ExecutionNodeSymbolicLayoutExtractor |
AbstractExecutionNode.lazyComputeLayoutExtractor()
Instantiates the used
ExecutionNodeSymbolicLayoutExtractor lazily
when AbstractExecutionNode.getLayoutExtractor() is called the first time. |
protected Term[] |
ExecutionBranchCondition.lazyComputeMergedBranchCondtions()
Computes the branch condition lazily when
ExecutionBranchCondition.getMergedBranchCondtions()
is called the first time. |
protected void |
AbstractExecutionMethodReturn.lazyComputeMethodReturnCondition()
Computes the method return condition lazily when
AbstractExecutionMethodReturn.getMethodReturnCondition()
or AbstractExecutionMethodReturn.getFormatedMethodReturnCondition() is called the first time. |
protected java.lang.String |
ExecutionAllArrayIndicesVariable.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionAuxiliaryContract.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
AbstractExecutionVariable.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionOperationContract.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionConstraint.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionMethodReturnValue.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected abstract java.lang.String |
AbstractExecutionElement.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
AbstractExecutionValue.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionBranchCondition.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionMethodReturn.lazyComputeName()
Computes the name of this node lazily when
AbstractExecutionElement.getName()
is called the first time. |
protected java.lang.String |
ExecutionMethodReturn.lazyComputeNameIncludingReturnValue()
Computes the name including the return value lazily when
ExecutionMethodReturn.getNameIncludingReturnValue() is called the first time. |
protected void |
ExecutionBranchCondition.lazyComputePathCondition()
Computes the path condition lazily when
ExecutionBranchCondition.getPathCondition()
or ExecutionBranchCondition.getFormatedPathCondition() is called the first time. |
protected IExecutionMethodReturnValue[] |
ExecutionMethodReturn.lazyComputeReturnValues()
Computes the return value lazily when
#getReturnValue() is called the first time. |
protected java.lang.String |
ExecutionMethodReturnValue.lazyComputeReturnValueString()
Computes the human readable return value of this node lazily when
ExecutionMethodReturnValue.getReturnValueString()
is called the first time. |
protected abstract java.lang.String |
AbstractExecutionMethodReturn.lazyComputeSignature()
Computes the signature lazily when
AbstractExecutionMethodReturn.getSignature() is called the first time. |
protected java.lang.String |
ExecutionExceptionalMethodReturn.lazyComputeSignature()
Computes the signature lazily when
AbstractExecutionMethodReturn.getSignature() is called the first time. |
protected java.lang.String |
ExecutionMethodReturn.lazyComputeSignature()
Computes the signature lazily when
AbstractExecutionMethodReturn.getSignature() is called the first time. |
protected java.lang.String |
ExecutionMethodReturn.lazyComputeSigntureIncludingReturnValue()
Computes the signature including the return value lazily when
ExecutionMethodReturn.getNameIncludingReturnValue() is called the first time. |
protected ExecutionValue[] |
ExecutionAllArrayIndicesVariable.lazyComputeValues()
Computes the value for
ExecutionVariable.getValues()
lazily when the method is called the first time. |
protected ExecutionValue[] |
ExecutionVariable.lazyComputeValues()
Computes the value for
ExecutionVariable.getValues()
lazily when the method 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. |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
AbstractSideProofRule.computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
Modifier and Type | Method and Description |
---|---|
protected boolean |
ThinBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected abstract boolean |
AbstractBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected abstract ImmutableArray<Node> |
AbstractSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
ImmutableArray<Node> |
AbstractBackwardSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
protected void |
AbstractSlicer.listModifiedHeapLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
Recursive utility method used by
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update. |
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
ReferencePrefix seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Term term,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionUtil.canComputeVariables(IExecutionNode<?> node,
Services services)
Checks if it is right now possible to compute the variables of the given
IExecutionNode
via IExecutionNode.getVariables() . |
static Term |
SymbolicExecutionUtil.computeBranchCondition(Node node,
boolean simplify,
boolean improveReadability)
Computes the branch condition of the given
Node . |
static Term |
SymbolicExecutionUtil.computePathCondition(Node node,
boolean simplify,
boolean improveReadability)
Computes the path condition of the given
Node . |
static Term |
SymbolicExecutionUtil.computePathCondition(Node parentNode,
Node childNode,
boolean simplify,
boolean improveReadability)
Computes the path condition between the given
Node s. |
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
SymbolicExecutionSideProofUtil.computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term and conditions. |
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. |
static ProofStarter |
SymbolicExecutionSideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
static Term |
SymbolicExecutionSideProofUtil.extractOperatorTerm(ApplyStrategyInfo info,
Operator operator)
Extracts the operator term for the formula with the given
Operator
from the site proof result (ApplyStrategyInfo ). |
static boolean |
SymbolicExecutionUtil.isNotNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
SymbolicExecutionUtil.isNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static SymbolicExecutionUtil.ContractPostOrExcPostExceptionVariableResult |
SymbolicExecutionUtil.searchContractPostOrExcPostExceptionVariable(Node node,
Services services)
Searches the used exception variable in the post or exceptional post branch of an applied
ContractRuleApp on the parent of the given Node . |
static Term |
SymbolicExecutionUtil.simplify(InitConfig initConfig,
Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
SymbolicExecutionUtil.simplify(InitConfig initConfig,
Term term)
Simplifies the given
Term in a side proof. |
static Term |
SymbolicExecutionUtil.simplify(Proof parentProof,
Term term)
Simplifies the given
Term in a side proof. |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof for the given
Sequent . |
Modifier and Type | Method and Description |
---|---|
ProofAggregate |
TacletProofObligationInput.getPO() |
ImmutableSet<PositionedString> |
EmptyEnvInput.read() |
void |
TacletProofObligationInput.readProblem() |
Modifier and Type | Method and Description |
---|---|
static ProofStarter |
SideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
ProofAggregate |
ProofStarter.UserProvidedInput.getPO() |
void |
ProofStarter.init(Sequent sequentToProve,
ProofEnvironment env,
java.lang.String proofName)
creates a new proof object for sequentToProve and registers it in the given environment
|
void |
ProofStarter.init(Term formulaToProve,
ProofEnvironment env)
creates a new proof object for formulaToProve and registers it in the given environment
|
ProofAggregate |
HelperClassForTests.parseThrowException(java.io.File file) |
ProofAggregate |
HelperClassForTests.parseThrowException(java.io.File file,
Profile profile) |
void |
ProofStarter.UserProvidedInput.readProblem() |
static java.util.HashMap<java.lang.String,java.lang.String> |
HelperClassForTests.setDefaultTacletOptions(java.io.File baseDir,
java.lang.String javaPathInBaseDir)
Ensures that the default taclet options are defined.
|
static java.util.HashMap<java.lang.String,java.lang.String> |
HelperClassForTests.setDefaultTacletOptionsForTarget(java.io.File javaFile,
java.lang.String containerTypeName,
java.lang.String targetName)
Ensures that the default taclet options are defined.
|
Copyright © 2003-2019 The KeY-Project.