martong added a comment.
In D112621#3660256 <https://reviews.llvm.org/D112621#3660256>, @manas wrote:
> Considering @ASDenysPetrov 's example of `LHS = [1, 2] U [8, 9]` and `RHS =
> [5, 6]`, I constructed a test case as following:
>
> `(((u1 >= 1 && u1 <= 2) || (u1 >= 8 && u1 <= 9)) && u2 >= 5 && u2 <= 6)`
>
> but I can see that the analyzer is bifurcating paths at the OR operator.
> Essentially, there are two diverged paths:
>
> 1. `1 <= u1 && u1 <= 2 && 5 <= u2 && u2 <= 6`
>
> 2. `8 <= u1 && u1 <= 9 && 5 <= u2 && u2 <= 6`
>
> Separately, they hit `VisitBinaryOperator<BO_NE>` and in both cases, we get
> `TRUE` for `(u1 != u2)`.
>
> Is there any other way to formulate the expression so that it constructs `LHS
> = [1, 2] U [8, 9]` and doesn't bifurcate?
@manas, constrain into `[8, 9]` first and then pop out each intermediate
element. This should work:
void clang_analyzer_eval(bool);
template <typename T>
void clang_analyzer_value(T x);
extern void abort() __attribute__((__noreturn__));
#define assert(expr) ((expr) ? (void)(0) : abort())
void testDisequalityRules(unsigned int u1, unsigned int u2, unsigned int u3,
int s1, int s2, int s3, unsigned char uch,
signed char sch, short ssh, unsigned short ush) {
assert(1 <= u1 && u1 <= 9);
assert(u1 != 3);
assert(u1 != 4);
assert(u1 != 5);
assert(u1 != 6);
assert(u1 != 7);
clang_analyzer_value(u1); // expected-warning{{32u:{ [1, 2], [8, 9]
}}}
assert(5 <= u2 && u2 <= 6);
clang_analyzer_value(u2); // expected-warning{{32u:{ [5, 6] }}}
clang_analyzer_eval(u1 != u2); // expected-warning{{TRUE}}
}
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D112621/new/
https://reviews.llvm.org/D112621
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
