
<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hello, Shweta. Currently, the static analyzer infrastructure isn't set up to run without any bug reporting—the "core" checkers which check for things like "division by zero" and "null pointer dereference" are used both for generating warnings and for halting analysis along a certain path.</div><div><br></div><div>I'm not sure what you mean by "getting symbolic expressions statically". The analyzer works in terms of symbolic and concrete values (SVals); the symbolic values have a typed representation with a basic hierarchical structure (SymExpr and SymbolData). In most parts of the analyzer, you don't ask for the current value of a variable but rather construct an expression involving the variable and ask the current state (ProgramState) to evaluate it.</div><div><br></div><div>Our current constraint solver is fairly simple, keeping sets of possible (scalar) values for symbols and applying a set-union each time a new constraint is added. The implementation uses sets of ranges as a fairly compact way to represent an accumulation of constraints on integers. However, constraints on symbols are not the only way a path can be deemed infeasible; any checker can mark the path as such. This is useful for, say, exceptions, which involve a control flow transfer that we can't follow without whole-program analysis.</div><div><br></div><div><br></div><div>Anna Zaks and I gave a talk at last year's LLVM Developer Meeting, which you can watch <a href="http://llvm.org/devmtg/2012-11/">here</a>. It's more aimed at checker writers, but the first part does contain a discussion of the high-level design of the analyzer and some of the important classes, including the ones I mentioned above.</div><div><br></div><div>Please feel free to e-mail us if you have specific questions about the static analyzer.</div><div><br></div><div>Best,</div><div>Jordan</div><div><br></div><br><div><div>On Mar 4, 2013, at 3:06 , Shweta Shinde <<a href="mailto:shwetasshinde24@gmail.com">shwetasshinde24@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><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>

_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br>http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev<br></blockquote></div><br></body></html>