<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; "><br><div><div>On Feb 2, 2013, at 8:25 AM, Arthur Yoo <<a href="mailto:phjy007@gmail.com">phjy007@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Hi all,<div><br></div><div>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. </div>
<div><br></div><div>In my understanding, symbolic execution(Clang static analyzer) will cover all possible paths. For example, here is an sample source code which will be <span style="font-family: 'Microsoft YaHei'; font-size: 13px; white-space: nowrap; ">analyzed</span> by static analyzer:</div>
<div><div> 1  void func(int arg) {</div><div> 2    int v;</div><div> 3     if(arg > 0)  </div><div> 4         v = arg + 1;</div><div> 5     else</div><div> 6         v = arg + 999;</div><div> 7     int a, b;</div><div>
 8     a = 99; </div><div> 9     b = a;</div><div>10  }</div><div><div style="">The symbolic execution path can be <span style="font-family: 'Microsoft YaHei'; font-size: 13px; white-space: nowrap; ">roughly</span> represented as follow(based on ExplodedGraph):</div>
<div style=""><a href="http://ww2.sinaimg.cn/large/a74ecc4cjw1e1fipmgpy5j.jpg">http://ww2.sinaimg.cn/large/a74ecc4cjw1e1fipmgpy5j.jpg</a><br></div><div style=""><div>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?</div></div></div></div></div></blockquote><div><br></div><div>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?</div><br><blockquote type="cite"><div dir="ltr"><div><div><div style="">
<div style="">Thanks for the help.</div></div><br>------<br>Best regards,<br>Arthur Yoo</div></div></div>
_______________________________________________<br>cfe-dev mailing list<br><a href="mailto:cfe-dev@cs.uiuc.edu">cfe-dev@cs.uiuc.edu</a><br>http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev<br></blockquote></div><br></body></html>