No such file libkleeRuntimePOSIX64_Debug+Asserts.bca

[h0pe-ay]

KLEE: NOTE: Using POSIX model: /usr/local/lib/klee/runtime/libkleeRuntimePOSIX64_Debug+Asserts.bca
KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/libkleeRuntimePOSIX64_Debug+Asserts.bca failed: No such file or directory

[MartinNowack]

Please post the output of ls /usr/local/lib/klee/runtime/.

[h0pe-ay]

Please post the output of ls /usr/local/lib/klee/runtime/.
libkleeRuntimeFortify32_Debug+Asserts.bca
libkleeRuntimeFortify32_Debug.bca
libkleeRuntimeFortify32_Release+Asserts.bca
libkleeRuntimeFortify32_Release.bca
libkleeRuntimeFortify32_Release+Debug+Asserts.bca
libkleeRuntimeFortify32_Release+Debug.bca
libkleeRuntimeFortify64_Debug+Asserts.bca
libkleeRuntimeFortify64_Debug.bca
libkleeRuntimeFortify64_Release+Asserts.bca
libkleeRuntimeFortify64_Release.bca
libkleeRuntimeFortify64_Release+Debug+Asserts.bca
libkleeRuntimeFortify64_Release+Debug.bca
libkleeRuntimeFreestanding32_Debug+Asserts.bca
libkleeRuntimeFreestanding32_Debug.bca
libkleeRuntimeFreestanding32_Release+Asserts.bca
libkleeRuntimeFreestanding32_Release.bca
libkleeRuntimeFreestanding32_Release+Debug+Asserts.bca
libkleeRuntimeFreestanding32_Release+Debug.bca
libkleeRuntimeFreestanding64_Debug+Asserts.bca
libkleeRuntimeFreestanding64_Debug.bca
libkleeRuntimeFreestanding64_Release+Asserts.bca
libkleeRuntimeFreestanding64_Release.bca
libkleeRuntimeFreestanding64_Release+Debug+Asserts.bca
libkleeRuntimeFreestanding64_Release+Debug.bca
libkleeRuntimeIntrinsic32_Debug+Asserts.bca
libkleeRuntimeIntrinsic32_Debug.bca
libkleeRuntimeIntrinsic32_Release+Asserts.bca
libkleeRuntimeIntrinsic32_Release.bca
libkleeRuntimeIntrinsic32_Release+Debug+Asserts.bca
libkleeRuntimeIntrinsic32_Release+Debug.bca
libkleeRuntimeIntrinsic64_Debug+Asserts.bca
libkleeRuntimeIntrinsic64_Debug.bca
libkleeRuntimeIntrinsic64_Release+Asserts.bca
libkleeRuntimeIntrinsic64_Release.bca
libkleeRuntimeIntrinsic64_Release+Debug+Asserts.bca
libkleeRuntimeIntrinsic64_Release+Debug.bca
libkleeRuntimeKLEELibc32_Debug+Asserts.bca
libkleeRuntimeKLEELibc32_Debug.bca
libkleeRuntimeKLEELibc32_Release+Asserts.bca
libkleeRuntimeKLEELibc32_Release.bca
libkleeRuntimeKLEELibc32_Release+Debug+Asserts.bca
libkleeRuntimeKLEELibc32_Release+Debug.bca
libkleeRuntimeKLEELibc64_Debug+Asserts.bca
libkleeRuntimeKLEELibc64_Debug.bca
libkleeRuntimeKLEELibc64_Release+Asserts.bca
libkleeRuntimeKLEELibc64_Release.bca
libkleeRuntimeKLEELibc64_Release+Debug+Asserts.bca
libkleeRuntimeKLEELibc64_Release+Debug.bca

[MartinNowack]

It looks like you didn't compile KLEE with POSIX support. Use the following additional flag for cmake -DENABLE_POSIX_RUNTIME=ON.

[h0pe-ay]

I have used the following additional flag for cmake -DENABLE_POSIX_RUNTIME=ON . But no new files are generated.

cmake
-DENABLE_POSIX_RUNTIME=ON
-DENABLE_KLEE_UCLIBC=ON
-DENABLE_KLEE_LIBCXX=ON
-DKLEE_LIBCXX_DIR=/usr/include/c++/9/libc++-install-90/libc++-install-100
-DKLEE_LIBCXX_INCLUDE_DIR=/usr/include/c++/9/libc++-install-90/libc++-install-100/include/c++/v1
-DENABLE_KLEE_EH_CXX=ON
-DKLEE_LIBCXXABI_SRC_DIR=/usr/include/c++/9/libc++-install-90/llvm-100/libcxxabi
-DKLEE_UCLIBC_PATH=/home/pwn/klee-uclibc-klee/
-DENABLE_UNIT_TESTS=ON
-DENABLE_SYSTEM_TESTS=ON
-DGTEST_SRC_DIR=/home/pwn/googletest-release-1.11.0
-DLLVM_CONFIG_BINARY=/usr/bin/llvm-config-10
-DLLVMCC=/usr/bin/clang-10
-DLLVMCXX=/usr/bin/clang++-10
-DCMAKE_C_COMPILER=clang
-DCMAKE_CXX_COMPILER=clang++
..

[MartinNowack]

You have to run make again. If that doesn't help, delete the build directory and run cmake and make again.

[h0pe-ay]

Thanks @MartinNowack The problem has been solved.