Dear Daniel, Thank you very much for your quick response.
> 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. I think that I did include all these libraries - trying to find out what was missing I included all the klee and all the llvm libraries. I wrote a simple main file (just including llvm "Hello world" pass, few includes from klee and a main function printing "hello") and a simple Makefile that includes all the libraries from llvm and klee (main.cpp and Makefile are attached). Maybe I am missing something with the Makefile (unfortunately, I am not very experienced in programming under Linux)? Any hint would be very welcome. Thank you very much in advance. Milena ----- Original Message ----- From: "Daniel Dunbar" <[email protected]> To: "Milena Vujosevic-Janicic" <milena at matf.bg.ac.rs> Cc: <klee-dev at keeda.stanford.edu> Sent: Monday, September 28, 2009 12:41 AM Subject: Re: [klee-dev] The simplest way to use functionalities of KLEE within another project? > > 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:7 98: > > 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:6 15: > > 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 > > > > > -- > Internal Virus Database is out-of-date. > Checked by AVG. > Version: 7.5.560 / Virus Database: 270.12.11/2089 - Release Date: 30.4.2009 17:53 > > -------------- next part -------------- A non-text attachment was scrubbed... Name: main.cpp Type: application/octet-stream Size: 1194 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090929/749af7d4/attachment.obj -------------- next part -------------- A non-text attachment was scrubbed... Name: Makefile Type: application/octet-stream Size: 1950 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090929/749af7d4/attachment-0001.obj
