about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--test/Feature/MemoryLimit.c23
1 files changed, 15 insertions, 8 deletions
diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c
index 8837e2e5..fb9f2c86 100644
--- a/test/Feature/MemoryLimit.c
+++ b/test/Feature/MemoryLimit.c
@@ -1,13 +1,20 @@
+// Check that we properly kill states when we exceed our memory bounds, for both
+// small and large allocations (large allocations commonly use mmap(), which can
+// follow a separate path in the allocator and statistics reporting).
+
 // RUN: %llvmgcc -emit-llvm -DLITTLE_ALLOC -g -c %s -o %t.little.bc
-// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.big.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log
+// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log 2> %t.little.err
 // RUN: not grep -q "MALLOC FAILED" %t.little.log
-// RUN: not grep -q "MALLOC FAILED" %t.big.log
 // RUN: not grep -q "DONE" %t.little.log
+// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.little.err
+
+// RUN: %llvmgcc -emit-llvm -g -c %s -o %t.big.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err
+// RUN: not grep -q "MALLOC FAILED" %t.big.log
 // RUN: not grep -q "DONE" %t.big.log
+// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.big.err
 
 #include <stdlib.h>
 #include <stdio.h>
@@ -18,10 +25,10 @@ int main() {
 #ifdef LITTLE_ALLOC
   printf("IN LITTLE ALLOC\n");
     
-  // 200 MBs total (in 32 byte chunks)
+  // 200 MBs total (in 1k chunks)
   for (i=0; i<100 && !malloc_failed; i++) {
-    for (j=0; j<(1<<16); j++){
-      void * p = malloc(1<<5);
+    for (j=0; j<(1<<11); j++){
+      void * p = malloc(1<<10);
       malloc_failed |= (p == 0);
     }
   }