|
14 | 14 | // DEFINE: -analyzer-config crosscheck-with-z3=true \ |
15 | 15 | // DEFINE: -analyzer-checker=core |
16 | 16 |
|
17 | | -// DEFINE: %{retry} = -analyzer-config crosscheck-with-z3-max-attempts-per-query |
| 17 | +// DEFINE: %{attempts} = -analyzer-config crosscheck-with-z3-max-attempts-per-query |
18 | 18 |
|
19 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{retry}=0 -verify=refuted |
20 | | -// RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{retry}=0 -verify=refuted |
21 | | -// RUN: Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{retry}=0 -verify=accepted |
| 19 | +// RUN: not %clang_analyze_cc1 %{attempts}=0 2>&1 | FileCheck %s --check-prefix=VERIFY-INVALID |
| 20 | +// VERIFY-INVALID: invalid input for analyzer-config option 'crosscheck-with-z3-max-attempts-per-query', that expects a positive value |
22 | 21 |
|
23 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{retry}=1 -verify=refuted |
24 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{retry}=1 -verify=refuted |
25 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{retry}=1 -verify=accepted |
| 22 | +// RUN: Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{attempts}=1 -verify=refuted |
| 23 | +// RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{attempts}=1 -verify=refuted |
| 24 | +// RUN: Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{attempts}=1 -verify=accepted |
26 | 25 |
|
27 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{retry}=2 -verify=refuted |
28 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{retry}=2 -verify=refuted |
29 | | -// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{retry}=2 -verify=accepted |
| 26 | +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{attempts}=2 -verify=refuted |
| 27 | +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{attempts}=2 -verify=refuted |
| 28 | +// RUN: Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{attempts}=2 -verify=accepted |
| 29 | + |
| 30 | +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{attempts}=3 -verify=refuted |
| 31 | +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{attempts}=3 -verify=refuted |
| 32 | +// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{attempts}=3 -verify=accepted |
30 | 33 |
|
31 | 34 |
|
32 | 35 | // REQUIRES: z3, asserts, shell, system-linux |
|
0 commit comments