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

Shweta Shinde shwetasshinde24 at gmail.com
Thu Mar 7 20:16:04 PST 2013

Hi Ryan

Thanks a lot for the patch! I will report back after checking how it works
for my analysis and benchmarks.


On Fri, Mar 8, 2013 at 11:59 AM, Ryan Govostes <rzg at apple.com> wrote:

> Hi Shweta,
> Please find attached a preliminary version of my patch. I am curious to
> hear from you how well it works.
> The STP-based constraint manager is implemented as a plug-in which lives
> in clang/tools/smt-constraint-manager/. There is a README file in that
> directory that explains how to build and use the plug-in. I have only
> tested it on OS X.
> The README also details some caveats that will affect both accuracy and
> performance.
> Note that with this patch applied, the static analyzer will perform worse
> even when the plug-in is not active, because I had to disable an
> optimization in SValBuilder::makeSymExprValNN. I also hope to solve this
> before submitting the patch, but please keep this in mind if you are
> planning on running benchmarks.
> Best,
> Ryan
> On Mar 7, 2013, at 7:27 PM, Shweta Shinde <shwetasshinde24 at gmail.com>
> wrote:
> Thanks for the reply!
> I will use the checkAssume callback and check if I can manage to get what
> I want.
> It will be great if STP is made available as an alternative in cases where
> precise results is the priority.
> For now, I would like to check if the slowdown due to Ryan's patch is
> significant or trivial for my purposes.
> Can I get the patch for checking the slowdown on my tests?
> Regards,
> Shweta
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130308/c6f8bf01/attachment.html>

More information about the cfe-dev mailing list