[cfe-dev] Static Analyzer - symbolic expressions in a program

[Shweta Shinde]

Hi all,

I am working on static symbolic analysis and came across Clang Static
Analyzer.
However, I am interested only in getting the symbolic expressions
statically and not the bug finding logic of static analyzer.

So far, I am able to view the graph (which show the value ranges
for symbolic variables) using the following option:
clang -cc1 -analyze -analyzer-checker=core -analyzer-viz-egraph-graphviz
test.c

Now, I want to get the actual symbolic expressions for these variables. How
can I get it?
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?

Also, what kind of solver does clang static analyzer use for
path satisfiability?

Regards,
Shweta
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130304/f7c858ac/attachment.html>