steakhal added a comment.
I genuinely think that in the following case we should warn, since the user
already had a chance to express the range assumption using an `assert`.
I think that regardless which checker in what condition checks for a given
constraint.
If the expression is tainted, we should warn each cases if the constraint
cannot be proven.
If that is NOT tainted, we should conservatively assume that the precondition
is satisfied.
---
**PS**: after checking the exploded graph for the following example, I
recognized that the range based constraint solver is not smart enough to prove
that `x` must be in range.
Even if we express the necessary information using asserts.
I'm not so sure about warning for this case, after seeing this :|
int scanf(const char *restrict format, ...);
void clang_analyzer_eval(int);
extern void __assert_fail (__const char *__assertion, __const char *__file,
unsigned int __line, __const char *__function)
__attribute__ ((__noreturn__));
#define assert(expr) \
((expr) ? (void)(0) : __assert_fail (#expr, __FILE__, __LINE__, __func__))
void foo(int y, int z) {
assert(y <= 10);
assert(z >= 20);
int x;
scanf("%d", &x);
if (x < y || x > z)
return;
// x should be in range [10, 20]
clang_analyzer_eval(0 <= x && x < 256);
// we want to warn if x is not proven to be in that range
// mySink(x); // requires x to be in [0, 255]
}
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D73536/new/
https://reviews.llvm.org/D73536
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
