Thanks, Cristi, that's a very good idea. I added this and applied the
patch in 110329.
Best,
Cristian
On 05/08/10 10:57, Cristian Zamfir wrote:
> 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>
>
