40cc4379cd
Before this commit the LIT test framework of the static analyzer had a
file called `analyzer_test.py` which implemented a tricky system for
selecting the constraint manager:
- (A) Test files without `REQUIRES: z3` were executed with the default
range-based constraint manager.
- (B) If clang was built with Z3 support _and_ `USE_Z3_SOLVER=1` was
passed to the test run, the test was executed with Z3 as the
constraint manager.
(There was support for executing the same RUN line twice if both
conditions were satisfied.)
Unfortunately, using Z3 as the constraint manager does not work in
practice (very slow and causes many crashes), so the (B) pathway became
unused (or was never truly used?) and became broken due to bit rot. (In
the CI bots the analyzer is built without Z3 support, so only the
pathway (A) is used.)
This commit removes `analyzer_test.py` (+ related logic in other build
files + the test `z3/enabled.c` which just tested that
`analyzer_test.py` is active), because it tries to implement a feature
that we don't need (only one constraint manager is functional) and its
code is so complicated and buggy that it isn't useful as a starting
point for future development.
The fact that this logic was broken implied that tests with `REQUIRES:
z3` were not executed during normal testing, so they were also affected
by bit rot. Unfortunately this also affected the tests of the
`z3-crosscheck` mode (aka Z3 refutation) which also depends on Z3 but
uses Z3 in a different way which is actually stable and functional.
In this commit I'm fixing most of the `REQUIRES: z3` tests that were
broken by straightforward issues. Two test files, `PR37855.c` and
`z3-crosscheck.c` were affected by more complex issues, so I marked them
as `XFAIL` for now. We're planning to fix them with follow-up commits in
the foreseeable future.
For additional background information see also the discourse thread
https://discourse.llvm.org/t/taking-ownership-of-clang-test-analysis/84689
34 lines
1.1 KiB
C
34 lines
1.1 KiB
C
// RUN: %clang_analyze_cc1 %s \
|
|
// RUN: -analyzer-checker=core,debug.ExprInspection \
|
|
// RUN: -analyzer-config eagerly-assume=true \
|
|
// RUN: -verify
|
|
|
|
// RUN: %clang_analyze_cc1 %s \
|
|
// RUN: -analyzer-checker=core,debug.ExprInspection \
|
|
// RUN: -analyzer-config eagerly-assume=true \
|
|
// RUN: -analyzer-config support-symbolic-integer-casts=true \
|
|
// RUN: -verify
|
|
|
|
// RUN: %clang_analyze_cc1 %s \
|
|
// RUN: -analyzer-checker=core,debug.ExprInspection \
|
|
// RUN: -analyzer-config eagerly-assume=true \
|
|
// RUN: -analyzer-config crosscheck-with-z3=true \
|
|
// RUN: -verify
|
|
|
|
// RUN: %clang_analyze_cc1 %s \
|
|
// RUN: -analyzer-checker=core,debug.ExprInspection \
|
|
// RUN: -analyzer-config eagerly-assume=true \
|
|
// RUN: -analyzer-config crosscheck-with-z3=true \
|
|
// RUN: -analyzer-config support-symbolic-integer-casts=true \
|
|
// RUN: -verify
|
|
|
|
// REQUIRES: z3
|
|
|
|
void k(long L) {
|
|
int g = L;
|
|
int h = g + 1;
|
|
int j;
|
|
j += -h < 0; // should not crash
|
|
// expected-warning@-1{{The left expression of the compound assignment uses uninitialized memory [core.uninitialized.Assign]}}
|
|
}
|