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 34