Installing the last version from https://github.com/ccadar/klee it works better, but I still get the following warnings
mint@mint ~/coreutils-6.11/obj-llvm/src $ klee --libc=uclibc --posix-runtime ./cat.bc --version KLEE: NOTE: Using model: /llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory = "klee-out-4" KLEE: WARNING ONCE: function "vasnprintf" has inline asm KLEE: WARNING: undefined reference to function: __ctype_b_loc KLEE: WARNING: undefined reference to function: __xstat64 KLEE: WARNING: undefined reference to function: signbitl KLEE: WARNING: executable has module level assembly (ignoring) KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 56353760) KLEE: WARNING ONCE: calling __user_main with extra arguments. KLEE: WARNING ONCE: calling external: __xstat64(1, 56242880, 56514336) KLEE: WARNING ONCE: calling external: getpagesize() KLEE: WARNING ONCE: calling external: vprintf(56141712, 56544832) cat (GNU coreutils) 6.11 License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html > This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. Written by Torbjorn Granlund and Richard M. Stallman. KLEE: WARNING ONCE: calling close_stdout with extra arguments. Copyright (C) 2008 Free Software Foundation, Inc. KLEE: done: total instructions = 29255 KLEE: done: completed paths = 1 KLEE: done: generated tests = 1 Are they really warnings, or are they a real problem?. I suppose klee can not propagate the symbolic values through functions that are undefined. Thanks. 2013/11/11 Daniel Liew <[email protected]> > > The most similar file to the file asked in my installation is > > /llvm-2.9/klee/Release+Asserts/lib/libkleeRuntimePOSIX.a. Can I "ln -s" > this > > file to the file asked without worries?. > > No you **cannot** symlink libkleeRunTimePOSIX.bca to > libkleeRunTimePOSIX.a they are in two completely different formats. > The *.bca files are LLVM bitcode archives and *.a files are archives > of native binary objects. > > Can you run? > > $ cd /llvm-2.9/klee > $ find . -iname '*.bca' > > if your runtime is building correctly it maybe that the files are > ending up in a different folder (e.g. "Release" instead of > "Release+Asserts" which might of happened if you used the > --with-runtime= argument at configure time). > > Can you also confirm that you are running the latest upstream KLEE > from GitHub ( https://github.com/ccadar/klee )? > > Thanks, > Dan. >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
