<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">On 4/5/13 4:03 PM, Giacomo Tagliabue
wrote:<br>
</div>
<blockquote
cite="mid:CANOVvD+Jymp+L2GsP2Kih1gHgu1nByKVkSX0_aJ64XJSFrt+1w@mail.gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html;
charset=ISO-8859-1">
<div dir="ltr">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?</div>
</blockquote>
<br>
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.<br>
<br>
-- John T.<br>
<br>
<blockquote
cite="mid:CANOVvD+Jymp+L2GsP2Kih1gHgu1nByKVkSX0_aJ64XJSFrt+1w@mail.gmail.com"
type="cite">
<div class="gmail_extra"><br>
<br>
<div class="gmail_quote">
On 5 April 2013 15:32, John Criswell <span dir="ltr"><<a
moz-do-not-send="true" href="mailto:criswell@illinois.edu"
target="_blank">criswell@illinois.edu</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
<div>
<div class="h5">
<div>On 4/5/13 3:16 PM, Giacomo Tagliabue wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">I created a loadable optimization
following the tutorial at <a
moz-do-not-send="true"
href="http://llvm.org/docs/WritingAnLLVMPass.html"
target="_blank">http://llvm.org/docs/WritingAnLLVMPass.html</a>.
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:<br>
<blockquote class="gmail_quote" style="margin:0px
0px 0px
0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">opt:
symbol lookup error:
/home/giacomo/llvm/Debug+Asserts/lib/Acsl.so:
undefined symbol: Z3_mk_config<br>
</blockquote>
<div>What's the issue?<br>
</div>
</div>
</blockquote>
<br>
</div>
</div>
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.<br>
<br>
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.<br>
<br>
-- John T.<br>
<br>
<blockquote type="cite">
<div dir="ltr">
<div>Thanks</div>
</div>
<br>
<fieldset></fieldset>
<br>
<pre>_______________________________________________
LLVM Developers mailing list
<a moz-do-not-send="true" href="mailto:LLVMdev@cs.uiuc.edu" target="_blank">LLVMdev@cs.uiuc.edu</a> <a moz-do-not-send="true" href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a>
<a moz-do-not-send="true" href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a>
</pre>
</blockquote>
<br>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
<br>
</body>
</html>