From 8409a27a57a6fd4aad8828b0912c3afd39efb7e0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 11 Feb 2016 10:35:47 +0000 Subject: Try to fix the TravisCI build when using Z3 as the solver. The ``test/Feature/SolverTimeout.c`` test fails there. The error message I see in TravisCI is ``` Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc" Command 2 Result: -11 Command 2 Output: Command 2 Stderr: KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" KLEE: WARNING: undefined reference to function: printf KLEE: ERROR: (location information missing) divide by zero KLEE: NOTE: now ignoring this error at this location 0 klee 0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34 1 klee 0x0000000000da85c9 2 libpthread.so.0 0x00007fca19936cb0 3 libz3.so 0x00007fca19079826 4 librt.so.1 0x00007fca1747640c 5 libpthread.so.0 0x00007fca1992ee9a 6 libc.so.6 0x00007fca1776c38d clone + 109 ``` The issue appears to be racey as I had to run several copies of KLEE in parallel for the bug to occur using Z3 4.4.1. I managed to get a coredump and got the backtrace from gdb for the crash which is ``` #0 0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112 #1 0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63 #2 0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312 #3 0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111 ``` The crash appears to be in Z3 itself but I can't reproduce the issue when using the version of Z3 from the master branch. For now we simply workaround the issue by not running the ``test/Feature/SolverTimeout.c`` test when using Z3 as the solver. We should revisit this issue when another stable release of Z3 is made. --- test/Feature/SolverTimeout.c | 3 +++ 1 file changed, 3 insertions(+) (limited to 'test/Feature') diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c index 2ef6d413..aa86a856 100644 --- a/test/Feature/SolverTimeout.c +++ b/test/Feature/SolverTimeout.c @@ -1,6 +1,9 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t1.bc +// FIXME: This test occasionally fails when using Z3 4.4.1 but +// not when using Z3 from the master branch. So disable the test for now. +// REQUIRES: stp #include int main() { -- cgit 1.4.1