[klee-dev] Error while replaying .path file

[Cadar, Cristian]

Hi Awanish,

Unfortunately that feature has not been maintained -- we need to fix it, 
but there are no immediate plans to do so.

You may be able to achieve something similar via seeding (-seed-file). 
Or if you just want to replay the test case, use klee-replay or link 
with the libkleeRuntest library (see the tutorials).

Best,
Cristian

On 18/02/2020 07:47, Awanish Pandey wrote:
> Dear all,
> I want to replay a path file, but I am getting an assertion 
> violation "hit an invalid branch in replay path mode".
> 
> This is my toy program
> /int main(int argc, char *argv[]){
>    if (argc != 2){
>      printf("error:");
>    }
>    int a;
>    FILE *fp = fopen(argv[1], "r");
>    fscanf(fp,"%d",&a);
>    if (a == 10)
>      assert(0);
>    fclose(fp);
>    return 0;
> }/
> 
> I run klee "/klee --libc=uclibc --posix-runtime --write-paths file.bc 
> --sym-arg 1  --sym-files 1 5/".
> It finds an assertion violation (at test case number 19) and when I 
> replayed it by command
> /klee --libc=uclibc --posix-runtime 
> --replay-path=klee-out-0/test000019.path file.bc/
> 
> Klee crashes on assertion violation in Executor.cpp
> 
> What is the issue? It will be very helpful.
> -- 
> Thanking You
> Awanish Pandey
>