mirror of
https://github.com/Gericom/teak-llvm.git
synced 2025-06-19 11:35:51 -04:00
[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 llvm-svn: 334067
This commit is contained in:
parent
80a764bab1
commit
a7d25d5934
@ -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
|
||||
|
||||
|
@ -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;
|
||||
|
@ -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
|
||||
|
3
clang/test/Analysis/z3/enabled.c
Normal file
3
clang/test/Analysis/z3/enabled.c
Normal file
@ -0,0 +1,3 @@
|
||||
// REQUIRES: z3
|
||||
// RUN: echo %clang_analyze_cc1 | FileCheck %s
|
||||
// CHECK: -analyzer-constraints=z3
|
Loading…
Reference in New Issue
Block a user