How does KLEE count number of branches

Question

I'm using Klee 2.9, and trying to obtain branch information from stat file klee generats. I fed in a one if-else statement program, and klee reported NumBranches as 8.

Code under test is shown below,

#include <stdio.h>
#include <stdbool.h>

int main(){
    int a;
    int b;
    klee_make_symbolic(&a,sizeof(a),"a");
    klee_make_symbolic(&b,sizeof(b),"b");
    if (a / b == 1) {
        printf("a==b\n");
    }
    else {
        printf("a!=b\n");   
    }
    return 0;
}

and file output run.stats in shown below, ('Instructions','FullBranches','PartialBranches','NumBranches','UserTime','NumStates','MallocUsage','NumQueries','NumQueryConstructs','NumObjects','WallTime','CoveredInstructions','UncoveredInstructions','QueryTime','SolverTime','CexCacheTime','ForkTime','ResolveTime',)

(0,0,0,8,5.609000e-03,0,528704,0,0,0,4.196167e-05,0,78,0.000000e+00,0.000000e+00,0.000000e+00,0.000000e+00,0.000000e+00)

(32,2,0,8,9.722000e-03,0,654176,3,56,0,3.826760e-01,27,51,3.799300e-01,3.802470e-01,3.801040e-01,6.900000e-05,0.000000e+00)

Can anyone explain me how does 8 come from?

Answer 1

Two possible reasons:

"klee_make_symbolic" and "printf" contains conditional statements. When KLEE executes the program, it does not differentiate your functions from external functions.

If you run KLEE with "--libc=uclibc", the main function will be replaced with "__uclibc_main". "__uclibc_main" first do some initialization works and then call the original "main" function. The initialization might contain some conditional statements.

You need to check the version of KLEE and the commands you used.