about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2012-11-28 18:08:52 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2012-11-28 18:08:52 +0000
commit993c4d6be0bcc826ccc1a735a09b875d8784ad7f (patch)
treecd28bdeed758dc4969d827efd952da6527594bbe
parent6d9be03c5f322207637c88eac881563c1f8420ac (diff)
downloadklee-993c4d6be0bcc826ccc1a735a09b875d8784ad7f.tar.gz
Only emitting a warning, instead of failing on large mallocs.
Addresses the issue raised by Bowen Zhou at http://keeda.stanford.edu/pipermail/klee-dev/2012-November/000972.html.
Fixed test case that depended on the old behavior.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@168797 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--lib/Core/MemoryManager.cpp7
-rw-r--r--test/Feature/Realloc.c (renamed from test/Feature/ReallocFailure.c)4
2 files changed, 5 insertions, 6 deletions
diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp
index 06c234a2..a1198007 100644
--- a/lib/Core/MemoryManager.cpp
+++ b/lib/Core/MemoryManager.cpp
@@ -36,10 +36,9 @@ MemoryManager::~MemoryManager() {
 MemoryObject *MemoryManager::allocate(uint64_t size, bool isLocal, 
                                       bool isGlobal,
                                       const llvm::Value *allocSite) {
-  if (size>10*1024*1024) {
-    klee_warning_once(0, "failing large alloc: %u bytes", (unsigned) size);
-    return 0;
-  }
+  if (size>10*1024*1024)
+    klee_warning_once(0, "Large alloc: %u bytes.  KLEE may run out of memory.", (unsigned) size);
+  
   uint64_t address = (uint64_t) (unsigned long) malloc((unsigned) size);
   if (!address)
     return 0;
diff --git a/test/Feature/ReallocFailure.c b/test/Feature/Realloc.c
index e5105c33..a47adad6 100644
--- a/test/Feature/ReallocFailure.c
+++ b/test/Feature/Realloc.c
@@ -1,5 +1,6 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
 // RUN: %klee --exit-on-error %t1.bc
+// RUN: grep "KLEE: WARNING ONCE: Large alloc" klee-last/warnings.txt
 
 #include <assert.h>
 #include <stdlib.h>
@@ -11,8 +12,7 @@ int main() {
   p[1] = 52;
 
   int *p2 = realloc(p, 1<<30);
-  assert(p2 == 0);
-  assert(p[1] == 52);
+  assert(p2[1] == 52);
 
   return 0;
 }