This is strange because Klee should handle out of memory exceptions, at least if you provided the max-memory switch. Did you try using that?
Cristi On Jul 17, 2010, at 6:11 PM, heechul Yun wrote: > This patch solve the segfault problem, but I encountered out of memory > exception instead. > It seems that the problem is not because of running out of file descriptors > but because of running out of memory. > > Easy reproduction is limiting heap size with ulimit as in the following, > > $ ulimit -v 65536 > > Running klee that requires more than 64MB of memory will give the following > memory allocation problem. > > $ klee --libc=uclibc --only-output-states-covering-new httpd.bc > .. > KLEE: WARNING: unable to open output test case .info file > ... > terminate called after throwing an instance of 'St9bad_alloc' > what(): std::bad_alloc > make: *** [test] Aborted > > Therefore, there will be no real fix for this (running out of memory!), but > it may be better to catch memory exception and give user some better > explanation. > > Just for curiosity, Is there anyone who is working on extending klee to > support smp or cloud? > > Best Regards, > > Heechul > > On Fri, Jul 16, 2010 at 11:04 AM, Cristian Zamfir <cristian.zamfir at > epfl.ch> wrote: > This happens when Klee runs out of file descriptors. You can avoid it by > increasing the number of file descriptors using ulimit. > > The crash happens because callers of openTestFile do not check if the return > is NULL. > We encountered this problem before. The attached patch should fix it, in the > sense that it avoids crashing and prints a warning instead. If it is ok, I > can commit it. > > Cristi > > > > On Jul 16, 2010, at 5:27 PM, Daniel Dunbar wrote: > > > 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 > >> > >> > > _______________________________________________ > > klee-dev mailing list > > klee-dev at keeda.stanford.edu > > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > > > > > -- > > Heechul
