[PATCH] D112621: [analyzer][solver] Introduce reasoning for not equal to operator

[Manas Gupta via Phabricator via cfe-commits]

manas added a comment.



In D112621#3949400 <https://reviews.llvm.org/D112621#3949400>, @steakhal wrote:

> `Analysis/constant-folding.c` seems to fail.
> Please run the `check-clang-analysis` build target to see what fails and investigate it.

@steakhal thank you for reviewing this! I investigated about the failing tests.

  // s1: [-3, -1], u1: [UINT_MAX - 3, UINT_MAX - 2]
  clang_analyzer_eval(u1 != s1); // expected-warning{{TRUE}}    # Line: 312
  
  // uch: [2, CHAR_MAX], sch: [SCHAR_MIN, 0]
  clang_analyzer_eval(uch != sch); // expected-warning{{TRUE}}  # Line: 406
  
  // ush: [2, USHRT_MAX], ssh: [SHRT_MIN, 0]
  clang_analyzer_eval(ush != ssh); // expected-warning{{TRUE}}  # Line: 422

Above tests are failing.

Previously, it was discussed that a good strategy is to "cast both [LHS and RHS] to the biggest type or unsigned one."

And for example, in the first failing test case, casting both rangesets,
`s1 = [-3,-1] -> [UINT_MAX-2, UINT_MAX]` and `u1 = [UINT_MAX-3, UINT_MAX-2] ->(unchanged) [UINT_MAX-3, UINT_MAX-2]`

`UINT_MAX -2` is overlapping  in both RangeSets.

Casting signed types to unsigned ones can leave us with overlapping values as shown above. Essentially, these tests were wrongly written. So, I am correcting these tests accordingly.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D112621/new/

https://reviews.llvm.org/D112621