diff --git a/CMakeLists.txt b/CMakeLists.txt index 7f6bcf26973..cad45136e74 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -643,6 +643,12 @@ unset(_flags) configure_file(${CMAKE_SOURCE_DIR}/include/klee/Config/config.h.cmin ${CMAKE_BINARY_DIR}/include/klee/Config/config.h) +################################################################################ +# Generate `klee/klee.h` and `klee-test-comp.c` +################################################################################ +configure_file(${CMAKE_SOURCE_DIR}/include/klee/klee.h ${CMAKE_BINARY_DIR}/include/klee/klee.h COPYONLY) +configure_file(${CMAKE_SOURCE_DIR}/include/klee-test-comp.c ${CMAKE_BINARY_DIR}/include/klee-test-comp.c COPYONLY) + ################################################################################ # Generate `CompileTimeInfo.h` ################################################################################ diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c index 90774aa2b22..413011abeaa 100644 --- a/include/klee-test-comp.c +++ b/include/klee-test-comp.c @@ -7,11 +7,11 @@ // //===----------------------------------------------------------------------===// +#include #ifdef EXTERNAL #include "klee.h" #include #include -#include #include #else void klee_make_symbolic(void *addr, unsigned int nbytes, const char *name); @@ -19,6 +19,7 @@ void klee_assume(_Bool condition); __attribute__((noreturn)) void klee_silent_exit(int status); void __assert_fail(const char *assertion, const char *file, unsigned int line, const char *function); +void klee_prefer_cex(void *, uintptr_t); #endif int __VERIFIER_nondet_int(void) { @@ -35,11 +36,13 @@ unsigned int __VERIFIER_nondet_uint(void) { return x; } +#ifdef __x86_64__ unsigned __int128 __VERIFIER_nondet_uint128(void) { unsigned __int128 x; klee_make_symbolic(&x, sizeof(x), "unsigned __int128"); return x; } +#endif unsigned __VERIFIER_nondet_unsigned(void) { unsigned x;