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/klee-libc/memmove.c | |
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/klee-libc/memmove.c')
0 files changed, 0 insertions, 0 deletions