[all-commits] [llvm/llvm-project] ac3edc: [analyzer][solver] Handle simplification to Concre...

[Gabor Marton via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: ac3edc5af09947210d8f8d25ddd7e42379ef6454
      https://github.com/llvm/llvm-project/commit/ac3edc5af09947210d8f8d25ddd7e42379ef6454
  Author: Gabor Marton <gabor.marton at ericsson.com>
  Date:   2021-10-14 (Thu, 14 Oct 2021)

  Changed paths:
    M clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
    M clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
    M clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
    A clang/test/Analysis/solver-sym-simplification-concreteint.c

  Log Message:
  -----------
  [analyzer][solver] Handle simplification to ConcreteInt

The solver's symbol simplification mechanism was not able to handle cases
when a symbol is simplified to a concrete integer. This patch adds the
capability.

E.g., in the attached lit test case, the original symbol is `c + 1` and
it has a `[0, 0]` range associated with it. Then, a new condition `c == 0`
is assumed, so a new range constraint `[0, 0]` comes in for `c` and
simplification kicks in. `c + 1` becomes `0 + 1`, but the associated
range is `[0, 0]`, so now we are able to realize the contradiction.

Differential Revision: https://reviews.llvm.org/D110913