Hi Cristi, 

Indeed, if we call klee_error instead of klee_warning, there is no point in 
calling it from everywhere. I didn't test, but the patch looks fine. 
Since several people ran into this problem, perhaps it is better to also say in 
the message to klee_error something like "try to increase your file descriptors 
limit".

Cristi

On Aug 5, 2010, at 11:39 AM, Cristian Cadar wrote:

> 
> 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
> <openOutputFile.patch>

Reply via email to