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

   1 // RUN: %clang_analyze_cc1 %s \
   2 // RUN:   -analyzer-checker=core,debug.ExprInspection \
   3 // RUN:   -analyzer-config eagerly-assume=true \
   4 // RUN:   -verify
   5
   6 // RUN: %clang_analyze_cc1 %s \
   7 // RUN:   -analyzer-checker=core,debug.ExprInspection \
   8 // RUN:   -analyzer-config eagerly-assume=true \
   9 // RUN:   -analyzer-config support-symbolic-integer-casts=true \
  10 // RUN:   -verify
  11
  12 // RUN: %clang_analyze_cc1 %s \
  13 // RUN:   -analyzer-checker=core,debug.ExprInspection \
  14 // RUN:   -analyzer-config eagerly-assume=true \
  15 // RUN:   -analyzer-config crosscheck-with-z3=true \
  16 // RUN:   -verify
  17
  18 // RUN: %clang_analyze_cc1 %s \
  19 // RUN:   -analyzer-checker=core,debug.ExprInspection \
  20 // RUN:   -analyzer-config eagerly-assume=true \
  21 // RUN:   -analyzer-config crosscheck-with-z3=true \
  22 // RUN:   -analyzer-config support-symbolic-integer-casts=true \
  23 // RUN:   -verify
  24
  25 // REQUIRES: z3
  26
  27 void k(long L) {
  28   int g = L;
  29   int h = g + 1;
  30   int j;
  31   j += -h < 0; // should not crash
  32   // expected-warning@-1{{garbage}}
  33 }