diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-10-17 15:27:05 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-10-17 15:27:05 +0100 |
| commit | 20bf195f8a4da5e2e17c59b01b11da8917ee4a8c (patch) | |
| tree | 3dad6a75ba8687d792c19bb3daada8feceb0822f /runtime/svcomp32 | |
| parent | 6b0082b01e60ea2361da401694ea5aa7f7a6e966 (diff) | |
| download | klee-20bf195f8a4da5e2e17c59b01b11da8917ee4a8c.tar.gz | |
Implemented SV-COMP 2016 runtime functions which can be activated with
the --svcomp-runtime flag. This is accompanied with a set of tests to check all the functions are callable. Due to the fact that the SV-COMP benchmark suite contains a mixture of i386 and x86_64 benchmarks it is necessary to compile the runtime functions twice, once for i386 and once for x86_64 and then link the right version in at runtime. An example function that is problematic is ``__VERIFIER_nondet_long()`` which is a different size on i386 and x86_64.
Diffstat (limited to 'runtime/svcomp32')
| -rw-r--r-- | runtime/svcomp32/Makefile | 36 | ||||
| l--------- | runtime/svcomp32/functions.c | 1 |
2 files changed, 37 insertions, 0 deletions
diff --git a/runtime/svcomp32/Makefile b/runtime/svcomp32/Makefile new file mode 100644 index 00000000..6f877690 --- /dev/null +++ b/runtime/svcomp32/Makefile @@ -0,0 +1,36 @@ +#===-- runtime/Intrinsic/Makefile --------------------------*- Makefile -*--===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +LEVEL=../.. + +# FIXME: This doesn't work. So we have to duplicate +# functions.c via a symlink +#SOURCES=../svcomp64/functions.c + +# Needed for LLVM version +include $(LEVEL)/Makefile.config + +ifeq ($(shell python -c "print($(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3)"), True) +# For these versions of LLVM KLEE expects kleeRuntimeIntrinsic to be a LLVM module rather than an archive +MODULE_NAME=kleeSVCOMPRuntime32 +else +# KLEE built against older versions of LLVM expects a library archive instead +BYTECODE_LIBRARY=1 +LIBRARYNAME=kleeSVCOMPRuntime32 +endif + +DONT_BUILD_RELINKED=1 +# Don't strip debug info from the module. +DEBUG_RUNTIME=1 +NO_PEDANTIC=1 +NO_BUILD_ARCHIVE=1 + +C.Flags += -fno-builtin -m32 + +include $(LEVEL)/Makefile.common diff --git a/runtime/svcomp32/functions.c b/runtime/svcomp32/functions.c new file mode 120000 index 00000000..5eba0694 --- /dev/null +++ b/runtime/svcomp32/functions.c @@ -0,0 +1 @@ +../svcomp64/functions.c \ No newline at end of file |