@@ -301,21 +301,27 @@ compareValueToThreshold(ProgramStateRef State, NonLoc Value, NonLoc Threshold,
301
301
// calling `evalBinOpNN`:
302
302
if (isNegative (SVB, State, Value) && isUnsigned (SVB, Threshold)) {
303
303
if (CheckEquality) {
304
- // negative_value == unsigned_value is always false
304
+ // negative_value == unsigned_threshold is always false
305
305
return {nullptr , State};
306
306
}
307
- // negative_value < unsigned_value is always false
307
+ // negative_value < unsigned_threshold is always true
308
308
return {State, nullptr };
309
309
}
310
310
if (isUnsigned (SVB, Value) && isNegative (SVB, State, Threshold)) {
311
- // unsigned_value == negative_value and unsigned_value < negative_value are
312
- // both always false
311
+ // unsigned_value == negative_threshold and
312
+ // unsigned_value < negative_threshold are both always false
313
313
return {nullptr , State};
314
314
}
315
- // FIXME: these special cases are sufficient for handling real-world
315
+ // FIXME: These special cases are sufficient for handling real-world
316
316
// comparisons, but in theory there could be contrived situations where
317
317
// automatic conversion of a symbolic value (which can be negative and can be
318
318
// positive) leads to incorrect results.
319
+ // NOTE: We NEED to use the `evalBinOpNN` call in the "common" case, because
320
+ // we want to ensure that assumptions coming from this precondition and
321
+ // assumptions coming from regular C/C++ operator calls are represented by
322
+ // constraints on the same symbolic expression. A solution that would
323
+ // evaluate these "mathematical" compariosns through a separate pathway would
324
+ // be a step backwards in this sense.
319
325
320
326
const BinaryOperatorKind OpKind = CheckEquality ? BO_EQ : BO_LT;
321
327
auto BelowThreshold =
0 commit comments