<div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)">Hi all,</span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)"><br>
</span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)">I am working on static symbolic analysis and came across Clang Static Analyzer.</span></div>
<div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)">However, I am interested only in getting the symbolic expressions statically and not the bug finding logic of static analyzer. </span></div>
<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)"><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)"><br>
</span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)">So far, I am able to view the graph (which </span><span style="font-size:small;background-color:transparent">show the value ranges for symbolic variables)</span> using the following option:</div>
</span><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:13px;background-color:rgb(255,255,255)">clang -cc1 -analyze -analyzer-checker=core -analyzer-viz-egraph-graphviz test.c</span><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif"><br>
</span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif">Now, I want to get the actual symbolic expressions for these variables. How can I get it? </span></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif">As I won't be doing any bug analysis should I still write a checker just to access the analysis data, or is there any other way I can get the path symbolic expressions for all paths?</span></div>
<div><span style="color:rgb(34,34,34);font-family:arial,sans-serif"><br></span></div><div><font color="#222222" face="arial, sans-serif">Also, what kind of solver does clang static analyzer use for path satisfiability?</font></div>
<div><br></div><div><div><span style>Regards,</span><br style><span style>Shweta</span><br></div>
</div>