Author: Balázs Benics Date: 2026-07-14T14:16:13+01:00 New Revision: c43967ca744ae2479987c1859df36fbb2fcf0866
URL: https://github.com/llvm/llvm-project/commit/c43967ca744ae2479987c1859df36fbb2fcf0866 DIFF: https://github.com/llvm/llvm-project/commit/c43967ca744ae2479987c1859df36fbb2fcf0866.diff LOG: [analyzer] Uplift UnSatAtErrorNodeDueToRefinedConstraint test after smarter range inference (#209443) Commit db28e48d67e3b0c44d88be9ea2d28eca2d239a9a taught `SymbolicRangeInferrer` to derive the range of `BO_Add`/`BO_Sub`/`BO_Mul` symbols from their operands via `inferFromCorners`. This broke `FalsePositiveRefutationBRVisitorTestBase.UnSatAtErrorNodeDueToRefinedConstraintNoReport`. The test relied on the analyzer not being able to bound `int y = x + n;` (with `x:[0,2]`, `n:[1,2]`), so that `reportIfCanBeTrue(y == 5)` created a false state that only the Z3 crosscheck could refute. Now the analyzer natively bounds y to `[1,4]`, proves `y == 5` infeasible, and never emits `CAN_BE_TRUE`, so the non-Z3 assertion lost its second line. Addition can never produce a gap (the sum of two intervals is a full interval), so the test's premise is no longer achievable with '+'. Switch to multiplication: for `x:[0,2]`, `n:[1,2]` the reachable products are `{0,1,2,4}`, but `inferFromCorners` over-approximates `x*n` to the contiguous range `[0,4]`. So `y == 3` is inside the inferred range (native manager returns `UNKNOWN -> CAN_BE_TRUE` emitted without Z3) yet is genuinely unreachable (Z3 refutes `x*n == 3` -> report invalidated with crosscheck). This restores the exact refutation-visitor mechanism the test exercises. Fixes up #209048. This issue would have been caught if we had a CI running Z3, like proposed in #184695. Assisted-by: Claude Opus 4.8 Added: Modified: clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp Removed: ################################################################################ diff --git a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp index 5d92cb906a154..0c73d8fa44b95 100644 --- a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp +++ b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp @@ -183,8 +183,10 @@ TEST_F(FalsePositiveRefutationBRVisitorTestBase, if (n >= 1 && n <= 2) { if (x >= 3) return; - // x: [0,2] and n: [1,2] - int y = x + n; // y: '(x+n)' Which is in approximately between 1 and 4. + // x: [0,2] and n: [1,2], so the reachable products of 'x*n' are + // {0,1,2,4}. The range manager cannot represent this gap and + // over-approximates the symbol '(x*n)' to the contiguous range [0,4]. + int y = x * n; // Registers the symbol 'y' with the constraint [1, MAX] in the true // branch. @@ -194,13 +196,14 @@ TEST_F(FalsePositiveRefutationBRVisitorTestBase, // SAT. Therefore that report is NOT invalidated. reachedWithNoContradiction(); // 'y' can be greater than zero. OK - // If we ask the analyzer whether the 'y' can be 5. It won't know, - // therefore, the state will be created where the 'y' expression is 5. + // If we ask the analyzer whether the 'y' can be 3. It won't know, + // because 3 is inside the over-approximated range [1,4], therefore + // the state will be created where the 'y' expression is 3. // Although, this assumption is false! - // 'y' can not be 5 if the maximal value of both x and n is 2. + // 'x*n' can not be 3 given x: [0,2] and n: [1,2]. // The BugPath which become UnSAT in the ErrorNode with a refined // constraint, should be invalidated. - reportIfCanBeTrue(y == 5); + reportIfCanBeTrue(y == 3); } } })"; _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
