Hi Alvin,
I am not sure the current replay is fully functional. There is probably a
divergence in the path when you replay. You can also take a look at this
previous thread:
http://keeda.stanford.edu/pipermail/klee-dev/2010-March/000271.html
Cristi
On Jul 14, 2010, at 8:53 PM, Alvin Cheung wrote:
> 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
