<div dir="ltr">Hello,<div><br></div><div>I am writing  a checker for the static analyzer with the following simple test case:</div><div>







<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><p class="">











</p><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></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. Is branch the only point that create a new path in the symbolic execution, or something else can also does the same thing?</p><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>