[Analyzer][Z3] Test fixes for Z3 constraint manager

Summary:
Since Z3 tests have been not been running [1] some tests needed to be
updated. I also added a regression test for [1].

[1] https://reviews.llvm.org/D47722

Reviewers: george.karpenkov, NoQ, ddcc

Reviewed By: george.karpenkov

Subscribers: mikhail.ramalho, dcoughlin, xazax.hun, szepet, zzheng, a.sidorin, cfe-commits

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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@334067 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/test/Analysis/PR24184.cpp b/test/Analysis/PR24184.cpp
index 1280334d4d6ad7e3ab19b6b2200f1b8c7fe445a8..bfc5ae6ea56b29881a913ee342e576f288b85dcb 100644 (file)
--- a/test/Analysis/PR24184.cpp
+++ b/test/Analysis/PR24184.cpp
@@ -1,3 +1,4 @@
+// UNSUPPORTED: z3
 // RUN: %clang_analyze_cc1 -w -analyzer-eagerly-assume -fcxx-exceptions -analyzer-checker=core -analyzer-checker=alpha.core.PointerArithm,alpha.core.CastToStruct -analyzer-max-loop 64 -verify %s
 // RUN: %clang_analyze_cc1 -w -analyzer-checker=core -analyzer-checker=cplusplus -fcxx-exceptions -analyzer-checker alpha.core.PointerArithm,alpha.core.CastToStruct -analyzer-max-loop 63 -verify %s
 

diff --git a/test/Analysis/constant-folding.c b/test/Analysis/constant-folding.c
index 8189868be2ec70addb22b5fb9f0d5aa66fba6d2f..e21d629e9a417e131d5685e53090496fbe696fb0 100644 (file)
--- a/test/Analysis/constant-folding.c
+++ b/test/Analysis/constant-folding.c
@@ -108,7 +108,11 @@ void testBitwiseRules(unsigned int a, int b) {
   clang_analyzer_eval((b | -2) == 0); // expected-warning{{FALSE}}
   clang_analyzer_eval((b | 10) == 0); // expected-warning{{FALSE}}
   clang_analyzer_eval((b | 0) == 0); // expected-warning{{UNKNOWN}}
+#ifdef ANALYZER_CM_Z3
+  clang_analyzer_eval((b | -2) >= 0); // expected-warning{{FALSE}}
+#else
   clang_analyzer_eval((b | -2) >= 0); // expected-warning{{UNKNOWN}}
+#endif
 
   // Check that dynamically computed constants also work.
   int constant = 1 << 3;

diff --git a/test/Analysis/loop-unrolling.cpp b/test/Analysis/loop-unrolling.cpp
index ce7ada8bd723f21141a535cf88d2b90d3bc5b1b2..b7375df38b695f22cfff5943804a362330dfa5db 100644 (file)
--- a/test/Analysis/loop-unrolling.cpp
+++ b/test/Analysis/loop-unrolling.cpp
@@ -368,7 +368,11 @@ int nested_inlined_unroll1() {
 int nested_inlined_no_unroll1() {
   int k;
   for (int i = 0; i < 9; i++) {
+#ifdef ANALYZER_CM_Z3
+    clang_analyzer_numTimesReached(); // expected-warning {{13}}
+#else
     clang_analyzer_numTimesReached(); // expected-warning {{15}}
+#endif
     k = simple_unknown_bound_loop();  // reevaluation without inlining, splits the state as well
   }
   int a = 22 / k; // no-warning

diff --git a/test/Analysis/z3/enabled.c b/test/Analysis/z3/enabled.c
new file mode 100644 (file)
index 0000000..9f44233
--- /dev/null
+++ b/test/Analysis/z3/enabled.c
@@ -0,0 +1,3 @@
+// REQUIRES: z3
+// RUN: echo %clang_analyze_cc1 | FileCheck %s
+// CHECK: -analyzer-constraints=z3