32 lines · 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 %s4 5// REQUIRES: z36 7int accepting(int n) {8 if (n == 4) {9 n = n / (n-4); // expected-warning {{Division by zero}}10 }11 return n;12}13 14int rejecting(int n, int x) {15 // Let's make the path infeasible.16 if (2 < x && x < 5 && x*x == x*x*x) {17 // Have the same condition as in 'accepting'.18 if (n == 4) {19 n = x / (n-4); // no-warning: refuted20 }21 }22 return n;23}24 25// CHECK: 1 BugReporter - Number of times all reports of an equivalence class was refuted26// CHECK-NEXT: 1 BugReporter - Number of reports passed Z327// CHECK-NEXT: 1 BugReporter - Number of reports refuted by Z328 29// CHECK: 1 Z3CrosscheckOracle - Number of Z3 queries accepting a report30// CHECK-NEXT: 1 Z3CrosscheckOracle - Number of Z3 queries rejecting a report31// CHECK-NEXT: 2 Z3CrosscheckOracle - Number of Z3 queries done32