From 20bf195f8a4da5e2e17c59b01b11da8917ee4a8c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 17 Oct 2015 15:27:05 +0100 Subject: 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. --- runtime/svcomp64/Makefile | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 runtime/svcomp64/Makefile (limited to 'runtime/svcomp64/Makefile') diff --git a/runtime/svcomp64/Makefile b/runtime/svcomp64/Makefile new file mode 100644 index 00000000..40d44ec3 --- /dev/null +++ b/runtime/svcomp64/Makefile @@ -0,0 +1,32 @@ +#===-- 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=../.. + +# 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=kleeSVCOMPRuntime64 +else +# KLEE built against older versions of LLVM expects a library archive instead +BYTECODE_LIBRARY=1 +LIBRARYNAME=kleeSVCOMPRuntime64 +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 -m64 + +include $(LEVEL)/Makefile.common -- cgit 1.4.1