| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
`-O0` has to be used in conjunction with, not instead of
`-Xclang -disable-O0-optnone`
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
|
|
|
|
|
|
test is marked XFAIL because there is a bug in the implementation
of `libkleeRuntest`.
Quite a few changes had to be made to the lit configuration in
order to support these tests.
To run the tests I had to fix #480 for the autoconf/Makefile build
system otherwise the `libkleeRuntest` library would not be found
by the system linker at runtime.
|
|
``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.
|
|
- You can now make tests disabled, or expected to fail, by writing something like:
// XFAIL: llvm-3.4
or
// REQUIRES: not-llvm-3.4
- This mechanism doesn't support version comparisons, it is mostly intended to
help with switching over to new LLVM versions and incrementally working
through the test failures.
|
|
|
|
time.
|
|
are now broken and will be fixed shortly.
|
|
|
|
This is needed because the helper tool 'not' is used by some tests
|
|
- Not working yet.
Also, ditch a bunch of unused substitution variables from the site.exp config
file.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102872 91177308-0d34-0410-b5e6-96231b3b80d8
|
