summaryrefslogtreecommitdiff
path: root/klee/tools
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2010-08-05 10:22:53 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2010-08-05 10:22:53 +0000
commitdee85226994486e2960633767d57dac3cc060248 (patch)
tree1c517d18c59d2afa7f056bb9c5df69821a849b90 /klee/tools
parentb58d9791aa13170d898a50d3f57c40420384c0c6 (diff)
Call klee_error instead of klee_warning when we fail to open a file,
and inform users about the common file descriptor problem. Based on patch and discussion with Cristian Zamfir.
Diffstat (limited to 'klee/tools')
-rw-r--r--klee/tools/klee/main.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/klee/tools/klee/main.cpp b/klee/tools/klee/main.cpp
index 2b7310ecd94..c31882599ec 100644
--- a/klee/tools/klee/main.cpp
+++ b/klee/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;
}