[Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

Since the range-based constraint manager (default) is weak in handling comparisons where symbols are on both sides it is wise to rearrange them to have symbols only on the left side. Thus e.g. A + n >= B + m becomes A - B >= m - n which enables the constraint manager to store a range m - n .. MAX_VALUE for the symbolic expression A - B. This can be used later to check whether e.g. A + k == B + l can be true, which is also rearranged to A - B == l - k so the constraint manager can check whether l - k is in the range (thus greater than or equal to m - n).

The restriction in this version is the the rearrangement happens only if both the symbols and the concrete integers are within the range [min/4 .. max/4] where min and max are the minimal and maximal values of their type.

The rearrangement is not enabled by default. It has to be enabled by using -analyzer-config aggressive-relational-comparison-simplification=true.

Co-author of this patch is Artem Dergachev (NoQ).

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

llvm-svn: 329780

3 files changed, 1007 insertions, 12 deletions

diff --git a/clang/test/Analysis/conditional-path-notes.c b/clang/test/Analysis/conditional-path-notes.c
index d842b7fc6ee..0ccf40f4cd1 100644
--- a/clang/test/Analysis/conditional-path-notes.c
+++ b/clang/test/Analysis/conditional-path-notes.c
@@ -78,6 +78,7 @@ void testDiagnosableBranchLogical(int a, int b) {
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
     // expected-note@-1 {{Taking true branch}}
+    // expected-note@-2 {{Assuming the condition is true}}
     *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
     // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:        </dict>
+// CHECK-NEXT:       </array>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>event</string>
+// CHECK-NEXT:      <key>location</key>
+// CHECK-NEXT:      <dict>
+// CHECK-NEXT:       <key>line</key><integer>79</integer>
+// CHECK-NEXT:       <key>col</key><integer>7</integer>
+// CHECK-NEXT:       <key>file</key><integer>0</integer>
+// CHECK-NEXT:      </dict>
+// CHECK-NEXT:      <key>ranges</key>
+// CHECK-NEXT:      <array>
+// CHECK-NEXT:        <array>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>7</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>11</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:        </array>
+// CHECK-NEXT:      </array>
+// CHECK-NEXT:      <key>depth</key><integer>0</integer>
+// CHECK-NEXT:      <key>extended_message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:      <key>message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>control</string>
+// CHECK-NEXT:      <key>edges</key>
+// CHECK-NEXT:       <array>
+// CHECK-NEXT:        <dict>
+// CHECK-NEXT:         <key>start</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:         <key>end</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1594,12 +1658,12 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:         <key>start</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1607,12 +1671,12 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1624,7 +1688,7 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:      <key>kind</key><string>event</string>
 // CHECK-NEXT:      <key>location</key>
 // CHECK-NEXT:      <dict>
-// CHECK-NEXT:       <key>line</key><integer>81</integer>
+// CHECK-NEXT:       <key>line</key><integer>82</integer>
 // CHECK-NEXT:       <key>col</key><integer>24</integer>
 // CHECK-NEXT:       <key>file</key><integer>0</integer>
 // CHECK-NEXT:      </dict>
@@ -1632,12 +1696,12 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:      <array>
 // CHECK-NEXT:        <array>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>5</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>26</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
@@ -1658,10 +1722,10 @@ void testNonDiagnosableBranchArithmetic(int a, int b) {
 // CHECK-NEXT:    <key>issue_hash_content_of_line_in_context</key><string>f56671e5f67c73abef619b56f7c29fa4</string>
 // CHECK-NEXT:   <key>issue_context_kind</key><string>function</string>
 // CHECK-NEXT:   <key>issue_context</key><string>testNonDiagnosableBranchArithmetic</string>
-// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>3</string>
+// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>4</string>
 // CHECK-NEXT:   <key>location</key>
 // CHECK-NEXT:   <dict>
-// CHECK-NEXT:    <key>line</key><integer>81</integer>
+// CHECK-NEXT:    <key>line</key><integer>82</integer>
 // CHECK-NEXT:    <key>col</key><integer>24</integer>
 // CHECK-NEXT:    <key>file</key><integer>0</integer>
 // CHECK-NEXT:   </dict>
diff --git a/clang/test/Analysis/explain-svals.cpp b/clang/test/Analysis/explain-svals.cpp
index ecb5af1f8ef..c1b5200eb8e 100644
--- a/clang/test/Analysis/explain-svals.cpp
+++ b/clang/test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@ void test_4(int x, int y) {
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re{{{{^\(argument 'x'\) \+ 1$}}}}
   clang_analyzer_explain(1 + y); // expected-warning-re{{{{^\(argument 'y'\) \+ 1$}}}}
-  clang_analyzer_explain(x + y); // expected-warning-re{{{{^unknown value$}}}}
+  clang_analyzer_explain(x + y); // expected-warning-re{{{{^\(argument 'x'\) \+ \(argument 'y'\)$}}}}
   clang_analyzer_explain(z); // expected-warning-re{{{{^undefined value$}}}}
   clang_analyzer_explain(&z); // expected-warning-re{{{{^pointer to local variable 'z'$}}}}
   clang_analyzer_explain(stat); // expected-warning-re{{{{^signed 32-bit integer '0'$}}}}
diff --git a/clang/test/Analysis/svalbuilder-rearrange-comparisons.c b/clang/test/Analysis/svalbuilder-rearrange-comparisons.c
new file mode 100644
index 00000000000..47366d24456
--- /dev/null
+++ b/clang/test/Analysis/svalbuilder-rearrange-comparisons.c
@@ -0,0 +1,931 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=debug.ExprInspection,core.builtin -analyzer-config aggressive-relational-comparison-simplification=true -verify %s
+
+void clang_analyzer_dump(int x);
+void clang_analyzer_eval(int x);
+
+void exit(int);
+
+#define UINT_MAX (~0U)
+#define INT_MAX (UINT_MAX & (UINT_MAX >> 1))
+
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+    unsigned int __line, __const char *__function)
+     __attribute__ ((__noreturn__));
+#define assert(expr) \
+  ((expr)  ? (void)(0)  : __assert_fail (#expr, __FILE__, __LINE__, __func__))
+
+int g();
+int f() {
+  int x = g();
+  // Assert that no overflows occur in this test file.
+  // Assuming that concrete integers are also within that range.
+  assert(x <= ((int)INT_MAX / 4));
+  assert(x >= -((int)INT_MAX / 4));
+  return x;
+}
+
+void compare_different_symbol_equal() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_same_symbol_equal() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_equal() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_int_equal() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less_or_equal() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less() {
+  int x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less() {
+  int x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less() {
+  int x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less() {
+  int x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less() {
+  int x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less() {
+  int x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less() {
+  int x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less() {
+  int x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less() {
+  int x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_same_symbol_less() {
+  int x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_int_less() {
+  int x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_int_less() {
+  int x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_right_int_less() {
+  int x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_right_int_less() {
+  int x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less() {
+  int x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less() {
+  int x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less() {
+  int x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less() {
+  int x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_different_symbol_equal_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 0}}
+}
+
+void compare_different_symbol_plus_left_int_equal_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_minus_left_int_equal_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_different_symbol_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 2}}
+}
+
+void compare_different_symbol_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) == 1}}
+}
+
+void compare_same_symbol_equal_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_equal_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_equal_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x == y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x == y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less_or_equal_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_or_equal_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_or_equal_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) >= 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) <= 1}}
+}
+
+void compare_same_symbol_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x <= y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_or_equal_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x <= y);
+  // expected-warning@-1{{TRUE}}
+}
+
+void compare_different_symbol_less_unsigned() {
+  unsigned x = f(), y = f();
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 0}}
+}
+
+void compare_different_symbol_plus_left_int_less_unsigned() {
+  unsigned x = f()+1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_minus_left_int_less_unsigned() {
+  unsigned x = f()-1, y = f();
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$9{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_different_symbol_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = f()+2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 2}}
+}
+
+void compare_different_symbol_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = f()-2;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 2}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 2}}
+}
+
+void compare_different_symbol_plus_left_plus_right_int_less_unsigned() {
+  unsigned x = f()+2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 1}}
+}
+
+void compare_different_symbol_plus_left_minus_right_int_less_unsigned() {
+  unsigned x = f()+2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$9{int}) - (conj_$2{int})) > 3}}
+}
+
+void compare_different_symbol_minus_left_plus_right_int_less_unsigned() {
+  unsigned x = f()-2, y = f()+1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 3}}
+}
+
+void compare_different_symbol_minus_left_minus_right_int_less_unsigned() {
+  unsigned x = f()-2, y = f()-1;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 2}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$9{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{((conj_$2{int}) - (conj_$9{int})) < 1}}
+}
+
+void compare_same_symbol_less_unsigned() {
+  unsigned x = f(), y = x;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_int_less_unsigned() {
+  unsigned x = f(), y = x;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_int_less_unsigned() {
+  unsigned x = f(), y = x;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  clang_analyzer_dump(x); // expected-warning{{conj_$2{int}}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_plus_left_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void compare_same_symbol_plus_left_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  ++x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_plus_right_int_less_unsigned() {
+  unsigned x = f(), y = x+1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) + 1}}
+  clang_analyzer_dump(x < y);
+  // expected-warning@-1{{Unknown}} // FIXME: Can this be simplified?
+}
+
+void compare_same_symbol_minus_left_minus_right_int_less_unsigned() {
+  unsigned x = f(), y = x-1;
+  --x;
+  clang_analyzer_dump(x); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_dump(y); // expected-warning{{(conj_$2{int}) - 1}}
+  clang_analyzer_eval(x < y);
+  // expected-warning@-1{{FALSE}}
+}
+
+void overflow(signed char n, signed char m) {
+  if (n + 0 > m + 0) {
+    clang_analyzer_eval(n - 126 == m + 3); // expected-warning{{UNKNOWN}}
+  }
+}