Dear all, I am a PhD student at the University of Belgrade, working in software safety. I have downloaded your tool Klee and ran it successfully on a range of examples.
I am planing to try to build a new verification tool on top of LLVM. I would also like to use some functionalities of Klee. I am using LLVM as libraries, but I have failed to use Klee in that way too. I made an empty project and in my Makefile I included all the Klee libraries (that were built within the distribution), but I got a lot of "undefined reference to ..." messages (you can see the error report at the end of the mail). What is the simplest way for me to use Klee? Am I missing some libraries or something else? Any suggestion will be more than welcome. Thank you very much in advance. Sincerely, Milena Vujosevic-Janicic Univ of Belgrade url: http://www.matf.bg.ac.rs/~milena (__cxa_atexit.o): In function `__cxa_atexit': /home/milena/llvm/klee/runtime/klee-libc/__cxa_atexit.c:32: undefined reference to `klee_warning_once' /home/milena/llvm/klee/runtime/klee-libc/__cxa_atexit.c:38: undefined reference to `klee_report_error' libKLEE/libklee-libc.a(abort.o): In function `abort': /home/milena/llvm/klee/runtime/klee-libc/abort.c:15: undefined reference to `klee_abort' libKLEE/libkleeCore.a(Memory.o): In function `ObjectState': /home/milena/llvm/klee/lib/Core/Memory.cpp:121: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:121: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:135: undefined reference to `klee::UpdateList::UpdateList(klee::UpdateList const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:135: undefined reference to `klee::UpdateList::UpdateList(klee::UpdateList const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:101: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:106: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:106: undefined reference to `klee::UpdateList::operator=(klee::UpdateList const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:106: undefined reference to `klee::UpdateList::~UpdateList()' /home/milena/llvm/klee/lib/Core/Memory.cpp:101: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:106: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:106: undefined reference to `klee::UpdateList::operator=(klee::UpdateList const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:106: undefined reference to `klee::UpdateList::~UpdateList()' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::flushRangeForWrite(unsigned int, unsigned int)': /home/milena/llvm/klee/lib/Core/Memory.cpp:289: undefined reference to `klee::UpdateList::extend(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:294: undefined reference to `klee::UpdateList::extend(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::flushRangeForRead(unsigned int, unsigned int) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:269: undefined reference to `klee::UpdateList::extend(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:273: undefined reference to `klee::UpdateList::extend(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `~ObjectState': /home/milena/llvm/klee/lib/Core/Memory.cpp:152: undefined reference to `klee::UpdateList::~UpdateList()' /home/milena/llvm/klee/lib/Core/Memory.cpp:152: undefined reference to `klee::UpdateList::~UpdateList()' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write8(klee::ref<klee::Expr>, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:426: undefined reference to `klee::UpdateList::extend(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write16(klee::ref<klee::Expr>, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:699: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:699: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:702: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:702: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write1(klee::ref<klee::Expr>, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:664: undefined reference to `klee::ZExtExpr::create(klee::ref<klee::Expr> const&, unsigned int)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write16(unsigned int, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:682: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:683: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write1(unsigned int, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:660: undefined reference to `klee::ZExtExpr::create(klee::ref<klee::Expr> const&, unsigned int)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write32(unsigned int, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:727: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:728: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:729: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:730: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write64(unsigned int, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:797: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' libKLEE/libkleeCore.a(Memory.o):/home/milena/llvm/klee/lib/Core/Memory.cpp:798: more undefined references to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' follow libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::getUpdates() const': /home/milena/llvm/klee/lib/Core/Memory.cpp:202: undefined reference to `klee::UpdateList::UpdateList(klee::Array const*, klee::UpdateNode const*)' /home/milena/llvm/klee/lib/Core/Memory.cpp:202: undefined reference to `klee::UpdateList::operator=(klee::UpdateList const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:202: undefined reference to `klee::UpdateList::~UpdateList()' /home/milena/llvm/klee/lib/Core/Memory.cpp:206: undefined reference to `klee::UpdateList::extend(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read8(unsigned int) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:370: undefined reference to `klee::ReadExpr::create(klee::UpdateList const&, klee::ref<klee::Expr>)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read64(unsigned int) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:559: undefined reference to `klee::ConcatExpr::create8(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read32(unsigned int) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:505: undefined reference to `klee::ConcatExpr::create4(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read16(unsigned int) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:471: undefined reference to `klee::ConcatExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read1(unsigned int) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:458: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read8(klee::ref<klee::Expr>) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:388: undefined reference to `klee::ReadExpr::create(klee::UpdateList const&, klee::ref<klee::Expr>)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read64(klee::ref<klee::Expr>) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:615: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:615: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:615: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:615: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:615: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o):/home/milena/llvm/klee/lib/Core/Memory.cpp:615: more undefined references to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' follow libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read64(klee::ref<klee::Expr>) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:615: undefined reference to `klee::ConcatExpr::create8(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read32(klee::ref<klee::Expr>) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:537: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:537: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:537: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:537: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:537: undefined reference to `klee::ConcatExpr::create4(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read16(klee::ref<klee::Expr>) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:491: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:491: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:491: undefined reference to `klee::ConcatExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::read1(klee::ref<klee::Expr>) const': /home/milena/llvm/klee/lib/Core/Memory.cpp:462: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write64(klee::ref<klee::Expr>, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:837: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:837: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:840: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:840: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:843: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:843: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:846: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:846: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:849: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:849: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:852: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:852: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:855: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:855: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:858: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:858: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `klee::ObjectState::write32(klee::ref<klee::Expr>, klee::ref<klee::Expr>)': /home/milena/llvm/klee/lib/Core/Memory.cpp:751: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:751: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:754: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:754: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:757: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:757: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' /home/milena/llvm/klee/lib/Core/Memory.cpp:760: undefined reference to `klee::ExtractExpr::create(klee::ref<klee::Expr>, unsigned int, unsigned int)' /home/milena/llvm/klee/lib/Core/Memory.cpp:760: undefined reference to `klee::AddExpr::create(klee::ref<klee::Expr> const&, klee::ref<klee::Expr> const&)' libKLEE/libkleeCore.a(Memory.o): In function `Expr': /home/milena/llvm/klee/include/klee/Expr.h:172: undefined reference to `klee::Expr::count' libKLEE/libkleeCore.a(Memory.o): In function `ConstantExpr': /home/milena/llvm/klee/include/klee/Expr.h:302: undefined reference to `vtable for klee::ConstantExpr' collect2: ld returned 1 exit status make[1]: *** [phd] Error 1 make[1]: Leaving directory `/home/milena/Desktop/phd' make: *** [all] Error 2
