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

[Ryan Govostes]

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/20130307/f53766b7/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ento-stp-shweta.diff
Type: application/octet-stream
Size: 40504 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130307/f53766b7/attachment.obj>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20130307/f53766b7/attachment-0001.html>