mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

[TravisCI] Workaround slow unit test execution for Debug builds.

Browse source 
Unit tests execute very slowly in Debug (i.e. unoptimized) builds.  This
causes TravisCI to terminate the job due to no console output being
seen.

To workaround this for the debug builds the tests are just compiled
but not executed. To implement this the `RUN_UNIT_TESTS` environment
variable now can take on the values `BUILD_ONLY`, `BUILD_AND_RUN`,
and `SKIP` rather than `0` or `1`.
This commit is contained in:
Dan Liew 2017-10-06 11:23:44 +01:00
parent 0633d5819f
commit d47aea3987
4 changed files with 38 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
contrib/ci/README.md
View file

@ -31,7 +31,7 @@ the future.
* `NO_SUPPRESS_OUTPUT` - Don't suppress output of some commands (`0` or `1`)
* `PYTHON_BINDINGS` - Build and test Python API bindings (`0` or `1`)
* `RUN_SYSTEM_TESTS` - Run system tests (`0` or `1`)
* `RUN_UNIT_TESTS` - Run unit tests (`0` or `1`)
* `RUN_UNIT_TESTS` - Run unit tests (`BUILD_ONLY` or `BUILD_AND_RUN` or `SKIP`)
* `TARGET_ARCH` - Target architecture (`x86_64` or `i686`)
* `TEST_INSTALL` - Test running `install` target (`0` or `1`)
* `UBSAN_BUILD` - Do [UndefinedBehaviourSanitizer](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html) build (`0` or `1`)

2
contrib/ci/scripts/ci_defaults.sh
View file

@ -10,7 +10,7 @@ export JAVA_BINDINGS="${JAVA_BINDINGS:-1}"
export NO_SUPPRESS_OUTPUT="${NO_SUPPRESS_OUTPUT:-0}"
export PYTHON_BINDINGS="${PYTHON_BINDINGS:-1}"
export RUN_SYSTEM_TESTS="${RUN_SYSTEM_TESTS:-1}"
export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-1}"
export RUN_UNIT_TESTS="${RUN_UNIT_TESTS:-BUILD_AND_RUN}"
export TARGET_ARCH="${TARGET_ARCH:-x86_64}"
export TEST_INSTALL="${TEST_INSTALL:-1}"
export UBSAN_BUILD="${UBSAN_BUILD:-0}"

36
contrib/ci/scripts/test_z3_unit_tests_cmake.sh
View file

@ -10,17 +10,35 @@ set -o pipefail
: ${Z3_BUILD_DIR?"Z3_BUILD_DIR must be specified"}
: ${RUN_UNIT_TESTS?"RUN_UNIT_TESTS must be specified"}
if [ "X${RUN_UNIT_TESTS}" != "X1" ]; then
echo "Skipping unit tests"
exit 0
fi
# Set CMake generator args
source ${SCRIPT_DIR}/set_generator_args.sh
cd "${Z3_BUILD_DIR}"
# Build and run internal tests
cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
# Run all tests that don't require arguments
run_quiet ./test-z3 /a
function build_unit_tests() {
# Build internal tests
cmake --build $(pwd) --target test-z3 "${GENERATOR_ARGS[@]}"
}
function run_unit_tests() {
# Run all tests that don't require arguments
run_quiet ./test-z3 /a
}
case "${RUN_UNIT_TESTS}" in
BUILD_AND_RUN)
build_unit_tests
run_unit_tests
;;
BUILD_ONLY)
build_unit_tests
;;
SKIP)
echo "RUN_UNIT_TESTS set to \"${RUN_UNIT_TESTS}\" so skipping build and run"
exit 0
;;
*)
echo "Error: RUN_UNIT_TESTS set to unhandled value \"${RUN_UNIT_TESTS}\""
exit 1
;;
esac