[fix] klee-test-comp.c

UnitTestBot · Nov 3, 2023 · 5659782 · 5659782
1 parent 1b1e789
commit 5659782
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git 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
@@ -7,18 +7,19 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include <stdint.h>
 #ifdef EXTERNAL
 #include "klee.h"
 #include <assert.h>
 #include <stddef.h>
-#include <stdint.h>
 #include <stdlib.h>
 #else
 void klee_make_symbolic(void *addr, unsigned int nbytes, const char *name);
 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;