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/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'runtime/Makefile') diff --git a/runtime/Makefile b/runtime/Makefile index 7eb02d3f..c0cfd01e 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -14,8 +14,8 @@ LEVEL=.. # # List all of the subdirectories that we will compile. -# -PARALLEL_DIRS=Intrinsic klee-libc Runtest + +PARALLEL_DIRS=Intrinsic klee-libc Runtest svcomp32 svcomp64 include $(LEVEL)/Makefile.config -- cgit 1.4.1