Hi, I've been doing some work with analyzing the predicates for certain test cases that Klee generates and I've noticed some odd behavior with sym-files.
When I set the klee run to use sym-files and during one of the paths it encounters a pointer error, the .pc file and the .ktest file generated for that test case are incorrect. Specifically, the kquery for the actual data in the symbolic file is blank, and the test case data for the file is all nulls. If I run the test case, the program does not crash (as the test case claims to cause.) On that same run of klee, test cases that did not encounter a pointer error have correct kquery and test case data for the symbolic file; only test cases that purport to result in a crash are 'empty'. Any pointers as to whats going wrong? Thanks, -- -David Kohlbrenner -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100207/206e4c82/attachment.html
