]>
Commit | Line | Data |
---|---|---|
418b2977 | 1 | #!/bin/sh |
b2441318 | 2 | # SPDX-License-Identifier: GPL-2.0 |
418b2977 LR |
3 | |
4 | # This script expects a mode (either --should-pass or --should-fail) followed by | |
5 | # an input file. The script uses the following environment variables. The test C | |
6 | # source file is expected to be named test.c in the directory containing the | |
7 | # input file. | |
8 | # | |
9 | # CBMC: The command to run CBMC. Default: cbmc | |
10 | # CBMC_FLAGS: Additional flags to pass to CBMC | |
11 | # NR_CPUS: Number of cpus to run tests with. Default specified by the test | |
12 | # SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to simple. | |
13 | # kernel: Version included in the linux kernel source. | |
14 | # simple: Use try_check_zero directly. | |
15 | # | |
16 | # The input file is a script that is sourced by this file. It can define any of | |
17 | # the following variables to configure the test. | |
18 | # | |
19 | # test_cbmc_options: Extra options to pass to CBMC. | |
20 | # min_cpus_fail: Minimum number of CPUs (NR_CPUS) for verification to fail. | |
21 | # The test is expected to pass if it is run with fewer. (Only | |
22 | # useful for .fail files) | |
23 | # default_cpus: Quantity of CPUs to use for the test, if not specified on the | |
24 | # command line. Default: Larger of 2 and MIN_CPUS_FAIL. | |
25 | ||
26 | set -e | |
27 | ||
28 | if test "$#" -ne 2; then | |
29 | echo "Expected one option followed by an input file" 1>&2 | |
30 | exit 99 | |
31 | fi | |
32 | ||
33 | if test "x$1" = "x--should-pass"; then | |
34 | should_pass="yes" | |
35 | elif test "x$1" = "x--should-fail"; then | |
36 | should_pass="no" | |
37 | else | |
38 | echo "Unrecognized argument '$1'" 1>&2 | |
39 | ||
40 | # Exit code 99 indicates a hard error. | |
41 | exit 99 | |
42 | fi | |
43 | ||
44 | CBMC=${CBMC:-cbmc} | |
45 | ||
46 | SYNC_SRCU_MODE=${SYNC_SRCU_MODE:-simple} | |
47 | ||
48 | case ${SYNC_SRCU_MODE} in | |
49 | kernel) sync_srcu_mode_flags="" ;; | |
50 | simple) sync_srcu_mode_flags="-DUSE_SIMPLE_SYNC_SRCU" ;; | |
51 | ||
52 | *) | |
53 | echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2 | |
54 | exit 99 | |
55 | ;; | |
56 | esac | |
57 | ||
58 | min_cpus_fail=1 | |
59 | ||
60 | c_file=`dirname "$2"`/test.c | |
61 | ||
62 | # Source the input file. | |
63 | . $2 | |
64 | ||
65 | if test ${min_cpus_fail} -gt 2; then | |
66 | default_default_cpus=${min_cpus_fail} | |
67 | else | |
68 | default_default_cpus=2 | |
69 | fi | |
70 | default_cpus=${default_cpus:-${default_default_cpus}} | |
71 | cpus=${NR_CPUS:-${default_cpus}} | |
72 | ||
73 | # Check if there are two few cpus to make the test fail. | |
74 | if test $cpus -lt ${min_cpus_fail:-0}; then | |
75 | should_pass="yes" | |
76 | fi | |
77 | ||
78 | cbmc_opts="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}" | |
79 | ||
80 | echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}" | |
81 | if ${CBMC} ${cbmc_opts} "${c_file}"; then | |
82 | # Verification successful. Make sure that it was supposed to verify. | |
83 | test "x${should_pass}" = xyes | |
84 | else | |
85 | cbmc_exit_status=$? | |
86 | ||
87 | # An exit status of 10 indicates a failed verification. | |
88 | # (see cbmc_parse_optionst::do_bmc in the CBMC source code) | |
89 | if test ${cbmc_exit_status} -eq 10 && test "x${should_pass}" = xno; then | |
90 | : | |
91 | else | |
92 | echo "CBMC returned ${cbmc_exit_status} exit status" 1>&2 | |
93 | ||
94 | # Parse errors have exit status 6. Any other type of error | |
95 | # should be considered a hard error. | |
96 | if test ${cbmc_exit_status} -ne 6 && \ | |
97 | test ${cbmc_exit_status} -ne 10; then | |
98 | exit 99 | |
99 | else | |
100 | exit 1 | |
101 | fi | |
102 | fi | |
103 | fi |