Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution |
Modifier and Type | Method and Description |
---|---|
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 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<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.updateAfterBlockMap(Node node,
RuleApp ruleApp)
Updates the after block maps when a symbolic execution tree node is detected.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
SymbolicExecutionTreeBuilder.isAfterBlockReached(int currentStackSize,
MethodFrame currentInnerMostMethodFrame,
SourceElement currentActiveStatement,
SymbolicExecutionTreeBuilder.JavaPair expectedPair)
Checks if the after block condition is fulfilled.
|
Modifier and Type | Method and Description |
---|---|
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 . |
Copyright © 2003-2019 The KeY-Project.