[cfe-dev] Clang Static Analyzer execution path for loop

[Anna Zaks]

On Apr 6, 2013, at 11:30 PM, Arthur Yoo <phjy007 at gmail.com> wrote:

> Hi all,
> 
> Now I am focusing on the execution path of Clang Static Analyzer. Firstly, I did some tests on code_1.c. 
> 
> //code_1.c
> 
> void func(int arg) {
> 
>     int v;
> 
>     v = 0;  
> 
>     int i;
> 
>     for(i = 0; i < arg; i++) {
> 
>         v = v + 1;
> 
>     }   
> 
>     int a, b;
> 
>     a = v;
> 
>     b = a;
> 
> }
> 
> The CFG of code_1.c is http://ww3.sinaimg.cn/large/a74e55b4jw1e3h14gvh8vj.jpg. 
> 
> Then I tried to get the corresponding execution path sequence. Through test I got its execution path sequence, which is B5-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2. (In code_1.c, the variable arg, which determines the loop times, is a symbolic value. And I used the default max_loop value in Clang Static Anaylzer, which equals 4.) 
> 
> 
> 
> I tried to do the same tests on code_2.c. 
> 
> //code_2.c
> 
> void func(int arg) {
> 
>     int v;
> 
>     v = arg + 1;
> 
>     if(arg < 314)  {
> 
>         for(int i = 0; i < arg; i++) {
> 
>             v = arg + 33; 
> 
>         }   
> 
>     } else {
> 
>         v = arg + 11; 
> 
>     }   
> 
>     int a, b;
> 
>     a = 62951413;
> 
>     b = v;
> 
> }
> 
> The CFG of code_2.c is http://ww2.sinaimg.cn/large/a74eed94jw1e3h13zu3raj.jpg.  And its execution path sequence is B7-B2-B1-B6-B5-B1-B4-B3-B5-B1-B4-B3-B5-B1-B4-B3-B5-B1-B4-B3. The rule of tracing path in code_2.c is consistent with the rule in code_1.c.
> 
> 
> 
> However, when I tried to do the same tests on code_3.c. 
> 
> //code_3.c
> 
> void func(int arg) {
> 
>     int v;
> 
>     v = arg + 1;
> 
>     if(arg < 314) {
> 
>         v = arg + 11; 
> 
>     } else {
> 
>         for(int i = 0; i < arg; i++) {
> 
>             v = arg + 33; 
> 
>         }
> 
>     }
> 
>     int a, b;
> 
>     a = 62951413;
> 
>     b = v;
> 
> }
> 
> The CFG of code_3.c is http://ww4.sinaimg.cn/large/a74ecc4cjw1e3h13ae2xtj.jpg. It seems that some strange things happened. Through test I got its execution path sequence, which is B7-B5-B4-B3-B2-B4-B3-B2-B4-B3-B2-B4-B3-B2-B6-B1. In fact, I expected the execution sequence should be B7-B5-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B4-B1-B3-B2-B6-B1. 
> 
> 
> 
Are you saying that  'v = arg + 11;' is executed twice on the path you are observing? 
How are you observing the execution path sequences? You cannot see the paths by observing the callbacks from the checkers since the analyzer does not make any guarantees on the order in which statements from different paths are processed. In this example, there are more than 2 paths through this program. You might be observing parts of different paths.

Cheers,
Anna.
> So, is there anybody can help me explain the execution path of Clang Static Analyzer in code_3.c?
> 
> Am I doing something stupid here? Any help will be greatly appreciated.
> 
> P.S. The version number of LLVM and Clang in my tests is 3.3.
> 
> ------
> 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/20130408/e1585c60/attachment.html>