]>
git.proxmox.com Git - mirror_ubuntu-focal-kernel.git/blob - tools/testing/selftests/rcutorture/formal/srcu-cbmc/tests/test_script.sh
3 # This script expects a mode (either --should-pass or --should-fail) followed by
4 # an input file. The script uses the following environment variables. The test C
5 # source file is expected to be named test.c in the directory containing the
8 # CBMC: The command to run CBMC. Default: cbmc
9 # CBMC_FLAGS: Additional flags to pass to CBMC
10 # NR_CPUS: Number of cpus to run tests with. Default specified by the test
11 # SYNC_SRCU_MODE: Choose implementation of synchronize_srcu. Defaults to simple.
12 # kernel: Version included in the linux kernel source.
13 # simple: Use try_check_zero directly.
15 # The input file is a script that is sourced by this file. It can define any of
16 # the following variables to configure the test.
18 # test_cbmc_options: Extra options to pass to CBMC.
19 # min_cpus_fail: Minimum number of CPUs (NR_CPUS) for verification to fail.
20 # The test is expected to pass if it is run with fewer. (Only
21 # useful for .fail files)
22 # default_cpus: Quantity of CPUs to use for the test, if not specified on the
23 # command line. Default: Larger of 2 and MIN_CPUS_FAIL.
27 if test "$#" -ne 2; then
28 echo "Expected one option followed by an input file" 1>&2
32 if test "x$1" = "x--should-pass"; then
34 elif test "x$1" = "x--should-fail"; then
37 echo "Unrecognized argument '$1'" 1>&2
39 # Exit code 99 indicates a hard error.
45 SYNC_SRCU_MODE
=${SYNC_SRCU_MODE:-simple}
47 case ${SYNC_SRCU_MODE} in
48 kernel
) sync_srcu_mode_flags
="" ;;
49 simple
) sync_srcu_mode_flags
="-DUSE_SIMPLE_SYNC_SRCU" ;;
52 echo "Unrecognized argument '${SYNC_SRCU_MODE}'" 1>&2
59 c_file
=`dirname "$2"`/test.c
61 # Source the input file.
64 if test ${min_cpus_fail} -gt 2; then
65 default_default_cpus
=${min_cpus_fail}
67 default_default_cpus
=2
69 default_cpus
=${default_cpus:-${default_default_cpus}}
70 cpus
=${NR_CPUS:-${default_cpus}}
72 # Check if there are two few cpus to make the test fail.
73 if test $cpus -lt ${min_cpus_fail:-0}; then
77 cbmc_opts
="-DNR_CPUS=${cpus} ${sync_srcu_mode_flags} ${test_cbmc_options} ${CBMC_FLAGS}"
79 echo "Running CBMC: ${CBMC} ${cbmc_opts} ${c_file}"
80 if ${CBMC} ${cbmc_opts} "${c_file}"; then
81 # Verification successful. Make sure that it was supposed to verify.
82 test "x
${should_pass}" = xyes
86 # An exit status of 10 indicates a failed verification.
87 # (see cbmc_parse_optionst::do_bmc in the CBMC source code)
88 if test ${cbmc_exit_status} -eq 10 && test "x
${should_pass}" = xno; then
91 echo "CBMC returned
${cbmc_exit_status} exit status
" 1>&2
93 # Parse errors have exit status 6. Any other type of error
94 # should be considered a hard error.
95 if test ${cbmc_exit_status} -ne 6 && \
96 test ${cbmc_exit_status} -ne 10; then