From: Jiri Slaby Date: Fri, 17 Mar 2017 13:15:18 +0100 Subject: errno: define __errno_location Patch-mainline: no POSIX runtime library is built on my system with a reference to __errno_location(). And then it is undefined when klee is run --with-posix: KLEE: NOTE: Using model: lib/libkleeRuntimePOSIX.bca KLEE: output directory is "test/Runtime/POSIX/Output/Read1.c.tmp.klee-out" KLEE: Using STP solver backend KLEE: WARNING: undefined reference to function: __errno_location KLEE: WARNING ONCE: calling external: __errno_location() KLEE: ERROR: (location information missing) ASSERTION FAIL: x == -1 && errno == EFAULT KLEE: NOTE: now ignoring this error at this location EXITING ON ERROR: Error: ASSERTION FAIL: x == -1 && errno == EFAULT Stack: #000000170 in main (argc=4, argv=24928704) Therefore, the tests fail. Define __errno_location as a weak symbol to return the actual int errno. Signed-off-by: Jiri Slaby --- runtime/POSIX/errno_location.c | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 runtime/POSIX/errno_location.c --- /dev/null +++ b/runtime/POSIX/errno_location.c @@ -0,0 +1,9 @@ +#include + +#undef errno +int errno __attribute__((weak)); + +int __attribute__((weak)) *__errno_location(void) +{ + return &errno; +}