<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hi, Arthur. The static analyzer is very much built on finding all possible paths through a program -- right now there's no way to tell it that two paths "merge" together in this way. However, in this case it may actually be able to figure this out: because 'arg' and 'v' are not referenced after the full if-statement, they could get cleaned out of the state being tracked, which means that the second time through the analyzer will say "oh, I've seen this state before".</div><div><br></div><div>We would like to do more things like this ("widening" to encompass/join two paths), but it's a hard problem to decide that two states are "the same", and if they aren't the same how to merge them with minimal loss of precision.</div><div><br></div><div>Apart from that, though, the analyzer's not even guaranteed to traverse paths in a depth-first search. Currently it does, but that decision has gone back and forth, and we might try BFS or some mixed search order again in the future. This currently isn't convenient to change: you have to tweak the constructor of CoreEngine in CoreEngine.h and then recompile.</div><div><br></div><div>Finally, though, if you are trying to generate notes along the path of execution, you should do this after the fact using a BugReporterVisitor. This is sort of like a checker for a bug path—you get to see all the nodes on <i>one</i> path that led to a particular bug report.</div><div><br></div><div>Hope that helps,</div><div>Jordan</div><div><br></div><br><div><div>On Feb 2, 2013, at 8:25 , 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 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>