For the code below, the ArrayBoundCheckerV2 will add the constraint x < 100 after the buf[x] = 1, see https://reviews.llvm.org/D23112.
void test_assume_after_access(unsigned long x) {
int buf[100];
buf[x] = 1;
clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
}
What is the purpose for doing this?
why not add x >= 0 as well?
I used checkLocation(), same as ArrayBoundCheckerV2, in my own checker too. Due to the uncertain calling order, I got the wrong constraints on x in my own checker. That’s why I pay attention to this problem.
If ‘x’ is 100 or greater, it’d mean that undefined behavior has already occured, and it’s pointless to explore that path further.
Same with ‘x’ being less than 0, so the checker should have added that as well.
So i believe that this is a valid behavior. A similar approach is taken by, say, DivZeroChecker that refutes the “y == 0” patch after “x / y” is evaluated. NullDereferenceChecker also assumes that all dereferenced pointers are non-null.
If they can prove that the operation is indeed unsafe on the current path, then the assumption would fail, and these checkers would report a warning instead.
What sort of problem are you having with these assumptions? Why are they affecting your checker? With constraints it shouldn’t normally ever be an issue, because adding constraints doesn’t really “mutate” the program state, it just “clarifies” it.
Thanks for the explanation, Artem! Sorry for my mistaken! ArrayBoundCheckerV2 did add the Idx >= 0 constraint as well.
It make sense to me that add the constraints on the symbol according to the program semantic!
My problem can be explained by the following diagram. IMHO, the constraints should be added on x after the access really occurred, this request may be a bit picky.