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.

1 files changed, 32 insertions, 0 deletions

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