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

[LSan] Don't run c_maxsat_example with LeakSanitizer because

Browse source 
it contains leaks that the Z3 developers don't intend to fix.
This commit is contained in:
Dan Liew 2017-10-11 08:10:13 +01:00
parent f90fe928af
commit ff5df20deb
2 changed files with 20 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

13
contrib/ci/scripts/sanitizer_env.sh
View file

@ -8,8 +8,21 @@
if [ "X${ASAN_BUILD}" = "X1" ]; then
# Use suppression files
export LSAN_OPTIONS="print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/lsan.txt"
# NOTE: If you get bad stacktraces try using `fast_unwind_on_malloc=0`
# NOTE: `malloc_context_size` controls size of recorded stacktrace for allocations.
# If the reported stacktraces appear incomplete try increasing the value.
export ASAN_OPTIONS="malloc_context_size=100,print_suppressions=1,suppressions=${Z3_SRC_DIR}/contrib/suppressions/sanitizers/asan.txt"
: ${ASAN_SYMBOLIZER_PATH?"ASAN_SYMBOLIZER_PATH must be specified"}
# Run command without checking for leaks
function run_no_lsan() {
ASAN_OPTIONS="${ASAN_OPTIONS},detect_leaks=0" "${@}"
}
else
# In non-ASan build just run directly
function run_no_lsan() {
"${@}"
}
fi
if [ "X${UBSAN_BUILD}" = "X1" ]; then

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

@ -42,9 +42,13 @@ run_quiet examples/tptp_build_dir/z3_tptp5 -help
# Build an run c_maxsat_example
cmake --build $(pwd) --target c_maxsat_example "${GENERATOR_ARGS[@]}"
run_quiet \
examples/c_maxsat_example_build_dir/c_maxsat_example \
${Z3_SRC_DIR}/examples/maxsat/ex.smt
# FIXME: It is known that the maxsat example leaks memory and the
# the Z3 developers have stated this is "wontfix".
# See https://github.com/Z3Prover/z3/issues/1299
run_no_lsan \
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.