1 files changed, 43 insertions, 0 deletions
diff --git a/test/Analysis/z3-crosscheck.c b/test/Analysis/z3-crosscheck.c
new file mode 100644
index 0000000000000..67d410434fbb0
--- /dev/null
+++ b/test/Analysis/z3-crosscheck.c
@@ -0,0 +1,43 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+      return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+      return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+    c = 0;
+  if (a != b)
+    g(3 / c); // no-warning
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+    z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+    h(1);
+  } else {
+    h(2);
+  }
+}