1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
// 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;
}
int unary(int x, long l)
{
int *z = 0;
int y = l;
if ((x & 1) && ((x & 1) ^ 1))
if (-y)
#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);
}
}
|
