From f15766baee334b2d045e72b392712ef133c28c3a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 6 Oct 2017 15:56:43 +0100 Subject: [PATCH] [TravisCI] Don't run the non-native example when building with UBSan. This a workaround. Right now `libz3` gets linked against a static UBSan runtime which means none of the non-native language bindings (e.g. python) can load `libz3` due to undefined symbols. We need to link `libz3` against a shared UBSan runtime to fix this. --- contrib/ci/scripts/test_z3_examples_cmake.sh | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/contrib/ci/scripts/test_z3_examples_cmake.sh b/contrib/ci/scripts/test_z3_examples_cmake.sh index 1b8f988a2..c188dbcf4 100755 --- a/contrib/ci/scripts/test_z3_examples_cmake.sh +++ b/contrib/ci/scripts/test_z3_examples_cmake.sh @@ -14,6 +14,7 @@ set -o pipefail : ${PYTHON_EXECUTABLE?"PYTHON_EXECUTABLE must be specified"} : ${DOTNET_BINDINGS?"DOTNET_BINDINGS must be specified"} : ${JAVA_BINDINGS?"JAVA_BINDINGS must be specified"} +: ${UBSAN_BUILD?"UBSAN_BUILD must be specified"} # Set compiler flags source ${SCRIPT_DIR}/set_compiler_flags.sh @@ -45,6 +46,14 @@ run_quiet \ examples/c_maxsat_example_build_dir/c_maxsat_example \ ${Z3_SRC_DIR}/examples/maxsat/ex.smt +if [ "X${UBSAN_BUILD}" = "X1" ]; then + # FIXME: We really need libz3 to link against a shared UBSan runtime. + # Right now we link against the static runtime which breaks all the + # non-native language bindings. + echo "FIXME: Can't run other examples when building with UBSan" + exit 0 +fi + if [ "X${PYTHON_BINDINGS}" = "X1" ]; then # Run python examples