| Interface | Description |
|---|---|
| ParametricMergeProcedure |
A
MergeProcedure like MergeWithPredicateAbstraction which
cannot be applied without parameters being set beforehand. |
| UnparametricMergeProcedure |
A
MergeProcedure like MergeByIfThenElse which can be applied
without setting any parameters. |
| Class | Description |
|---|---|
| MergeByIfThenElse |
Rule that merges two sequents based on the if-then-else construction: If two
locations are assigned different values in the states, the value in the
merged state is chosen based on the path condition.
|
| MergeIfThenElseAntecedent |
Rule that merges two sequents based on the if-then-else construction: If two
locations are assigned different values in the states, the value in the
merged state is chosen based on the path condition.
|
| MergeTotalWeakening |
Rule that merges two sequents based on "total" weakening: Replacement of
symbolic state by an update setting every program variable to a fresh Skolem
constant, if the respective program variable does not evaluate to the same
value in both states - in this case, the original value is preserved (->
idempotency).
|
| MergeWithLatticeAbstraction |
Rule that merges two sequents based on a specified set of abstract domain
lattices.
|
| MergeWithPredicateAbstraction |
Rule that merges two sequents based on a lattice of user-defined predicates.
|
| MergeWithPredicateAbstractionFactory |
A factory class for
MergeWithPredicateAbstraction which is itself a
MergeProcedure. |