Hi Cristi,
That's a rather minor thing, but instead of having all the callers of
openTestFile (and openOutputFile) call klee_error or assert, I would
just call klee_error directly in openOutputFile. Let me know if you see
any problems in the attached patch.
Thanks,
Cristian
On 25/07/10 21:09, Cristian Zamfir wrote:
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: openOutputFile.patch
Type: text/x-diff
Size: 594 bytes
Desc: not available
Url :
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100805/f9e32b3b/attachment.bin
