Re: [klee-dev] Trouble replaying test cases with symbolic files

2017-08-17 Thread Cristian Cadar
Hi, just a short note to say that this is now fixed in the mainline. Cristian On 09/08/17 16:55, Cristian Cadar wrote: Yes, the right way to replay tests generated with --posix-runtime is via klee-replay. As Yude said, it is possible in some circumstances for KLEE to explore paths that

Re: [klee-dev] Trouble replaying test cases with symbolic files

2017-08-09 Thread Cristian Cadar
Yes, the right way to replay tests generated with --posix-runtime is via klee-replay. As Yude said, it is possible in some circumstances for KLEE to explore paths that triggers errors in programs using symbolic files, but here there is actually a bug in KLEE that I plan to fix very soon. In

Re: [klee-dev] Trouble replaying test cases with symbolic files

2017-08-05 Thread Yude Lin
Hi Daniel, I think the first method doesn't understand symbolic inputs specified by '--posix-runtime', so you're right. Isn't it an expected result for the second method? If 'A' doesn't exist or is unreadable then the program crashes on fclose(NULL); test01 probably specifies an unreadable