[cfe-dev] backward path analysis

[Zhongxing Xu]

On Fri, Jun 11, 2010 at 11:55 PM, Cristian Zamfir
<cristian.zamfir at epfl.ch>wrote:

>
> Hello,
>
> I am new to the Clang Static Analyzer and I am trying to determine if it
> can be used to find the set of paths from the beginning of a program to a
> given basic bloc in the program. Enumerating all these paths will most
> likely be intractable, but obtaining them on-demand may be possible. This is
> in a way similar to a backward slicing algorithm.
>
> Here is a simple example. Could the analyzer figure out that the only path
> through function func that triggers the bug must execute the first case of
> the switch statement?
>
> int func(int x) {
>        int y;
>        switch(x) {
>                case 1:
>                        y = 0;
>                        break;
>                case 2:
>                        y = 1;
>                        break;
>                default:
>                        y = 2;
>                        break;
>        }
>
>        if (y != 0)
>                return 0;
>        else
>                return 1;
> }
>
> int main (int argc, char* argv) {
>        ...
>        if( func(argc) == 1 )
>                BUG();                        //this is the target basic
> block
>        ...
> }
>
> Is this already possible? If not, how complex would it be to write in the
> analyzer? Does the analyzer support path-sensitive analyses?
>

There are two analysis engine implemented. The standard flow sensitive data
flow analysis supports both forward and backward analysis. The path
sensitive analysis engine only supports forward analysis.


>
> I also have a few other questions:
>
> Does the analyzer support deadlock and data-race detection? I did not see
> this in the source code.
>

No.


>
> Also, I thought that normally static analysis will have lots of false
> positives. I ran scan-build on the linux kernel and it reported no bugs.
> Instead, it reported a few bugs in the analyzer.
>
> Thanks a lot,
> Cristi
>
>
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20100612/abc09a06/attachment.html>