[klee-dev] Error while replaying .path file

Awanish Pandey avanis1994 at gmail.com
Tue Feb 18 07:47:12 GMT 2020


*******************
This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. 
If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address.
*******************
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
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list