Clang Project

clang_source_code/test/Analysis/z3-crosscheck.c
1// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
2// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
3// REQUIRES: z3
4
5int foo(int x) 
6{
7  int *z = 0;
8  if ((x & 1) && ((x & 1) ^ 1))
9#ifdef NO_CROSSCHECK
10      return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
11#else
12      return *z; // no-warning
13#endif
14  return 0;
15}
16
17void g(int d);
18
19void f(int *a, int *b) {
20  int c = 5;
21  if ((a - b) == 0)
22    c = 0;
23  if (a != b)
24    g(3 / c); // no-warning
25}
26
27_Bool nondet_bool();
28
29void h(int d) {
30  int x, y, k, z = 1;
31  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
32    z = 2 * z;
33  }
34}
35
36void i() {
37  _Bool c = nondet_bool();
38  if (c) {
39    h(1);
40  } else {
41    h(2);
42  }
43}
44