<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Arthur, <div><br><div>You are seeing the behavior I've described in the previous reply. When the analyzer knows that the loop will be executed more than 4 times (or whatever the loop unrolling bound is), it is NOT going to continue exploring the path after unrolling the loop 4 times. In order to continue exploring, it needs so simulate/approximate the remaining iterations. Simulating the remaining iterations is a feature that the analyzer does not currently have.</div><div><br></div><div>When we don't know that the loop has to execute at least 4 times, the rest of the function will be explored. In particular, we would explore a path on which exactly one iteration of the loop is executed following by the lines 8-15.</div><div><br></div><div>Anna.</div><div><br><div><div>On Apr 10, 2013, at 6:48 AM, Arthur Yoo <<a href="mailto:phjy007@gmail.com">phjy007@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><div dir="ltr"><p class="">Hi Anna, </p><p class="">Thank you and Jordan for your reply to answer my questions. Now I can understand the execution path sequence of ex3. However, it seems that I met another problem with loop execution path. <br></p><p class="">Here is my test code ex4:<br></p><p class=""> 1 void func(int arg) {</p><p class=""> 2 int v;</p><p class=""> 3 v = 0;</p><p class=""> 4 int i;</p><p class=""> 5 for(int i = 0; i < arg; i++) {</p><p class=""> 6 v = v + 1; </p><p class=""> 7 }</p><p class=""> 8 </p><p class=""> 9 if(arg < 0) {</p><p class=""> 10 v = 5566;</p><p class=""> 11 }</p><p class=""> 12 </p><p class=""> 13 int c;</p><p class=""> 14 c = v;</p><p class=""> 15 }</p><p class="">The corresponding CFG of ex4 is<span class="Apple-converted-space"> </span><a href="http://ww3.sinaimg.cn/large/a74ecc4cjw1e3kuhrthqij.jpg">http://ww3.sinaimg.cn/large/a74ecc4cjw1e3kuhrthqij.jpg</a></p><p class="">With analyzer, I get its execution path sequence: B7-B6-B3-B1-B2-B1-B5-B4-B6-B3-B1-B5-B4-B6-B3-B1-B5-B4-B6-B3-B1-B5-B4. It shows that the analyzer traces all possible paths in its CFG since arg(in line 5) is a symbolic value. Analyzer has no idea about whether arg is greater than zero. </p><p class="">Then I replaced the arg in line 5 with a concrete number(say 64, actually any number which is greater than three). <br></p><p class="">for(int i = 0; i < arg; i++) --> for(int i = 0; i < 64; i++)</p><p class="">Then the analyzer gave me the following execution path sequence: B7-B6-B5-B4-B6-B5-B4-B6-B5-B4-B6-B5-B4.</p><p class="">It is right that the loop has been executed for four time, but it seems that the analyzer didn't </p><p class="">cover all possible paths. In other words, it means that the analyzer didn't analyze the range from line 9 to line 14 in ex4's source code. I can't find the corresponding CFG blocks which represent the part of source code from line 9 to line 14 of ex4 in this execution path sequence. </p><p class="">In addition, I did another four tests. In these four tests, I replaced the loop condition with 0, 1, 2 and 3 for each time. The corresponding execution path sequences are below.</p><p class="">for(int i = 0; i < 3; i++): B7-B6-B5-B4-B6-B5-B4-B6-B5-B4-B6-B3-B1-B2-B1</p><p class="">for(int i = 0; i < 2; i++):<span class=""> </span>B7-B6-B5-B4-B6-B5-B4-B6-B3-B1-B2-B1</p><p class="">for(int i = 0; i < 1; i++):<span class=""> </span>B7-B6-B5-B4-B6-B3-B1-B2-B1</p><p class="">for(int i = 0; i < 0; i++):<span class=""> </span>B7-B6-B3-B1-B2-B1</p><p class="">With these four execution path sequences above, I can get the conclusion that for these four cases, the analyzer analyzed the whole ex4 source code and traced all possible paths in ex4. </p><p class="">So I don't know why the analyzer didn't analyze the range from line 9 to line 14 in ex4's source code when the loop time is more or equal to 4?</p><div class="gmail_extra"><br><br><div class="gmail_quote"><div class="gmail_extra" style="font-family: arial, sans-serif; font-size: 14px;">Best regards,</div><div class="gmail_extra" style="font-family: arial, sans-serif; font-size: 14px;">Arthur Yoo</div></div></div></div></div></blockquote></div><br></div></div></body></html>