[klee-dev] Klee Symbolic Files
daniel at zuster.org
Mon Feb 8 23:31:32 PST 2010
Without more information its hard for me to know what might be happening here.
Is it possible to find a small test case?
On Sun, Feb 7, 2010 at 1:40 PM, David <dkohlbre at cmu.edu> wrote:
> 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?
> -David Kohlbrenner
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
More information about the klee-dev