<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><div class="gmail_extra"><br><br><div class="gmail_quote">
On 5 April 2013 15:32, John Criswell <span dir="ltr"><<a 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 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 href="mailto:LLVMdev@cs.uiuc.edu" target="_blank">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a>
<a 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>