[LLVMdev] Z3 and loadable optimization

[John Criswell]

On 4/5/13 3:16 PM, Giacomo Tagliabue wrote:
> I created a loadable optimization following the tutorial at 
> http://llvm.org/docs/WritingAnLLVMPass.html. I want to use the Z3 
> library, installed in my system, in my optimization. When I include 
> z3++.h (the name of the library) in the code and use its classes, it 
> compiles well, but when I try to run it it says:
>
>     opt: symbol lookup error:
>     /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so: undefined symbol:
>     Z3_mk_config
>
> What's the issue?

If the Z3 library is a dynamically linked library, then it's probably 
not being loaded into opt.  You might be able to force loading of it 
with the -load option or by setting your LD_LIBRARY_PATH environment 
variable to include the location of the Z3 library.

If the Z3 library is a statically linked library (a .a file on Linux), 
then it might be the case that not all of the symbols in libz3.a are 
being linked into your pass's .so file (because the linker doesn't think 
those symbols are used).  LLVM has similar problems with its .a files 
and uses LinkAllPasses.h to trick the compiler into including all the 
functions that it needs for .a files.  A similar hack should fix the 
problem that you're seeing.

-- John T.

> Thanks
>
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130405/94904585/attachment.html>