[LLVMdev] Z3 and loadable optimization

[John Criswell]

On 4/5/13 4:03 PM, Giacomo Tagliabue wrote:
> 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?

Yes and Yes.  Try using the -load option of the opt command to load 
libz3.so into opt's address space.  It might work even though libz3.so 
isn't a plugin to opt.

-- John T.

>
>
> On 5 April 2013 15:32, John Criswell <criswell at illinois.edu 
> <mailto: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 list
>>     LLVMdev at cs.uiuc.edu  <mailto: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/c50656bb/attachment.html>