mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

[TravisCI] Don't run the non-native example when building with UBSan.

Browse source 
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.
This commit is contained in:
Dan Liew 2017-10-06 15:56:43 +01:00
parent a9fcfc531b
commit f15766baee
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
contrib/ci/scripts/test_z3_examples_cmake.sh
View file

@ -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