[cfe-dev] Symbolic Execution Path Order Problem

[Pengfei Wang via cfe-dev]

Hello,

I am writing  a checker for the static analyzer with the following simple
test case:

void kernel_func(MSG *uptr){

    char * localbuffer =(char*) malloc(uptr->msglength);

    if (localbuffer != NULL) {

        memcpy(localbuffer, uptr->msg, uptr->msglength);

    }

    printf("Kernel() Copied msg is %s\n", localbuffer);

    free(localbuffer);

}

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.

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?

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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20151207/777b1185/attachment.html>