clang/test/Analysis/z3/crosscheck-statistics.c

   1 // RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s  \
   2 // RUN:   -analyzer-config crosscheck-with-z3=true \
   3 // RUN:   -analyzer-stats 2>&1 | FileCheck %s
   4
   5 // REQUIRES: z3
   6
   7 // expected-error@1 {{Z3 refutation rate:1/2}}
   8
   9 int accepting(int n) {
  10   if (n == 4) {
  11     n = n / (n-4); // expected-warning {{Division by zero}}
  12   }
  13   return n;
  14 }
  15
  16 int rejecting(int n, int x) {
  17   // Let's make the path infeasible.
  18   if (2 < x && x < 5 && x*x == x*x*x) {
  19     // Have the same condition as in 'accepting'.
  20     if (n == 4) {
  21       n = x / (n-4); // no-warning: refuted
  22     }
  23   }
  24   return n;
  25 }
  26
  27 // CHECK:       1 BugReporter         - Number of times all reports of an equivalence class was refuted
  28 // CHECK-NEXT:  1 BugReporter         - Number of reports passed Z3
  29 // CHECK-NEXT:  1 BugReporter         - Number of reports refuted by Z3
  30
  31 // CHECK:       1 Z3CrosscheckOracle - Number of Z3 queries accepting a report
  32 // CHECK-NEXT:  1 Z3CrosscheckOracle - Number of Z3 queries rejecting a report
  33 // CHECK-NEXT:  2 Z3CrosscheckOracle - Number of Z3 queries done