<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div><br class=""></div><div><blockquote type="cite" class=""><div class="">On Dec 7, 2015, at 2:01 PM, Pengfei Wang via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hello,<div class=""><br class=""></div><div class="">I am writing a checker for the static analyzer with the following simple test case:</div><div class=""><p class=""><span class="">void</span> kernel_func(<span class="">MSG</span> *uptr){</p><p class=""><span class=""> char</span> * localbuffer =(<span class="">char</span>*) <span class="">malloc</span>(uptr-><span class="">msglength</span>);</p><p class=""><span class=""></span><span class=""> if</span> (localbuffer != NULL) {</p><p class=""><span class=""></span><span class=""></span> memcpy(localbuffer, uptr-><span class="">msg</span>, uptr-><span class="">msglength</span>);</p><p class=""><span class=""></span> }</p><div class="">
<br class="webkit-block-placeholder"></div><p class=""><span class=""><span class=""></span></span><span class=""> printf</span><span class="">(</span>"Kernel() Copied <span class="">msg</span> is %s\n"<span class="">, localbuffer);</span></p><p class=""><span class=""></span><span class=""> free</span>(localbuffer);</p><p class="">}<br class=""></p><p class="">In my opinion, there should be only two execution paths for the path-sensitive symbolic execution, for the reason that there is only one branch in the program. One execution steps into the IF statement, while the other one not. However, the test results shows a much longer execution trace. The forepart of the execution trace is similar to what I said above, two paths, but the rest doesn't make any sense to me. It repeated executing some part of the program that have already executed before, and not all the repeated process starts from a branch, some even start from the beginning of the program but without the taints I made before, which should be added if execute the program from the start point. </p><p class="">I am not sure what happens, but I kinda feel like some sort of backward order happens in the execution. </p></div></div></div></blockquote><div>How are you examining the execution order? The best way of finding out what the graph looks like and what caused the splits is by dumping the ExplodedGraph as described in <a href="http://clang-analyzer.llvm.org/checker_dev_manual.html#testing" class="">http://clang-analyzer.llvm.org/checker_dev_manual.html#testing</a>.</div><div class=""><br class=""></div><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><p class="">Is branch the only point that create a new path in the symbolic execution, or something else can also does the same thing?</p></div></div></div></blockquote>There are various reasons for splitting. For example, checkers could create 2 successor states. Said that we try to keep the number of splits to the minimum.<br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><p class="">Can anyone tell me why this happen? Do I miss something or misunderstanding how the path-sensitive symbolic execution works? I'll be very appreciate for any answers. Thank you!</p></div></div>
_______________________________________________<br class="">cfe-dev mailing list<br class=""><a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a><br class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev<br class=""></div></blockquote></div><br class=""></body></html>