Class | Description |
---|---|
JoinIfThenElse |
Rule that joins two sequents based on the if-then-else construction: If two
locations are assigned different values in the states, the value in the
joined state is chosen based on the path condition.
|
JoinIfThenElseAntecedent |
Rule that joins two sequents based on the if-then-else
construction: If two locations are assigned different
values in the states, the value in the joined state is
chosen based on the path condition.
|
JoinWeaken |
Rule that joins 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).
|
JoinWithLatticeAbstraction |
Rule that joins two sequents based on a specified set of abstract domain
lattices.
|
JoinWithSignLattice |
Rule that joins two sequents based on a sign lattice for integers.
|