about summary refs log tree commit diff homepage
path: root/runtime/Runtest
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2015-10-17 15:27:05 +0100
committerDan Liew <daniel.liew@imperial.ac.uk>2015-10-17 15:27:05 +0100
commit20bf195f8a4da5e2e17c59b01b11da8917ee4a8c (patch)
tree3dad6a75ba8687d792c19bb3daada8feceb0822f /runtime/Runtest
parent6b0082b01e60ea2361da401694ea5aa7f7a6e966 (diff)
downloadklee-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/Runtest')
0 files changed, 0 insertions, 0 deletions