Skip to content

Commit 2d550b9

Browse files
[Clang] Make Z3 Tests Work with Internal Shell
These tests were setting environment variables, which needs to be done explicitly with env when using the internal shell.
1 parent d86da4e commit 2d550b9

File tree

2 files changed

+14
-14
lines changed

2 files changed

+14
-14
lines changed

clang/test/Analysis/z3-crosscheck-max-attempts.cpp

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3,28 +3,28 @@
33
// RUN: | FileCheck %s --match-full-lines
44
// CHECK: crosscheck-with-z3-max-attempts-per-query = 3
55

6-
// DEFINE: %{mocked_clang} = \
7-
// DEFINE: LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \
8-
// DEFINE: %clang_analyze_cc1 %s \
9-
// DEFINE: -analyzer-config crosscheck-with-z3=true \
6+
// DEFINE: %{mocked_clang} = \
7+
// DEFINE: env LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \
8+
// DEFINE: %clang_analyze_cc1 %s \
9+
// DEFINE: -analyzer-config crosscheck-with-z3=true \
1010
// DEFINE: -analyzer-checker=core
1111

1212
// DEFINE: %{attempts} = -analyzer-config crosscheck-with-z3-max-attempts-per-query
1313

1414
// RUN: not %clang_analyze_cc1 %{attempts}=0 2>&1 | FileCheck %s --check-prefix=VERIFY-INVALID
1515
// VERIFY-INVALID: invalid input for analyzer-config option 'crosscheck-with-z3-max-attempts-per-query', that expects a positive value
1616

17-
// RUN: Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{attempts}=1 -verify=refuted
18-
// RUN: Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{attempts}=1 -verify=refuted
19-
// RUN: Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{attempts}=1 -verify=accepted
17+
// RUN: env Z3_SOLVER_RESULTS="UNDEF" %{mocked_clang} %{attempts}=1 -verify=refuted
18+
// RUN: env Z3_SOLVER_RESULTS="UNSAT" %{mocked_clang} %{attempts}=1 -verify=refuted
19+
// RUN: env Z3_SOLVER_RESULTS="SAT" %{mocked_clang} %{attempts}=1 -verify=accepted
2020

21-
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{attempts}=2 -verify=refuted
22-
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{attempts}=2 -verify=refuted
23-
// RUN: Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{attempts}=2 -verify=accepted
21+
// RUN: env Z3_SOLVER_RESULTS="UNDEF,UNDEF" %{mocked_clang} %{attempts}=2 -verify=refuted
22+
// RUN: env Z3_SOLVER_RESULTS="UNDEF,UNSAT" %{mocked_clang} %{attempts}=2 -verify=refuted
23+
// RUN: env Z3_SOLVER_RESULTS="UNDEF,SAT" %{mocked_clang} %{attempts}=2 -verify=accepted
2424

25-
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{attempts}=3 -verify=refuted
26-
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{attempts}=3 -verify=refuted
27-
// RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{attempts}=3 -verify=accepted
25+
// RUN: env Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNDEF" %{mocked_clang} %{attempts}=3 -verify=refuted
26+
// RUN: env Z3_SOLVER_RESULTS="UNDEF,UNDEF,UNSAT" %{mocked_clang} %{attempts}=3 -verify=refuted
27+
// RUN: env Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT" %{mocked_clang} %{attempts}=3 -verify=accepted
2828

2929

3030
// REQUIRES: z3, z3-mock, asserts, shell, system-linux

clang/test/Analysis/z3/D83660.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// RUN: Z3_SOLVER_RESULTS="SAT,SAT,SAT,SAT,UNDEF" \
1+
// RUN: env Z3_SOLVER_RESULTS="SAT,SAT,SAT,SAT,UNDEF" \
22
// RUN: LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \
33
// RUN: %clang_analyze_cc1 -analyzer-constraints=z3 \
44
// RUN: -analyzer-checker=core %s -verify

0 commit comments

Comments
 (0)