Hi Milena, On Sun, Sep 27, 2009 at 1:41 PM, Milena Vujosevic-Janicic <milena at matf.bg.ac.rs> wrote: > 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.
Cool! > 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. Ok. Klee isn't currently structured all that great in terms of reusable libraries (at least for the symbolic execution core), but this should be possible. > 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). It looks like you are missing a number of libraries. Look at $KLEE_SRC_ROOT/tools/klee/Makefile to see the libraries that are linked into the 'klee' executable, those should be more or less the libraries you need to link. - Daniel > 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 > > > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
