[cfe-dev] Static Analyzer symbolic execution path

[Anna Zaks]

On Feb 2, 2013, at 8:25 AM, Arthur Yoo <phjy007 at gmail.com> wrote:

> Hi all,
> 
> Recently I am working on developing a checker of Clang Static Analyzer. Because Clang Static Analyzer has a powerful symbolic execution engine, I choose Clang Static Analyzer as the platform for my work. My Checker mainly does some analysis work for C source code files. The checker will make use of the program states during its analysis execution and it will generate a report for each analysis. 
> 
> In my understanding, symbolic execution(Clang static analyzer) will cover all possible paths. For example, here is an sample source code which will be analyzed by static analyzer:
>  1  void func(int arg) {
>  2    int v;
>  3     if(arg > 0)  
>  4         v = arg + 1;
>  5     else
>  6         v = arg + 999;
>  7     int a, b;
>  8     a = 99; 
>  9     b = a;
> 10  }
> The symbolic execution path can be roughly represented as follow(based on ExplodedGraph):
> http://ww2.sinaimg.cn/large/a74ecc4cjw1e1fipmgpy5j.jpg
> And the execution sequence is 1-2-3-(1)-4-5. However, is there any possible means to change the execution sequence to be linear? That is to say, is there any possible means to change the execution sequence to be 1-2-(1)-4-5?

The analyzer is designed in away such that the checkers should not assume the order in which the exploded graph is built/processed. The checkers can store the information required for processing a successor inside the ExplodedNode instead of relying on the order. The order is decided when CoreEngine is constructed and it should not matter which order is chosen (apart from performance and coverage metrics). Why do you need the order to be different?

> Thanks for the help.
> 
> ------
> Best regards,
> Arthur Yoo
> _______________________________________________
> 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/20130204/4ceb346d/attachment.html>