Seems like it, yes. Please file a bugzilla if you have a reasonable test case.
There are cases where KLEE can fail to generate a report (the solver times out, for example), but it shouldn't crash. - Daniel On Fri, Jul 16, 2010 at 7:16 AM, heechul Yun <heechul.yun at gmail.com> wrote: > I ran KLEE to test a http protocol parser. In the middle of symbolic > execution by KLEE, it gave me the following message and halt. in the output > directory, only files up to test00031.ktest. > Is this a bug in KLEE? > KLEE: ERROR: klee-uclibc/libc/string/strcpy.c:27: memory error: out of bound > pointer > KLEE: NOTE: now ignoring this error at this location > KLEE: WARNING: unable to write output test case, losing it > KLEE: WARNING: error opening: test000033.ptr.err > 0 ? klee 0x08bfb468 > make: *** [test] Segmentation fault > -- > Heechul > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
