return St;
}
- // sym is not a constant, but it might be not-equal to a constant.
- // Observe: V >= sym is the same as sym <= V.
- // check: is sym != V?
- // check: is sym > V?
- // if both are true, the path is infeasible.
-
- if (isNotEqual(St, sym, V)) {
- // Is sym > V?
- //
- // We're not doing heavy range analysis yet, so all we can accurately
- // reason about are the edge cases.
- //
- // If V == 0, since we know that sym != V, we also know that sym > V.
- isFeasible = V != 0;
- }
- else
- isFeasible = true;
-
+ isFeasible = !isNotEqual(St, sym, V) ||
+ (V != llvm::APSInt::getMaxValue(V.getBitWidth(), V.isSigned()));
+
return St;
}
isFeasible = *X <= V;
return St;
}
-
- isFeasible = true;
+
+ isFeasible = !isNotEqual(St, sym, V) ||
+ (V != llvm::APSInt::getMinValue(V.getBitWidth(), V.isSigned()));
+
return St;
}
int* qux();
-int f9(int len) {
+int f9(unsigned len) {
assert (len != 0);
int *p = 0;
- for (int i = 0; i < len; ++i)
+ for (unsigned i = 0; i < len; ++i)
p = qux(i);
return *p++; // no-warning
}
-int f9b(int len) {
+int f9b(unsigned len) {
assert (len > 0); // note use of '>'
int *p = 0;
- for (int i = 0; i < len; ++i)
+ for (unsigned i = 0; i < len; ++i)
p = qux(i);
return *p++; // no-warning