danix800 added a comment.
One of the observable issue with inconsistent size type is
void clang_analyzer_eval(int);
typedef unsigned long long size_t;
void *malloc(unsigned long size);
void free(void *);
void symbolic_longlong_and_int0(long long len) {
char *a = malloc(5);
(void)a[len + 1]; // no-warning
// len: [-1,3]
clang_analyzer_eval(-1 <= len && len <= 3); // expected-warning {{TRUE}}
clang_analyzer_eval(0 <= len); // expected-warning {{UNKNOWN}}
clang_analyzer_eval(len <= 2); // expected-warning {{UNKNOWN}}
free(a);
}
which is extracted from `clang/test/Analysis/array-bound-v2-constraint-check.c`,
with `DynamicMemoryModeling` turned on,
the second warning does not hold anymore: `clang_analyzer_eval(0 <= len);`
will be reported as `TRUE` which is not expected.
`DynamicMemoryModeling` will record the extent of allocated memory as `5ULL`,
`ArrayBoundV2` will do `len + 1 < 5ULL` assumption, simplified to `len < 4ULL`,
which casts `len` to unsigned, dropping `-1`, similar to
void clang_analyzer_eval(int);
void test(int len) {
if (len >= -1 && len <= 4U) { // len is promoted into unsigned, thus can
never be negative
clang_analyzer_eval(0 <= len); // TRUE
}
}
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D158499/new/
https://reviews.llvm.org/D158499
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
