From e35f30ccb608b930c01646aa8e0fbf6d81f731c4 Mon Sep 17 00:00:00 2001
From: Markus Blatt <markus@dr-blatt.de>
Date: Tue, 3 Jun 2014 11:25:02 +0200
Subject: [PATCH] [poolallocator] Throw bad_alloc when freeing null pointer

---
 dune/common/poolallocator.hh | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/dune/common/poolallocator.hh b/dune/common/poolallocator.hh
index 10883cef1..9a70f677d 100644
--- a/dune/common/poolallocator.hh
+++ b/dune/common/poolallocator.hh
@@ -539,8 +539,12 @@ namespace Dune
       freed->next_ = head_;
       head_ = freed;
       //--allocated_;
-    }else
+    }
+    else
+    {
       std::cerr<< "Tried to free null pointer! "<<b<<std::endl;
+      throw std::bad_alloc();
+    }
   }
 
   template<class T, std::size_t S>
-- 
GitLab