diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-14 17:55:07 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2017-01-14 21:37:19 +0000 |
commit | 3c8cb4600392675a34f2505f630523a494844d3d (patch) | |
tree | bbe0cf8b9d2e369175ad03020d7bdb47e9e11aa9 /runtime/Runtest | |
parent | 23e656156e4790a06a295d48932db53f2a582227 (diff) | |
download | klee-3c8cb4600392675a34f2505f630523a494844d3d.tar.gz |
Write tests to test `libkleeRuntest`. The `replay_posix_runtime.c`
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.
Diffstat (limited to 'runtime/Runtest')
-rw-r--r-- | runtime/Runtest/Makefile | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile index 666fe06d..82e21345 100644 --- a/runtime/Runtest/Makefile +++ b/runtime/Runtest/Makefile @@ -59,3 +59,14 @@ ifeq ($(HOST_OS), $(filter $(HOST_OS), Linux GNU GNU/kFreeBSD)) # Don't allow unresolved symbols. LLVMLibsOptions += -Wl,--no-undefined endif + +ifeq ($(HOST_OS), Linux) + # HACK: Setup symlinks that `ldconfig` would set up + # so that libkleeRuntest can be used from the build directory. + # This is needed to run tests. + sym_link_name := $(SharedLibDir)/$(SharedPrefix)$(LIBRARYNAME)$(SHLIBEXT).$(SHARED_VERSION) + +all:: $(LibName.SO) + $(Verb) [ ! -e "$(sym_link_name)" ] && ln -s $(LibName.SO) "$(sym_link_name)" || echo "" + +endif |