A non-text attachment was scrubbed...
Name: failed_test_case.patch
Type: application/octet-stream
Size: 3886 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100725/d49074eb/attachment.obj
-------------- next part --------------
Thanks for noticing. I updated it.
Cristi
On Jul 25, 2010, at 9:48 PM, heechul Yun wrote:
> I think there is a mistake.
> Please see the red lines of your patch.
>
> if (WriteTestInfo) {
> double elapsed_time = util::getWallTime() - start_time;
> std::ostream *f = openTestFile("info", id);
> if(f) {
> *f << "Time to generate test case: "
> << elapsed_time << "s\n";
> delete f;
> }
> } else {
> klee_error("unable to open output test case .info file");
> }
> }
> }
>
> I think the correct code should be the following
>
> if (WriteTestInfo) {
> double elapsed_time = util::getWallTime() - start_time;
> std::ostream *f = openTestFile("info", id);
> if(f) {
> *f << "Time to generate test case: "
> << elapsed_time << "s\n";
> delete f;
> } else {
> klee_error("unable to open output test case .info file");
> }
> }
>
>
> Best
>
> Heechul
>
>
> On Sun, Jul 25, 2010 at 2:41 PM, Cristian Zamfir <cristian.zamfir at epfl.ch>
> wrote:
>
> Hi Cristi,
>
> You are right, I doubt that the reasons for running out of fds are transient,
> so it is better to stop. I modified the patch.
>
>
>
> Cristi
>
>
> On Jul 16, 2010, at 8:19 PM, Cristian Cadar wrote:
>
> >
> > Hi Cristi,
> >
> > That's a good patch. I'm just wondering if there's really any benefit of
> > continuing execution once KLEE runs out of file descriptors. That is, we
> > could instead just call klee_error instead of klee_warning in
> > openOutputFile.
> >
> > Best,
> > Cristian
> >
> > On 16/07/10 17:04, Cristian Zamfir 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
> >>
>
>
>
>
>
> --
>
> Heechul
