clang/test/Analysis/unary-sym-expr-z3-refutation.c


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

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core,debug.ExprInspection \
// RUN:   -analyzer-config eagerly-assume=true \
// RUN:   -verify

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core,debug.ExprInspection \
// RUN:   -analyzer-config eagerly-assume=true \
// RUN:   -analyzer-config support-symbolic-integer-casts=true \
// RUN:   -verify

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core,debug.ExprInspection \
// RUN:   -analyzer-config eagerly-assume=true \
// RUN:   -analyzer-config crosscheck-with-z3=true \
// RUN:   -verify

// RUN: %clang_analyze_cc1 %s \
// RUN:   -analyzer-checker=core,debug.ExprInspection \
// RUN:   -analyzer-config eagerly-assume=true \
// RUN:   -analyzer-config crosscheck-with-z3=true \
// RUN:   -analyzer-config support-symbolic-integer-casts=true \
// RUN:   -verify

// REQUIRES: z3

void k(long L) {
  int g = L;
  int h = g + 1;
  int j;
  j += -h < 0; // should not crash
  // expected-warning@-1{{The left expression of the compound assignment uses uninitialized memory [core.uninitialized.Assign]}}
}