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/Makefile | |
| 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/Makefile')
| -rw-r--r-- | runtime/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
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 |