[PATCH] D47726: [Analyzer][Z3] Test fixes for Z3 constraint manager

Vlad Tsyrklevich via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Tue Jun 5 23:30:10 PDT 2018


This revision was automatically updated to reflect the committed changes.
Closed by commit rL334067: [Analyzer][Z3] Test fixes for Z3 constraint manager (authored by vlad.tsyrklevich, committed by ).
Herald added a subscriber: llvm-commits.

Repository:
  rL LLVM

https://reviews.llvm.org/D47726

Files:
  cfe/trunk/test/Analysis/PR24184.cpp
  cfe/trunk/test/Analysis/constant-folding.c
  cfe/trunk/test/Analysis/loop-unrolling.cpp
  cfe/trunk/test/Analysis/z3/enabled.c


Index: cfe/trunk/test/Analysis/PR24184.cpp
===================================================================
--- cfe/trunk/test/Analysis/PR24184.cpp
+++ cfe/trunk/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
 
Index: cfe/trunk/test/Analysis/z3/enabled.c
===================================================================
--- cfe/trunk/test/Analysis/z3/enabled.c
+++ cfe/trunk/test/Analysis/z3/enabled.c
@@ -0,0 +1,3 @@
+// REQUIRES: z3
+// RUN: echo %clang_analyze_cc1 | FileCheck %s
+// CHECK: -analyzer-constraints=z3
Index: cfe/trunk/test/Analysis/constant-folding.c
===================================================================
--- cfe/trunk/test/Analysis/constant-folding.c
+++ cfe/trunk/test/Analysis/constant-folding.c
@@ -108,7 +108,11 @@
   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;
Index: cfe/trunk/test/Analysis/loop-unrolling.cpp
===================================================================
--- cfe/trunk/test/Analysis/loop-unrolling.cpp
+++ cfe/trunk/test/Analysis/loop-unrolling.cpp
@@ -368,7 +368,11 @@
 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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D47726.150077.patch
Type: text/x-patch
Size: 2253 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20180606/f639aca2/attachment.bin>


More information about the llvm-commits mailing list