[klee-dev] KLEE generated only one path whereas program has two

[Sumit Kumar]

Hi,

I tried the latest version (1.2.0) of KLEE using docker. I used the
following program:

#include<stdio.h>
#include "../../klee_src/include/klee/klee.h"

int main(){
        int a;
        int x;

        klee_make_symbolic(&a, sizeof(a), "a");
        klee_make_symbolic(&x, sizeof(x), "x");

        a = x;

        if(x < 0){
                a = 1;
        }
}

I compiled the above program using clang:

        clang -emit-llvm -c -o simple.bc simple.c

I ran klee using the command:

        klee simple.bc

But the output from KLEE indicated that it completed only one path whereas
the program clearly has two paths. Can anyone please explain why this
happened ?

--
Thanks and Regards,
Sumit

_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev