From 20bf195f8a4da5e2e17c59b01b11da8917ee4a8c Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
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/svcomp32/Makefile | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 runtime/svcomp32/Makefile

(limited to 'runtime/svcomp32/Makefile')

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
-- 
cgit 1.4.1