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 . |