[PATCH] D140086: [analyzer][solver] Improve reasoning for not equal to operator

Wed Jan 4 16:24:38 PST 2023

manas added a comment.

In D140086#4010175 <https://reviews.llvm.org/D140086#4010175>, @steakhal wrote:

>> This test fails.
>>
>>   void testfoo(unsigned char u, signed int s) {
>>     if (u >= 253 && u <= 255 && s < INT_MAX - 2) {
>>       // u: [253, 254], s: [INT_MIN, INT_MAX - 2]
>>       clang_analyzer_eval(u != s); // expected-warning{{UNKNOWN}}
>>                                    // but returns TRUE
>>     }
>>   }
>
> I feel like we have something to talk about.
> When I do the review pro bono, I'd like to focus on higher-level issues and let the submitter deal with the smaller concerns.

I think there has been some miscommunication. When I mentioned the failing example, I didn't mean to leave/delegate the pending work.

Nonetheless, I fixed it by re-introducing bitwidth comparison. Here is a Z3 proof https://gist.github.com/weirdsmiley/a9917815e71e4ec09e076522df039841

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D140086