[all-commits] [llvm/llvm-project] c43967: [analyzer] Uplift UnSatAtErrorNodeDueToRefinedCons...

[Balázs Benics via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: c43967ca744ae2479987c1859df36fbb2fcf0866
      https://github.com/llvm/llvm-project/commit/c43967ca744ae2479987c1859df36fbb2fcf0866
  Author: Balázs Benics <benicsbalazs at gmail.com>
  Date:   2026-07-14 (Tue, 14 Jul 2026)

  Changed paths:
    M clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp

  Log Message:
  -----------
  [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



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications