[LLVMdev] Z3 and loadable optimization

[Giacomo Tagliabue]

I think I am in the first case, but I don't understand something, the -load
option during which command? opt? and which file should I load? libz3.so?


On 5 April 2013 15:32, John Criswell <criswell at illinois.edu> wrote:

>  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 listLLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.eduhttp://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130405/bdc0b4a4/attachment.html>