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? Thanks -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130405/bdb9cbee/attachment.html>
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>
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>