<div dir="ltr"><div><div><div><div></div>I would suggest you take a look at KLEE, PAGAI and GiNaC.<br>The first two are LLVM-based tools that do symbolic manipulation (of sorts) and the last is a C++ library for doing symbolic computation which is quite easy to use with an RTTI build of LLVM.<br>
</div>If you can give us an example of what symbolic equation you might be trying to "solve", I'm sure we can narrow it down or suggest something new.<br></div>Also, Ben Hardekopf & Calvin Lin have an article in CGO'11 about a flow-sensitive pointer analysis. You might take a look and see if they used something that might help you out.<br>
<br></div>H.<br><div><div><div><div><div><br></div></div></div></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Nov 18, 2013 at 11:31 AM, Peter Chang <span dir="ltr"><<a href="mailto:blankboy2011@gmail.com" target="_blank">blankboy2011@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><p style="clear:both;vertical-align:baseline;line-height:18px;font-size:14px;font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;margin:0px 0px 1em;border:0px;padding:0px">


Hello,</p><p style="clear:both;vertical-align:baseline;line-height:18px;font-size:14px;font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;margin:0px 0px 1em;border:0px;padding:0px">

I want to do points-to anlysis in llvm IR. I want it to be path sensitive, which means that when I print out the result, I need append the condition for the "May" Points-to.</p><p style="clear:both;vertical-align:baseline;line-height:18px;font-size:14px;font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;margin:0px 0px 1em;border:0px;padding:0px">


I plan to using symbolic execution to achieve this goal.</p><p style="clear:both;vertical-align:baseline;line-height:18px;font-size:14px;font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;margin:0px 0px 1em;border:0px;padding:0px">


Are there any tools in llvm, or stand-alone tools to solve the symbolic equation.</p><p style="clear:both;vertical-align:baseline;line-height:18px;font-size:14px;font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;margin:0px 0px 1em;border:0px;padding:0px">


Thank you!</p><span class="HOEnZb"><font color="#888888"><p style="clear:both;vertical-align:baseline;line-height:18px;font-size:14px;font-family:Arial,'Liberation Sans','DejaVu Sans',sans-serif;margin:0px 0px 1em;border:0px;padding:0px">


----Peter Chang</p></font></span></div>
<br>_______________________________________________<br>
LLVM Developers mailing list<br>
<a href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a><br>
<br></blockquote></div><br></div>