Modifier and Type | Method and Description |
---|---|
Node |
ProjectedNode.getProofNode() |
Modifier and Type | Method and Description |
---|---|
static <T> ScriptResult |
ScriptResult.create(Node node,
ProjectedNode onNode,
ProofScriptCommandCall<T> call) |
Constructor and Description |
---|
ProjectedNode(Node node,
ProjectedNode parent)
Creates the wrapper object for a proof node
|
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractProofControl.emitInteractivePrune(Node node) |
void |
AbstractProofControl.pruneTo(Node node)
Prunes a proof to the given node.
|
void |
DefaultProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
ProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
void |
InteractionListener.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
void |
InteractionListener.runPrune(Node node) |
Modifier and Type | Method and Description |
---|---|
void |
InteractionListener.runAutoMode(java.util.List<Node> initialGoals,
Proof proof,
ApplyStrategyInfo info) |
Modifier and Type | Method and Description |
---|---|
Node |
KeYMediator.getSelectedNode()
returns the current selected node
|
Node |
KeYSelectionModel.getSelectedNode()
returns the node that is selected by the user
|
Modifier and Type | Method and Description |
---|---|
void |
KeYSelectionModel.nearestOpenGoalSelection(Node old)
selects the first open goal below the given node old if no open goal
is available node old is selected.
|
void |
KeYMediator.nonGoalNodeChosen(Node node)
notifies that a node that is not a goal has been chosen
|
boolean |
KeYMediator.processDelayedCut(Node invokedNode) |
void |
KeYMediator.setBack(Node node) |
void |
KeYSelectionModel.setSelectedNode(Node n)
sets the node that is focused by the user
|
Modifier and Type | Method and Description |
---|---|
Node |
NodeInfoVisualizer.getNode() |
Modifier and Type | Method and Description |
---|---|
protected void |
ProofMacroWorker.emitProofMacroFinished(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
static java.util.SortedSet<NodeInfoVisualizer> |
NodeInfoVisualizer.getInstances(Node node)
Returns the set of open
NodeInfoWindow s associated with the specified node. |
static boolean |
NodeInfoVisualizer.hasInstances(Node node)
Returns
true iff there are any open NodeInfoWindow s
associated with the specified node. |
Constructor and Description |
---|
InspectorForDecisionPredicates(Services services,
Node node,
int cutMode,
java.util.List<ApplicationCheck> additionalChecks) |
NodeInfoVisualizer(Node node,
java.lang.String longName,
java.lang.String shortName)
Creates a new
NodeInfoVisualizer . |
ProofMacroWorker(Node node,
ProofMacro macro,
KeYMediator mediator,
PosInOccurrence posInOcc)
Instantiates a new proof macro worker.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<javax.swing.Action> |
ContextMenuAdapter.getContextActions(KeYMediator mediator,
ContextMenuKind kind,
Node underlyingObject) |
Modifier and Type | Method and Description |
---|---|
Node |
CurrentGoalView.jumpToIntroduction(Node node,
SequentFormula form)
given a node and a sequent formula, returns the first node
among the node's parents that contains the sequent formula @form.
|
Modifier and Type | Method and Description |
---|---|
Node |
CurrentGoalView.jumpToIntroduction(Node node,
SequentFormula form)
given a node and a sequent formula, returns the first node
among the node's parents that contains the sequent formula @form.
|
java.lang.String |
HTMLSyntaxHighlighter.process(java.lang.String plainTextString,
Node displayedNode)
Computes a String for the given plain text where HTML elements have been
escaped and syntax highlighting has been added.
|
Constructor and Description |
---|
InnerNodeView(Node node,
MainWindow mainWindow) |
OpenCurrentNodeAction(MainWindow mainWindow,
Node node) |
SequentViewDock(MainWindow mainWindow,
Node node) |
Constructor and Description |
---|
OriginTermLabelVisualizer(PosInOccurrence pos,
Node node,
Services services)
Creates a new
OriginTermLabelVisualizer . |
Modifier and Type | Method and Description |
---|---|
Node |
ProofDifferenceView.getLeft() |
Node |
ProofDifferenceView.getRight() |
Modifier and Type | Method and Description |
---|---|
static ProofDifference |
ProofDifference.create(Node left,
Node right,
java.util.function.Function<Term,java.lang.String> printer) |
static ProofDifference |
ProofDifference.create(Services services,
Node left,
Node right) |
void |
ProofDifferenceView.setLeft(Node left) |
void |
ProofDifferenceView.setRight(Node right) |
Constructor and Description |
---|
OpenDifferenceWithParent(MainWindow mainWindow,
Node node) |
ProofDifferenceView(Node left,
Node right,
KeYMediator mediator) |
Modifier and Type | Method and Description |
---|---|
protected Node |
GUIAbstractTreeNode.findChild(Node n) |
Node |
GUIAbstractTreeNode.getNode() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
GUIAbstractTreeNode.ensureBranchLabelIsSet(Node p_node) |
GUIAbstractTreeNode |
GUIProofTreeModel.find(Node n)
Return the GUIProofTreeNode corresponding to node n, if one
has already been generated, and null otherwise.
|
de.uka.ilkd.key.gui.prooftree.GUIBranchNode |
GUIProofTreeModel.findBranch(Node n)
Return the GUIBranchNode corresponding to the subtree rooted
at n, if one has already been generated, and null otherwise.
|
protected javax.swing.tree.TreeNode |
GUIAbstractTreeNode.findBranch(Node p_node) |
protected Node |
GUIAbstractTreeNode.findChild(Node n) |
de.uka.ilkd.key.gui.prooftree.GUIBranchNode |
GUIProofTreeModel.getBranchNode(Node n,
java.lang.Object label)
Return the GUIBranchNode corresponding to the subtree rooted
at n.
|
GUIAbstractTreeNode |
GUIProofTreeModel.getProofTreeNode(Node n)
Return the GUIProofTreeNode corresponding to node n.
|
static boolean |
ProofTreeViewFilter.hiddenByGlobalFilters(Node node) |
protected void |
ProofTreeView.makeNodeExpanded(Node n) |
void |
ProofTreeView.makeNodeVisible(Node n)
moves the scope of the tree view to the given node so that it
is visible
|
abstract boolean |
ProofTreeViewFilter.showSubtree(Node node) |
void |
GUIProofTreeModel.updateTree(Node p_node) |
Constructor and Description |
---|
GUIAbstractTreeNode(GUIProofTreeModel tree,
Node node) |
Modifier and Type | Method and Description |
---|---|
java.util.Map<Node,PosInOccurrence> |
ServiceCaches.getExhaustiveMacroCache() |
Modifier and Type | Method and Description |
---|---|
void |
Services.saveNameRecorder(Node n) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
VariableNamer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
|
Modifier and Type | Method and Description |
---|---|
ProofMacroFinishedInfo |
ProofMacro.applyTo(UserInterfaceControl uic,
Node node,
PosInOccurrence posInOcc,
ProverTaskListener listener)
Apply this macro on the given node.
|
ProofMacroFinishedInfo |
AbstractProofMacro.applyTo(UserInterfaceControl uic,
Node node,
PosInOccurrence posInOcc,
ProverTaskListener listener) |
boolean |
ProofMacro.canApplyTo(Node node,
PosInOccurrence posInOcc)
Can this macro be applied on the given node?
This method should not make any changes but check if the macro can be
applied or not on the given node.
|
boolean |
AbstractProofMacro.canApplyTo(Node node,
PosInOccurrence posInOcc) |
Modifier and Type | Method and Description |
---|---|
Node |
ScriptNode.getProofNode() |
Modifier and Type | Method and Description |
---|---|
protected static Goal |
EngineState.getGoal(ImmutableList<Goal> openGoals,
Node node) |
void |
EngineState.setGoal(Node node) |
void |
ScriptNode.setProofNode(Node proofNode) |
Modifier and Type | Method and Description |
---|---|
Node |
Node.child(int i) |
Node |
Node.commonAncestor(Node other)
Search for the root of the smallest subtree containing
this and other ; we assume that the two nodes are
part of the same proof tree |
Node |
Proof.findAny(java.util.function.Predicate<Node> pred)
Bread-first search for the first node, that matches the given
predicate.
|
Node |
ProofTreeEvent.getNode() |
Node |
Goal.node()
returns the referenced node
|
Node |
Node.parent() |
Node |
Proof.root()
returns the root node of the proof
|
Modifier and Type | Method and Description |
---|---|
java.util.Iterator<Node> |
Node.childrenIterator() |
java.util.Iterator<Node> |
Node.iterator()
Returns an iterator over this node's children.
|
java.util.Iterator<Node> |
Node.leavesIterator() |
ImmutableList<Node> |
Proof.pruneProof(Node cuttingPoint)
Prunes the subtree beneath the node
cuttingPoint , i.e. |
ImmutableList<Node> |
Proof.pruneProof(Node cuttingPoint,
boolean fireChanges) |
java.util.Iterator<Node> |
Node.subtreeIterator() |
Modifier and Type | Method and Description |
---|---|
void |
Node.add(Node newChild)
Makes the given node a child of this node.
|
void |
Node.addAll(Node[] newChildren)
Makes the given node children of this node.
|
void |
Proof.breadthFirstSearch(Node startNode,
ProofVisitor visitor)
Makes a downwards directed breadth first search on the proof tree, starting with node
startNode . |
Goal |
Goal.clone(Node node)
clones the goal (with copy of tacletindex and ruleAppIndex).
|
Node |
Node.commonAncestor(Node other)
Search for the root of the smallest subtree containing
this and other ; we assume that the two nodes are
part of the same proof tree |
boolean |
Proof.find(Node node)
returns true iff the given node is found in the proof tree
|
boolean |
Node.find(Node node)
Searches for a given node in the subtree starting with this node.
|
protected void |
Goal.fireGoalReplaced(Goal goal,
Node parent,
ImmutableList<Goal> newGoals) |
protected void |
Proof.fireNotesChanged(Node node)
Fires the event
ProofTreeListener.notesChanged(ProofTreeEvent) to all listener. |
void |
Proof.fireProofExpanded(Node node)
fires the event that the proof has been expanded at the given node
|
protected void |
Proof.fireProofIsBeingPruned(Node below)
fires the event that the proof is being pruned at the given node
|
protected void |
Proof.fireProofPruned(Node below)
fires the event that the proof has been pruned at the given node
|
int |
Node.getChildNr(Node child) |
Goal |
Proof.getClosedGoal(Node node)
Get the closed goal belonging to the given node if it exists.
|
ImmutableList<Goal> |
Proof.getClosedSubtreeGoals(Node node)
Returns a list of all (closed) goals of the closed subtree pending from this node.
|
Goal |
Proof.getGoal(Node node)
returns the goal that belongs to the given node or null if the
node is an inner one
|
java.lang.String |
VariableNameProposer.getNameProposal(java.lang.String basename,
Services services,
Node undoAnchor) |
java.lang.String |
InstantiationProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
VariableNameProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
InstantiationProposerCollection.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals) |
ImmutableList<Goal> |
Proof.getSubtreeEnabledGoals(Node node)
get the list of goals of the subtree starting with node which are enabled.
|
ImmutableList<Goal> |
Proof.getSubtreeGoals(Node node)
returns the list of goals of the subtree starting with node.
|
void |
GoalListener.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
boolean |
Proof.isClosedGoal(Node node) |
boolean |
Proof.isGoal(Node node)
returns true if the given node is part of a Goal
|
static boolean |
NodeInfo.isSymbolicExecutionRuleApplied(Node node)
Checks if a rule is applied on the given
Node which performs symbolic execution. |
ImmutableList<Node> |
Proof.pruneProof(Node cuttingPoint)
Prunes the subtree beneath the node
cuttingPoint , i.e. |
ImmutableList<Node> |
Proof.pruneProof(Node cuttingPoint,
boolean fireChanges) |
void |
Proof.setRoot(Node root)
sets the root of the proof
|
void |
Proof.traverseFromChildToParent(Node child,
Node parent,
ProofVisitor visitor) |
void |
ProofVisitor.visit(Proof proof,
Node visitedNode) |
Modifier and Type | Method and Description |
---|---|
Node |
Proof.findAny(java.util.function.Predicate<Node> pred)
Bread-first search for the first node, that matches the given
predicate.
|
Constructor and Description |
---|
Goal(Node node,
RuleAppIndex ruleAppIndex)
creates a new goal referencing the given node
|
Node(Proof proof,
Sequent seq,
Node parent)
creates a node with the given contents, the given collection of children (all
elements must be of class Node) and the given parent node.
|
NodeInfo(Node node) |
ProofTreeEvent(Proof source,
Node node)
Create ProofTreeEvent for an event that happens at
the specified node.
|
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services)
Computes the
IProofReference of the given Node . |
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services,
ImmutableList<IProofReferencesAnalyst> analysts)
Computes the
IProofReference of the given Node . |
Modifier and Type | Method and Description |
---|---|
java.util.LinkedHashSet<IProofReference<?>> |
ClassAxiomAndInvariantProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
ProgramVariableReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
MethodBodyExpandProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
ContractProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
IProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
MethodCallProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
protected IProofReference<IProgramMethod> |
MethodCallProofReferencesAnalyst.createReference(Node node,
Services services,
ExecutionContext context,
MethodReference mr)
Creates an
IProofReference to the called IProgramMethod . |
protected ExecutionContext |
MethodCallProofReferencesAnalyst.extractContext(Node node,
Services services)
Extracts the
ExecutionContext . |
protected void |
ProgramVariableReferencesAnalyst.listReferences(Node node,
ProgramElement pe,
ProgramVariable arrayLength,
java.util.LinkedHashSet<IProofReference<?>> toFill,
boolean includeExpressionContainer)
Extracts the proof references recursive.
|
Modifier and Type | Method and Description |
---|---|
java.util.LinkedHashSet<Node> |
DefaultProofReference.getNodes()
Returns the
Node s in which the reference was found. |
java.util.LinkedHashSet<Node> |
IProofReference.getNodes()
Returns the
Node s in which the reference was found. |
Modifier and Type | Method and Description |
---|---|
void |
DefaultProofReference.addNodes(java.util.Collection<Node> nodes)
|
void |
IProofReference.addNodes(java.util.Collection<Node> nodes)
|
Constructor and Description |
---|
DefaultProofReference(java.lang.String kind,
Node node,
T target)
Constructor
|
Modifier and Type | Field and Description |
---|---|
Node |
NodeGoalPair.node |
Modifier and Type | Method and Description |
---|---|
Node |
DelayedCut.getNode() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Node> |
DelayedCut.getSubtrees() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
ApplicationCheck.check(Node cutNode,
Term cutFormula) |
java.lang.String |
ApplicationCheck.NoNewSymbolsCheck.check(Node cutNode,
Term cutFormula) |
Constructor and Description |
---|
DelayedCut(Proof proof,
Node node,
Term formula,
ImmutableList<Node> subtrees,
int sideOfDecisionPredicate,
RuleApp firstAppliedRuleApp) |
DelayedCutProcessor(Proof proof,
Node node,
Term descisionPredicate,
int mode) |
NodeGoalPair(Node node,
Goal goal) |
Constructor and Description |
---|
DelayedCut(Proof proof,
Node node,
Term formula,
ImmutableList<Node> subtrees,
int sideOfDecisionPredicate,
RuleApp firstAppliedRuleApp) |
Modifier and Type | Method and Description |
---|---|
void |
InitConfig.registerRuleIntroducedAtNode(RuleApp r,
Node node,
boolean isAxiom) |
Modifier and Type | Method and Description |
---|---|
Node |
AbstractProblemLoader.ReplayResult.getNode() |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
OutputStreamProofSaver.builtinRuleIfInsts(Node node,
ImmutableList<PosInOccurrence> ifInsts) |
java.lang.String |
OutputStreamProofSaver.ifFormulaInsts(Node node,
ImmutableList<IfFormulaInstantiation> l) |
void |
OutputStreamProofSaver.node2Proof(Node node,
java.lang.Appendable ps)
Print applied rule(s) for a proof node and its decendants into the passed writer
such that in can be loaded again as a proof.
|
Constructor and Description |
---|
ReplayResult(java.lang.String status,
java.util.List<java.lang.Throwable> errors,
Node node) |
Modifier and Type | Method and Description |
---|---|
Node |
PredicateEstimator.Result.getCommonParent() |
Node |
ProspectivePartner.getCommonParent() |
Node |
ProspectivePartner.getNode(int index) |
Modifier and Type | Method and Description |
---|---|
java.util.List<java.lang.String> |
LateApplicationCheck.check(Node node,
Node cutNode,
ApplicationCheck check) |
void |
ProspectivePartner.setCommonParent(Node commonParent) |
Constructor and Description |
---|
ProspectivePartner(Term commonFormula,
Node node1,
SequentFormula formula1,
Term update1,
Node node2,
SequentFormula formula2,
Term update2)
Constructs a new prospective partner object, i.e.
|
Constructor and Description |
---|
RuleJustificationByAddRules(Node node,
boolean isAxiom) |
Modifier and Type | Method and Description |
---|---|
Node |
NodeReplacement.getNode() |
Node |
RuleAppInfo.getOriginalNode() |
Modifier and Type | Method and Description |
---|---|
void |
NodeChangeJournal.goalReplaced(Goal source,
Node parent,
ImmutableList<Goal> newGoals)
Informs the listener that the given goal
source
has been replaced by the goals newGoals (note that
source may be an element of
newGoals ). |
Constructor and Description |
---|
NodeReplacement(Node p_node,
Node p_parent,
ImmutableList<SequentChangeInfo> p_changes) |
Modifier and Type | Method and Description |
---|---|
void |
GoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
Modifier and Type | Field and Description |
---|---|
protected Node |
DefaultGoalChooser.currentSubtreeRoot |
Modifier and Type | Method and Description |
---|---|
protected void |
DefaultGoalChooser.findMinimalSubtree(Node p_startNode)
Search for a minimal subtree of the proof tree which is not
closable (constraints of its goals are inconsistent) starting
at p_startNode
PRECONDITION: all goals have satisfiable constraints
|
protected boolean |
DefaultGoalChooser.findMinimalSubtreeBelow(Node p_startNode)
Search for a minimal subtree of the proof tree which is not
closable (constraints of its goals are inconsistent) below
p_startNode
PRECONDITION: * !isSatisfiableSubtree ( p_startNode )
* all goals have satisfiable constraints
|
protected boolean |
DefaultGoalChooser.isSatisfiableSubtree(Node p_root) |
void |
DefaultGoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals) |
protected void |
DefaultGoalChooser.updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
protected void |
DepthFirstGoalChooser.updateGoalListHelp(Node node,
ImmutableList<Goal> newGoals) |
Modifier and Type | Method and Description |
---|---|
Node |
CloseAfterMergeRuleBuiltInRuleApp.getCorrespondingMergeNode() |
Node |
MergeRuleBuiltInRuleApp.getMergeNode() |
Node |
CloseAfterMergeRuleBuiltInRuleApp.getThePartnerNode() |
Modifier and Type | Method and Description |
---|---|
CloseAfterMergeRuleBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames)
Creates a complete CloseAfterMergeBuiltInRuleApp.
|
void |
CloseAfterMergeRuleBuiltInRuleApp.setCorrespondingMergeNode(Node correspondingMergeNode) |
void |
MergeRuleBuiltInRuleApp.setMergeNode(Node mergeNode) |
void |
CloseAfterMergeRuleBuiltInRuleApp.setThePartnerNode(Node thePartnerNode) |
Constructor and Description |
---|
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames) |
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Node mergeNode,
ImmutableList<MergePartner> mergePartners,
MergeProcedure concreteRule,
SymbolicExecutionStateWithProgCnt thisSEState,
ImmutableList<SymbolicExecutionState> mergePartnerStates,
Term distForm,
java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners) |
Modifier and Type | Field and Description |
---|---|
LRUCache<Node,IfInstantiationCachePool.IfInstantiationCache> |
IfInstantiationCachePool.cacheMgr |
Modifier and Type | Method and Description |
---|---|
IfInstantiationCachePool.IfInstantiationCache |
IfInstantiationCachePool.getCache(Node n) |
void |
IfInstantiationCachePool.release(Node n) |
Modifier and Type | Field and Description |
---|---|
protected Node |
AbstractUpdateExtractor.node
Contains the
Node of KeY's proof tree to compute memory layouts for. |
Modifier and Type | Method and Description |
---|---|
protected Node |
SymbolicExecutionTreeBuilder.findMethodCallNode(Node currentNode,
RuleApp ruleApp)
|
Node |
AbstractUpdateExtractor.NodeGoal.getCurrentNode()
Returns the current
Node . |
Node |
AbstractUpdateExtractor.ExecutionVariableValuePair.getGoalNode()
Returns the
Node on which this result is based on. |
Node |
TruthValueTracingUtil.BranchResult.getLeafNode()
Returns the leaf
Node . |
Node[] |
ExecutionNodeReader.KeYlessBranchCondition.getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this
IExecutionBranchCondition . |
Node |
AbstractUpdateExtractor.NodeGoal.getParent()
Returns the parent of
AbstractUpdateExtractor.NodeGoal.getCurrentNode() . |
Node |
ExecutionNodeReader.AbstractKeYlessExecutionElement.getProofNode()
Returns the
Node in KeY's proof tree which is represented by this execution tree node. |
protected Node |
AbstractUpdateExtractor.getRoot()
Returns the root
Node of the proof. |
protected Node |
SymbolicExecutionTreeBuilder.searchPreviousSymbolicExecutionNode(Node node)
Searches the first node in the parent hierarchy (including the given node)
which executes a statement.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<Node> |
SymbolicExecutionTreeBuilder.findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
Node node) |
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> |
SymbolicExecutionTreeBuilder.getAfterBlockMaps(int id)
Returns the after block map used for the given ID.
|
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> |
SymbolicExecutionTreeBuilder.getAfterBlockMaps(SymbolicExecutionTermLabel label)
Returns the after block map.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(int id)
Returns the method call stack used for the given ID.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(int id)
Returns the method call stack used for the given ID.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(RuleApp ruleApp)
Returns the method call stack.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(RuleApp ruleApp)
Returns the method call stack.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(SymbolicExecutionTermLabel label)
Returns the method call stack.
|
protected java.util.Map<Node,ImmutableList<Node>> |
SymbolicExecutionTreeBuilder.getMethodCallStack(SymbolicExecutionTermLabel label)
Returns the method call stack.
|
protected java.util.Set<Node> |
SymbolicExecutionTreeBuilder.getMethodReturnsToIgnore(int id)
Returns the method
Node s of method calls for
which its return should be ignored. |
protected java.util.Set<Node> |
SymbolicExecutionTreeBuilder.getMethodReturnsToIgnore(RuleApp ruleApp)
Returns the method
Node s of method calls for
which its return should be ignored. |
protected java.util.Set<Node> |
SymbolicExecutionTreeBuilder.getMethodReturnsToIgnore(SymbolicExecutionTermLabel label)
Returns the method
Node s of method calls for
which its return should be ignored. |
Modifier and Type | Method and Description |
---|---|
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.addNodeToTreeAndUpdateParent(Node node,
AbstractExecutionNode<?> parentToAddTo,
AbstractExecutionNode<?> executionNode)
Adds the new created
AbstractExecutionNode to the symbolic execution tree
if available and returns the new parent for future detected nodes. |
protected void |
SymbolicExecutionTreeBuilder.addToBlockMap(Node node,
AbstractExecutionBlockStartNode<?> blockStartNode)
Adds the given
AbstractExecutionNode add reason for a new block to the block maps. |
protected void |
SymbolicExecutionTreeBuilder.addToBlockMap(Node node,
AbstractExecutionBlockStartNode<?> blockStartNode,
int stackSize,
SourceElement... sourceElements)
Adds the given
AbstractExecutionNode add reason for a new block to the block maps. |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.analyzeNode(Node node,
AbstractExecutionNode<?> parentToAddTo,
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Analyzes the given
Proof and his contained proof tree by
filling the start node SymbolicExecutionTreeBuilder.getStartNode()
with IExecutionNode s which are instantiated if a Node
in KeY's proof tree applies a rule of symbolic execution. |
protected static void |
TruthValueTracingUtil.analyzeTacletGoal(Node parent,
TacletApp tacletApp,
TacletGoalTemplate tacletGoal,
java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> labels,
Services services,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Analyzes the given
TacletGoalTemplate . |
protected static Term |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
FormulaTermLabel label,
boolean antecedentRuleApplication,
TermBuilder tb)
Checks if new minor IDs are available.
|
protected static void |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available.
|
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 int |
AbstractUpdateExtractor.countOpenChildren(Node node)
Counts the number of open child
Node s. |
protected IExecutionNode<?>[] |
SymbolicExecutionTreeBuilder.createCallStack(Node node)
Computes the method call stack of the given
Node . |
protected AbstractExecutionNode<?> |
SymbolicExecutionTreeBuilder.createExecutionTreeModelRepresentation(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement)
Creates a new execution tree model representation (
IExecutionNode )
if possible for the given Node in KeY's proof tree. |
protected AbstractExecutionMethodReturn<?> |
SymbolicExecutionTreeBuilder.createMehtodReturn(AbstractExecutionNode<?> parent,
Node node,
SourceElement statement,
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions completions)
Creates an method return node.
|
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 ImmutableSet<Term> |
SymbolicLayoutExtractor.extractAppliedCutsSet(Node goalnode,
Node root)
Extracts the applied cut rules in the given
Node . |
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
Node node)
Searches the relevant after block
Map in the given once for the given Node . |
protected Node |
SymbolicExecutionTreeBuilder.findMethodCallNode(Node currentNode,
RuleApp ruleApp)
|
protected ImmutableList<Node> |
SymbolicExecutionTreeBuilder.findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
Node node) |
IExecutionNode<?> |
SymbolicExecutionTreeBuilder.getBestExecutionNode(Node proofNode)
Returns the best matching
IExecutionNode for the given proof Node
in the parent hierarchy. |
IExecutionNode<?> |
SymbolicExecutionTreeBuilder.getExecutionNode(Node proofNode)
Searches the
IExecutionNode which represents the given Node of KeY's proof tree. |
protected boolean |
SymbolicExecutionTreeBuilder.hasBranchCondition(Node node)
Checks if the given
Node has a branch condition. |
protected void |
SymbolicExecutionTreeBuilder.initMethodCallStack(Node root,
Services services)
This method initializes
#methodCallStack in case that the
initial Sequent contains MethodFrame s in its modality. |
protected void |
SymbolicExecutionTreeBuilder.initNewLoopBodyMethodCallStack(Node node)
This method initializes the method call stack of loop body modalities
with the values from the original call stack.
|
protected void |
SymbolicExecutionTreeBuilder.initNewMethodCallStack(Node currentNode,
PosInOccurrence childPIO)
Initializes a new method call stack.
|
protected void |
SymbolicExecutionTreeBuilder.initNewValidiityMethodCallStack(Node node)
This method initializes the method call stack of validity modalities
with the values from the original call stack.
|
protected boolean |
SymbolicExecutionTreeBuilder.isContained(ImmutableList<IExecutionNode<?>> list,
Node node)
Checks if one of the give
IExecutionNode s represents the given Node . |
protected boolean |
SymbolicExecutionTreeBuilder.isInImplicitMethod(Node node)
Checks if the given
Node handles something in an implicit method. |
protected boolean |
SymbolicExecutionTreeBuilder.isNotInImplicitMethod(Node node)
Checks if the given
Node is not in an implicit method. |
protected boolean |
AbstractUpdateExtractor.isParentReachedOnAllChildGoals(Node currentNode,
java.util.List<AbstractUpdateExtractor.NodeGoal> branchLeafs)
Checks if parent backward iteration on all given
AbstractUpdateExtractor.NodeGoal has
reached the given Node . |
java.util.Set<AbstractExecutionNode<?>> |
SymbolicExecutionTreeBuilder.prune(Node node)
Prunes the symbolic execution tree at the first
IExecutionNode in the parent hierarchy of the given
Node (including the Node itself). |
protected Node |
SymbolicExecutionTreeBuilder.searchPreviousSymbolicExecutionNode(Node node)
Searches the first node in the parent hierarchy (including the given node)
which executes a statement.
|
protected boolean |
SymbolicExecutionTreeBuilder.shouldPrune(Node node) |
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.updateAfterBlockMap(Node node,
RuleApp ruleApp)
Updates the after block maps when a symbolic execution tree node is detected.
|
protected void |
SymbolicExecutionTreeBuilder.updateCallStack(Node node,
SourceElement statement)
Updates the call stack (
#methodCallStack ) if the given Node
in KeY's proof tree is a method call. |
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIds(Node childNode,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if available. |
Modifier and Type | Method and Description |
---|---|
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.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
Node node)
Searches the relevant after block
Map in the given once for the given Node . |
protected ImmutableList<Node> |
SymbolicExecutionTreeBuilder.findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
Node node) |
protected ImmutableList<Node> |
SymbolicExecutionTreeBuilder.findMethodCallStack(java.util.Map<Node,ImmutableList<Node>> methodCallStack,
Node node) |
Constructor and Description |
---|
AbstractUpdateExtractor(Node node,
PosInOccurrence modalityPio)
Constructor.
|
BranchResult(Node leafNode,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results,
Term condition,
java.lang.String conditionString,
Name termLabelName)
Constructor.
|
ExecutionVariableExtractor(Node node,
PosInOccurrence modalityPio,
IExecutionNode<?> executionNode,
Term condition,
boolean simplifyConditions)
Constructor.
|
ExecutionVariableValuePair(ProgramVariable programVariable,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
ExecutionVariableValuePair(Term arrayIndex,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
ExecutionVariableValuePair(Term arrayStartIndex,
Term arrayEndIndex,
Term arrayRangeConstant,
Term parent,
Term value,
Term condition,
boolean stateMember,
Node goalNode)
Constructor.
|
ExtractedExecutionValue(IExecutionNode<?> parentNode,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
ExtractedExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term additionalCondition,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
Constructor.
|
NodeGoal(Node currentNode,
ImmutableList<Goal> startingGoals)
A reached child node during backward iteration.
|
SymbolicLayoutExtractor(Node node,
PosInOccurrence modalityPio,
boolean useUnicode,
boolean usePrettyPrinting,
boolean simplifyConditions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Node[] |
IExecutionBranchCondition.getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this
IExecutionBranchCondition . |
Node |
IExecutionElement.getProofNode()
Returns the
Node in KeY's proof tree which is represented by this execution tree node. |
Modifier and Type | Method and Description |
---|---|
protected Node |
ExecutionMethodReturn.findMethodReturnNode(Node node)
Searches from the given
Node the parent which applies
the rule "methodCallReturn" in the same modality. |
Node[] |
ExecutionBranchCondition.getMergedProofNodes()
Returns the branch condition nodes in KeY's proof tree
which are merged into this
IExecutionBranchCondition . |
Node |
AbstractExecutionElement.getProofNode()
Returns the
Node in KeY's proof tree which is represented by this execution tree node. |
Modifier and Type | Method and Description |
---|---|
void |
ExecutionBranchCondition.addMergedProofNode(Node node)
Adds a merged proof
Node . |
protected static LocationVariable |
ExecutionOperationContract.extractResultVariableFromPostBranch(Node node,
Services services)
Extracts the result variable from the given post branch.
|
protected Node |
ExecutionMethodReturn.findMethodReturnNode(Node node)
Searches from the given
Node the parent which applies
the rule "methodCallReturn" in the same modality. |
Constructor and Description |
---|
AbstractExecutionBlockStartNode(ITreeSettings settings,
Node proofNode)
Constructor.
|
AbstractExecutionElement(ITreeSettings settings,
Node proofNode)
Constructor.
|
AbstractExecutionMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
AbstractExecutionNode(ITreeSettings settings,
Node proofNode)
Constructor.
|
AbstractExecutionValue(ITreeSettings settings,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
AbstractExecutionVariable(ITreeSettings settings,
Node proofNode,
IProgramVariable programVariable,
IExecutionValue parentValue,
Term arrayIndex,
Term additionalCondition,
PosInOccurrence modalityPIO)
Constructor.
|
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable arrayProgramVariable,
Term additionalCondition)
Constructor.
|
ExecutionAuxiliaryContract(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionBranchCondition(ITreeSettings settings,
Node proofNode,
java.lang.String additionalBranchLabel)
Constructor.
|
ExecutionBranchStatement(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionConstraint(ITreeSettings settings,
Node proofNode,
PosInOccurrence modalityPIO,
Term term)
Constructor.
|
ExecutionExceptionalMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
ExecutionJoin(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionLoopCondition(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionLoopInvariant(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionLoopStatement(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionMethodCall(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionMethodReturn(ITreeSettings settings,
Node proofNode,
ExecutionMethodCall methodCall)
Constructor.
|
ExecutionMethodReturnValue(ITreeSettings settings,
Node proofNode,
PosInOccurrence modalityPIO,
Term returnValue,
Term condition)
Constructor.
|
ExecutionOperationContract(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionStart(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionStatement(ITreeSettings settings,
Node proofNode)
Constructor.
|
ExecutionTermination(ITreeSettings settings,
Node proofNode,
IProgramVariable exceptionVariable,
IExecutionTermination.TerminationKind terminationKind)
Constructor.
|
ExecutionValue(Node proofNode,
ExecutionVariable variable,
boolean valueUnknown,
Term value,
java.lang.String valueString,
java.lang.String typeString,
Term condition,
java.lang.String conditionString)
Constructor.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" child value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
Term arrayIndex,
ExecutionValue lengthValue,
Term additionalCondition)
Constructor for an array cell value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" value.
|
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 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.
|
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 |
---|---|
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 AbstractSlicer.SequentInfo |
AbstractSlicer.analyzeSequent(Node node,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the aliases specified by the updates of the current
Node
at the application PosInOccurrence and computes the current this reference. |
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 |
---|---|
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is exceeded.
|
protected void |
ExecutedSymbolicExecutionTreeNodesStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected void |
SymbolicExecutionBreakpointStopCondition.handleNodeLimitNotExceeded(int maxApplications,
long timeout,
Proof proof,
long startTime,
int countApplied,
Goal goal,
Node node,
RuleApp ruleApp,
java.lang.Integer executedNumberOfSetNodes)
Handles the state that the node limit is not exceeded.
|
protected boolean |
SymbolicExecutionBreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
protected boolean |
BreakpointStopCondition.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Checks if a breakpoint is hit.
|
void |
SymbolicExecutionGoalChooser.updateGoalList(Node node,
ImmutableList<Goal> newGoals)
The given node has become an internal node of the proof tree, and the
children of the node are the given goals
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
AbstractConditionalBreakpoint.conditionMet(RuleApp ruleApp,
Proof proof,
Node node)
Checks if the condition, that was given by the user, evaluates to true with the current of the proof
|
protected boolean |
KeYWatchpoint.conditionMet(RuleApp ruleApp,
Proof proof,
Node node) |
protected boolean |
AbstractHitCountBreakpoint.hitcountExceeded(Node node)
Checks if the Hitcount is exceeded for the given
JavaLineBreakpoint . |
boolean |
AbstractHitCountBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
AbstractConditionalBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
SymbolicExecutionExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
ExceptionBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
FieldWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
IBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node)
Determines if the breakpoint represented by this BreakpointStopConition is triggered.
|
boolean |
KeYWatchpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
MethodBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
boolean |
LineBreakpoint.isBreakpointHit(SourceElement activeStatement,
RuleApp ruleApp,
Proof proof,
Node node) |
protected abstract boolean |
AbstractConditionalBreakpoint.isInScope(Node node)
Checks if the statement of a given
Node is in the scope of this breakpoint. |
protected boolean |
KeYWatchpoint.isInScope(Node node) |
protected boolean |
MethodBreakpoint.isInScope(Node node) |
protected boolean |
LineBreakpoint.isInScope(Node node) |
protected abstract boolean |
AbstractConditionalBreakpoint.isInScopeForCondition(Node node)
Checks if the statement of a given
Node is in the scope of this breakpoint. |
protected boolean |
KeYWatchpoint.isInScopeForCondition(Node node) |
protected boolean |
MethodBreakpoint.isInScopeForCondition(Node node) |
protected boolean |
LineBreakpoint.isInScopeForCondition(Node node) |
boolean |
SymbolicExecutionExceptionBreakpoint.isParentNode(Node node,
Node parent)
Checks if the given node is a parent of the other given node.
|
boolean |
ExceptionBreakpoint.isParentNode(Node node,
Node parent)
Checks if the given node is a parent of the other given node.
|
protected void |
AbstractConditionalBreakpoint.refreshVarMaps(RuleApp ruleApp,
Node node)
Modifies toKeep and variableNamingMap to hold the correct parameters after execution of the given ruleApp on the given node
|
Modifier and Type | Method and Description |
---|---|
static Node |
SymbolicExecutionUtil.findMethodCallNode(Node node,
PosInOccurrence pio)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static Node |
SymbolicExecutionUtil.findParentSetNode(Node node)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node, RuleApp) ). |
Modifier and Type | Method and Description |
---|---|
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. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<IProgramVariable> |
SymbolicExecutionUtil.collectAllElementaryUpdateTerms(Node node)
Collects all
IProgramVariable used in ElementaryUpdate s. |
static ImmutableList<Goal> |
SymbolicExecutionUtil.collectGoalsInSubtree(Node node)
|
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 ImmutableList<Term> |
SymbolicExecutionUtil.computeRootElementaryUpdates(Node root)
Computes the initial
ElementaryUpdate s on the given root Node . |
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,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
IExecutionContext context,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractReturnVariableValueSequent(Services services,
TypeReference contextObjectType,
IProgramMethod contextMethod,
ReferencePrefix contextObject,
Node methodReturnNode,
Node methodCallEmptyNode,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the return value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractTermSequent(Services sideProofServices,
Node node,
PosInOccurrence pio,
Term additionalConditions,
Term term,
boolean keepUpdates)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static SymbolicExecutionUtil.SiteProofVariableValueInput |
SymbolicExecutionUtil.createExtractVariableValueSequent(Services services,
Node node,
PosInOccurrence pio,
Term additionalConditions,
IProgramVariable variable)
Creates a
Sequent which can be used in site proofs to
extract the value of the given IProgramVariable from the
sequent of the given Node . |
static NotationInfo |
SymbolicExecutionUtil.createNotationInfo(Node node)
Creates the
NotationInfo for the given Node . |
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term newSuccedent)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorTerm(Node node,
Operator operator)
|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorValue(Node node,
Operator operator)
|
static Node |
SymbolicExecutionUtil.findMethodCallNode(Node node,
PosInOccurrence pio)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static Node |
SymbolicExecutionUtil.findParentSetNode(Node node)
Searches for the given
Node the parent node
which also represents a symbolic execution tree node
(checked via SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node, RuleApp) ). |
static IProgramVariable |
SymbolicExecutionUtil.findSelfTerm(Node node,
PosInOccurrence pio)
|
static boolean |
SymbolicExecutionUtil.hasLoopCondition(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given
Node has a loop condition. |
static Term |
SymbolicExecutionUtil.instantiateTerm(Node node,
Term term,
TacletApp tacletApp,
Services services)
|
static boolean |
SymbolicExecutionUtil.isBlockSpecificationElement(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as block/loop contract.
|
static boolean |
SymbolicExecutionUtil.isBranchStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as branch statement.
|
static boolean |
SymbolicExecutionUtil.isDoWhileLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a do while loop. |
static boolean |
SymbolicExecutionUtil.isExceptionalMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as exceptional method return.
|
static boolean |
SymbolicExecutionUtil.isForLoopCondition(Node node,
SourceElement statement)
Checks if the given
SourceElement is a for loop. |
static boolean |
SymbolicExecutionUtil.isInImplicitMethod(Node node,
RuleApp ruleApp)
Checks if the currently executed code is in an implicit method
(
IProgramMethod.isImplicit() is true ). |
static boolean |
SymbolicExecutionUtil.isLoopBodyTermination(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop body termination.
|
static boolean |
SymbolicExecutionUtil.isLoopInvariant(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as loop invariant.
|
static boolean |
SymbolicExecutionUtil.isLoopStatement(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as loop statement.
|
static boolean |
SymbolicExecutionUtil.isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement)
Checks if the given node should be represented as method call.
|
static boolean |
SymbolicExecutionUtil.isMethodCallNode(Node node,
RuleApp ruleApp,
SourceElement statement,
boolean allowImpliciteMethods)
Checks if the given node should be represented as method call.
|
static boolean |
SymbolicExecutionUtil.isMethodReturnNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as method return.
|
static boolean |
SymbolicExecutionUtil.isNotNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
SymbolicExecutionUtil.isNull(Node node,
Term additionalAntecedent,
Term newSuccedent)
|
static boolean |
SymbolicExecutionUtil.isOperationContract(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as operation contract.
|
static boolean |
SymbolicExecutionUtil.isStatementNode(Node node,
RuleApp ruleApp,
SourceElement statement,
PositionInfo posInfo)
Checks if the given node should be represented as statement.
|
static boolean |
SymbolicExecutionUtil.isSymbolicExecutionTreeNode(Node node,
RuleApp ruleApp)
|
static boolean |
SymbolicExecutionUtil.isTerminationNode(Node node,
RuleApp ruleApp)
Checks if the given node should be represented as termination.
|
static Sort |
SymbolicExecutionUtil.lazyComputeExceptionSort(Node node,
IProgramVariable exceptionVariable)
Computes the exception
Sort lazily when #getExceptionSort()
is called the first time. |
static boolean |
SymbolicExecutionUtil.lazyComputeIsAdditionalBranchVerified(Node node)
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
static boolean |
SymbolicExecutionUtil.lazyComputeIsExceptionalTermination(Node node,
IProgramVariable exceptionVariable)
Checks if is an exceptional termination.
|
static boolean |
SymbolicExecutionUtil.lazyComputeIsMainBranchVerified(Node node)
Checks if this branch would be closed without the uninterpreted predicate
and thus be treated as valid/closed in a regular proof.
|
static Term |
SymbolicExecutionUtil.posInOccurrenceInOtherNode(Node original,
PosInOccurrence pio,
Node toApplyOn)
Returns the
Term described by the given PosInOccurrence of the original Node
in the Node to apply on. |
static PosInOccurrence |
SymbolicExecutionUtil.posInOccurrenceToOtherSequent(Node original,
PosInOccurrence pio,
Node toApplyTo)
Returns the
PosInOccurrence described by the given PosInOccurrence of the original Node
in the Node to apply too. |
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 . |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
TestCaseGenerator.generateJUnitTestCase(Model m,
Node n) |
protected java.util.Map<java.lang.String,Sort> |
TestCaseGenerator.generateTypeInferenceMap(Node n) |
Modifier and Type | Method and Description |
---|---|
void |
MediatorProofControl.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc)
|
Modifier and Type | Method and Description |
---|---|
protected Node |
NodePreorderIterator.getNextOnParent(Node node)
Returns the next element to select if all children of the given
Node are visited. |
protected Node |
SearchNodeReversePreorderIterator.lastLeaf(Node node)
Returns the last leaf node.
|
Node |
NodePreorderIterator.next()
Returns the next
Node in the containment hierarchy. |
Node |
SearchNodePreorderIterator.next()
Returns the next
Node in the containment hierarchy. |
Node |
SearchNodeReversePreorderIterator.previous()
Returns the next
Node in the containment hierarchy. |
Modifier and Type | Method and Description |
---|---|
static ProgramVariable |
MiscTools.findActualVariable(ProgramVariable originalVar,
Node node)
Returns the actual variable for a given one (this means it returns the renamed variable).
|
protected Node |
NodePreorderIterator.getNextOnParent(Node node)
Returns the next element to select if all children of the given
Node are visited. |
static java.lang.String |
MiscTools.getRuleDisplayName(Node node)
Returns the display name of the applied rule in the given
Node of the proof tree in
KeY. |
static java.lang.String |
MiscTools.getRuleName(Node node)
Returns the name of the applied rule in the given
Node of the proof tree in KeY. |
protected Node |
SearchNodeReversePreorderIterator.lastLeaf(Node node)
Returns the last leaf node.
|
Constructor and Description |
---|
NodePreorderIterator(Node start)
Constructor.
|
SearchNodePreorderIterator(Node start)
Constructor.
|
SearchNodeReversePreorderIterator(Node start)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Node |
SymbolicExecutionStateWithProgCnt.getCorrespondingNode() |
Node |
SymbolicExecutionState.getCorrespondingNode() |
static Node |
MergeRuleUtils.getIntroducingNodeforLocVar(LocationVariable var,
Node node)
Finds the node, from the given leaf on, where the variable was
introduced.
|
Modifier and Type | Method and Description |
---|---|
static void |
MergeRuleUtils.closeMergePartnerGoal(Node mergeNodeParent,
Goal mergePartner,
PosInOccurrence pio,
SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Term pc,
java.util.Set<Name> newNames)
Closes the given partner goal, using the
CloseAfterMerge rule. |
static boolean |
MergeRuleUtils.equalsModBranchUniqueRenaming(SourceElement se1,
SourceElement se2,
Node node,
Services services)
An equals method that, before the comparison, replaces all program
locations in the supplied arguments by their branch-unique versions.
|
static LocationVariable |
MergeRuleUtils.getBranchUniqueLocVar(LocationVariable var,
Node startLeaf)
Find a location variable for the given one that is unique for the branch
corresponding to the given goal, but not necessarily globally unique.
|
static Node |
MergeRuleUtils.getIntroducingNodeforLocVar(LocationVariable var,
Node node)
Finds the node, from the given leaf on, where the variable was
introduced.
|
static SymbolicExecutionState |
MergeRuleUtils.sequentToSEPair(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C).
|
static SymbolicExecutionStateWithProgCnt |
MergeRuleUtils.sequentToSETriple(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C,p).
|
void |
SymbolicExecutionStateWithProgCnt.setCorrespondingNode(Node correspondingNode) |
void |
SymbolicExecutionState.setCorrespondingNode(Node correspondingNode) |
Constructor and Description |
---|
SymbolicExecutionState(Term symbolicState,
Term pathCondition,
Node correspondingNode) |
SymbolicExecutionStateWithProgCnt(Term symbolicState,
Term pathCondition,
Term programCounter,
Node correspondingNode) |
Modifier and Type | Method and Description |
---|---|
Node |
ProofExplorationService.applyChangeFormula(Goal g,
PosInOccurrence pio,
Term term,
Term newTerm) |
Node |
ProofExplorationService.soundAddition(Goal g,
Term t,
boolean antecedent)
Create a new Tacletapp that add a formula to the sequent using the cut rule and disabeling one of the branches
|
Modifier and Type | Method and Description |
---|---|
static ExplorationNodeData |
ExplorationNodeData.get(Node node) |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runMacro(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
void |
InteractionRecorder.runPrune(Node node) |
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runAutoMode(java.util.List<Node> initialGoals,
Proof proof,
ApplyStrategyInfo info) |
Modifier and Type | Method and Description |
---|---|
java.util.function.Function<Node,java.lang.String> |
LogPrinter.getMatchExpr() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
LogPrinter.getBranchingLabel(Node node) |
Modifier and Type | Method and Description |
---|---|
void |
LogPrinter.setMatchExpr(java.util.function.Function<Node,java.lang.String> matchExpr) |
Modifier and Type | Method and Description |
---|---|
Node |
NodeInteraction.getNode(Proof proof) |
Modifier and Type | Method and Description |
---|---|
java.util.Optional<Node> |
NodeIdentifier.findNode(Node node) |
java.util.Optional<Node> |
NodeIdentifier.findNode(Proof proof) |
Modifier and Type | Method and Description |
---|---|
java.util.Optional<Node> |
NodeIdentifier.findNode(Node node) |
static NodeIdentifier |
NodeIdentifier.get(Node node) |
Constructor and Description |
---|
MacroInteraction(Node node,
ProofMacro macro,
PosInOccurrence posInOcc,
ProofMacroFinishedInfo info) |
NodeInteraction(Node node) |
PruneInteraction(Node node) |
RuleInteraction(Node node,
RuleApp app) |
Constructor and Description |
---|
AutoModeInteraction(java.util.List<Node> initialNodes,
ApplyStrategyInfo info) |
Modifier and Type | Method and Description |
---|---|
static <T extends IBuiltInRuleApp> |
BuiltInRuleInteractionFactory.create(Node node,
T app) |
Constructor and Description |
---|
ContractBuiltInRuleInteraction(ContractRuleApp app,
Node node) |
LoopContractInternalBuiltInRuleInteraction(LoopContractInternalBuiltInRuleApp app,
Node node) |
LoopInvariantBuiltInRuleInteraction(LoopInvariantBuiltInRuleApp app,
Node node) |
MergeRuleBuiltInRuleInteraction(MergeRuleBuiltInRuleApp app,
Node node) |
OSSBuiltInRuleInteraction(OneStepSimplifierRuleApp app,
Node node) |
SMTBuiltInRuleInteraction(RuleAppSMT app,
Node node) |
UseDependencyContractBuiltInRuleInteraction(UseDependencyContractApp app,
Node node) |
Copyright © 2003-2019 The KeY-Project.