[klee-dev] symbolic files and replay

[Alvin Cheung]

Hello,

I wrote a small program to test klee replay with symbolic files:

#define BUFSIZE 10
int main(int a, char * b[])
{
   char buf[BUFSIZE];
   int fd = open("A", O_RDONLY);

   unsigned numChars = 0;
   ssize_t r = read(fd, buf, BUFSIZE);

   unsigned i;
   for (i = 0; i < r; ++i)
   {
     if (buf[i] != '\0')
       ++numChars;
   }

   close(fd);
   return numChars;
}

I created a concrete file "A" with 20 non '\0' chars and then manually recorded 
the branches in main.  Then I modified klee to read the branch log only if the 
branches are in main (and back to default behavior otherwise), and ran klee 
with:

klee -replay-path=branchLog --posix-runtime --init-env test.bc -sym-files 1 20

My intention was to have klee generate constraints for the first 10 chars in 
the 
symbolic file "A" after replay, but instead I got an `!branch && "hit invalid 
branch in replay path mode" failed' error at the buf[i] != '\0' branch (the log 
says the condition is true).  Just wondering if I am using klee incorrectly?

Thanks,
Alvin