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.

1 files changed, 62 insertions, 0 deletions

diff --git a/include/klee/klee_svcomp.h b/include/klee/klee_svcomp.h
new file mode 100644
index 00000000..27ca1404
--- /dev/null
+++ b/include/klee/klee_svcomp.h
@@ -0,0 +1,62 @@
+//===-- klee_svomp.h           ---------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+// This file declares the SV-COMP 2016 functions
+// as defined in http://sv-comp.sosy-lab.org/2016/rules.php
+
+#include "klee/klee.h"
+#include "stdint.h"
+
+/* Start SV-COMP specific type declarations
+ *
+ * Taken from ``ddv-machzwd/ddv_machzwd_all_false-unreach-call.i``. Not really
+ * sure if it's applicable everywhere.
+ */
+typedef long long loff_t;
+typedef unsigned long sector_t;
+struct __pthread_t_struct
+{
+      int id;
+};
+typedef struct __pthread_t_struct pthread_t;
+
+/* End SV-COMP specific type declarations */
+
+#define SVCOMP_NONDET_DECL_D(NAME,T) \
+  T __VERIFIER_nondet_ ## NAME();
+
+#define SVCOMP_NONDET_DECL(NAME) SVCOMP_NONDET_DECL_D(NAME,NAME)
+
+SVCOMP_NONDET_DECL_D(bool,_Bool)
+SVCOMP_NONDET_DECL(char)
+SVCOMP_NONDET_DECL(float)
+SVCOMP_NONDET_DECL(int)
+SVCOMP_NONDET_DECL(long)
+SVCOMP_NONDET_DECL(loff_t)
+SVCOMP_NONDET_DECL_D(pointer,void*)
+SVCOMP_NONDET_DECL_D(pchar,char*)
+SVCOMP_NONDET_DECL(pthread_t)
+SVCOMP_NONDET_DECL(sector_t)
+SVCOMP_NONDET_DECL(short)
+SVCOMP_NONDET_DECL(size_t)
+SVCOMP_NONDET_DECL_D(u32, uint32_t)
+SVCOMP_NONDET_DECL_D(uchar,unsigned char)
+SVCOMP_NONDET_DECL_D(uint, unsigned int)
+SVCOMP_NONDET_DECL_D(ulong, unsigned long)
+SVCOMP_NONDET_DECL(unsigned)
+SVCOMP_NONDET_DECL_D(ushort, unsigned short)
+
+#undef SVCOMP_NONDET_D_DECL
+#undef SVCOMP_NONDET_DECL
+
+void __VERIFIER_assume(int condition);
+void __VERIFIER_assert(int cond);
+__attribute__ ((__noreturn__)) void __VERIFIER_error();
+void __VERIFIER_atomic_begin();
+void __VERIFIER_atomic_end();