hey, KLEE: WARNING ONCE: function "PyOS_string_to_double" has inline asm
Means that there is asm code used inside the C. This is not supported by asm, so you will not be able to execute this symbolically. KLEE: WARNING: undefined reference to function: cos Means that the function "cos" is used, but the definition is not in the bitcode. If you compile the bitcode to machine code, the function will be linked directly. If you run the bitcode in C, it is missing and, again, can not be executed symbolically. You should give each of those functions a look. Maybe you can find the code somewhere and compile it to bitcode yourself. Or you can replace the call with a function with similar semantics, which does exist in bitcode. Did you compile against klee's version of ulibc? Some of the undefined functions look like they may be in there. The POSIX environment model may be helpful as well. The floating-point functions (atan, cos) are simply not there, as klee does not support floats. The dlopen, dlsym and dlerror are used to open external libraries. Those are not there as bitcode, so klee will not be able to execute them symbolically. I have never seen the last ERROR, but maybe someone else can shed some light on that one. Cheers, Sven On 08/17/2015 05:00 AM, Dipanjan Das wrote: > Hi Everybody, > > I compiled Python with llvm-gcc to generate LLVM bitcode to be run on top > of KLEE. Though python.bc gets generated successfully, KLEE throws a bunch > of warnings during execution. Moreover, there's an LLVM error at the end > that causes KLEE to abort: "LVM ERROR: invalid argument to evalConstant()". > Does anybody have any clue on this? > > KLEE: WARNING ONCE: function "PyOS_string_to_double" has inline asm > KLEE: WARNING ONCE: function "PyOS_double_to_string" has inline asm > KLEE: WARNING: undefined reference to function: __ctype_b_loc > KLEE: WARNING: undefined reference to function: __finite > KLEE: WARNING: undefined reference to function: __isinf > KLEE: WARNING: undefined reference to function: __xstat64 > KLEE: WARNING: undefined reference to function: alarm > KLEE: WARNING: undefined reference to function: atan2 > KLEE: WARNING: undefined reference to function: bind_textdomain_codeset > KLEE: WARNING: undefined reference to function: bindtextdomain > KLEE: WARNING: undefined reference to function: copysign > KLEE: WARNING: undefined reference to function: cos > KLEE: WARNING: undefined reference to function: dcgettext > KLEE: WARNING: undefined reference to function: dgettext > KLEE: WARNING: undefined reference to function: dlerror > KLEE: WARNING: undefined reference to function: dlopen > KLEE: WARNING: undefined reference to function: dlsym > KLEE: WARNING: undefined reference to function: exp > KLEE: WARNING: undefined reference to function: fabs > KLEE: WARNING: undefined reference to function: faccessat > KLEE: WARNING: undefined reference to function: fchmodat > KLEE: WARNING: undefined reference to function: fchownat > KLEE: WARNING: undefined reference to function: fdopendir > KLEE: WARNING: undefined reference to function: fexecve > KLEE: WARNING: undefined reference to function: floor > KLEE: WARNING: undefined reference to function: fmod > KLEE: WARNING: undefined reference to function: forkpty > KLEE: WARNING: undefined reference to function: fstat64 > KLEE: WARNING: undefined reference to function: fstatat64 > KLEE: WARNING: undefined reference to function: futimens > KLEE: WARNING: undefined reference to function: getitimer > KLEE: WARNING: undefined reference to function: getpgid > KLEE: WARNING: undefined reference to function: getresgid > KLEE: WARNING: undefined reference to function: getresuid > KLEE: WARNING: undefined reference to function: getsid > KLEE: WARNING: undefined reference to function: gettext > KLEE: WARNING: undefined reference to function: hypot > KLEE: WARNING: undefined reference to function: linkat > KLEE: WARNING: undefined reference to function: log > KLEE: WARNING: undefined reference to function: lseek64 > KLEE: WARNING: undefined reference to function: lstat64 > KLEE: WARNING: undefined reference to function: lutimes > KLEE: WARNING: undefined reference to function: mkdirat > KLEE: WARNING: undefined reference to function: mkfifoat > KLEE: WARNING: undefined reference to function: mknodat > KLEE: WARNING: undefined reference to function: modf > KLEE: WARNING: undefined reference to function: nice > KLEE: WARNING: undefined reference to function: openat64 > KLEE: WARNING: undefined reference to function: openpty > KLEE: WARNING: undefined reference to function: posix_fadvise64 > KLEE: WARNING: undefined reference to function: posix_fallocate64 > KLEE: WARNING: undefined reference to function: pow > KLEE: WARNING: undefined reference to function: pread64 > KLEE: WARNING: undefined reference to function: pwrite64 > KLEE: WARNING: undefined reference to function: readlinkat > KLEE: WARNING: undefined reference to function: readv > KLEE: WARNING: undefined reference to function: renameat > KLEE: WARNING: undefined reference to function: round > KLEE: WARNING: undefined reference to function: sendfile64 > KLEE: WARNING: undefined reference to function: setegid > KLEE: WARNING: undefined reference to function: seteuid > KLEE: WARNING: undefined reference to function: setitimer > KLEE: WARNING: undefined reference to function: setregid > KLEE: WARNING: undefined reference to function: setreuid > KLEE: WARNING: undefined reference to function: sigaltstack > KLEE: WARNING: undefined reference to function: sin > KLEE: WARNING: undefined reference to function: stat64 > KLEE: WARNING: undefined reference to function: symlinkat > KLEE: WARNING: undefined reference to function: textdomain > KLEE: WARNING: undefined reference to function: truncate64 > KLEE: WARNING: undefined reference to function: utimensat > KLEE: WARNING: undefined reference to function: writev > LVM ERROR: invalid argument to evalConstant() > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
