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

[Shweta Shinde]

Hi Ryan

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

Thanks,
Shweta


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>