C++: Predicate factoring to prevent a bad standard order.

This commit is contained in:
Mathias Vorreiter Pedersen 2022-09-08 13:55:27 +01:00
Родитель 1d834799a2
Коммит f119b50c2f
1 изменённых файлов: 22 добавлений и 2 удалений

Просмотреть файл

@ -542,12 +542,32 @@ private predicate unequalIntegralSsa(
) {
exists(SemExpr e, int d1, int d2 |
unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
bounded(e, b, d2, true, _, _, _) and
bounded(e, b, d2, false, _, _, _) and
boundedUpper(e, b, d1) and
boundedLower(e, b, d2) and
delta = d2 + d1
)
}
/**
* Holds if `b + delta` is an upper bound for `e`.
*
* This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
*/
pragma[nomagic]
private predicate boundedUpper(SemExpr e, SemBound b, int delta) {
bounded(e, b, delta, true, _, _, _)
}
/**
* Holds if `b + delta` is a lower bound for `e`.
*
* This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`.
*/
pragma[nomagic]
private predicate boundedLower(SemExpr e, SemBound b, int delta) {
bounded(e, b, delta, false, _, _, _)
}
/** Weakens a delta to lie in the range `[-1..1]`. */
bindingset[delta, upper]
private int weakenDelta(boolean upper, int delta) {