diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/klee/main.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 2b7310ec..c3188259 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -353,9 +353,9 @@ std::ostream *KleeHandler::openOutputFile(const std::string &filename) { std::string path = getOutputFilename(filename); f = new std::ofstream(path.c_str(), io_mode); if (!f) { - klee_warning("out of memory"); + klee_error("error opening file \"%s\" (out of memory)", filename.c_str()); } else if (!f->good()) { - klee_warning("error opening: %s", filename.c_str()); + klee_error("error opening file \"%s\". KLEE may have run out of file descriptors: try to increase the maximum number of open file descriptors by using ulimit.", filename.c_str()); delete f; f = NULL; } |