Interface | Description |
---|---|
SimultaneousVisitor |
TODO: Document.
|
Class | Description |
---|---|
JoinRuleUtils |
This class encapsulates static methods used in the JoinRule implementation.
|
JoinRuleUtils.CollectLocationVariablesVisitor |
Visitor for collecting program locations in a Java block.
|
JoinRuleUtils.CollectLocationVariablesVisitorHashSet |
Visitor for collecting program locations in a Java block.
|
JoinRuleUtils.LocVarReplBranchUniqueMap |
Map for renaming variables to their branch-unique names.
|
JoinRuleUtils.Option<T> |
A simple Scala-like option type: Either Some(value) or None.
|
JoinRuleUtils.Option.None<T> | |
JoinRuleUtils.Option.Some<T> | |
JoinRuleUtils.TermWrapper |
Simple term wrapper for comparing terms modulo renaming.
|
JoinRuleUtils.TermWrapperFactory |
Creates
JoinRuleUtils.TermWrapper objects, thereby ensuring
that equal term wrappers also have equal hash codes. |
ProgramVariablesMatchVisitor |
TODO: Document.
|
SimultaneousJavaASTVisitor |
Extends the JavaASTWalker to use the visitor mechanism.
|
SimultaneousJavaASTWalker |
Walks through the Java AST of two program elements simultaneously in
depth-left-fist-order at default.
|
SymbolicExecutionState |
A symbolic execution state is a pair of a symbolic state in form of a
parallel update, and a path condition in form of a JavaDL formula.
|
SymbolicExecutionStateWithProgCnt |
A symbolic execution state with program counter is a triple of a symbolic
state in form of a parallel update, a path condition in form of a JavaDL
formula, and a program counter in form of a JavaDL formula with non-empty
Java Block (and a possible post condition as first, and only, sub term).
|