mymemory: use the right *&^% allocator!!

[model-checker.git] / mymemory.cc

diff --git a/mymemory.cc b/mymemory.cc
index a825bb940f66f4331e723eadd8983f9bd8d05e70..11542bfa26af49c0b1f93c23841f6138b0354865 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -63,9 +63,17 @@ void free( void * ptr ){
 }
 
 void * operator new(size_t size) throw(std::bad_alloc) {
-       return MYMALLOC(size);
+       return malloc(size);
 }
 
 void operator delete(void *p) throw() {
-       MYFREE(p);
+       free(p);
+}
+
+void * operator new[](size_t size) throw(std::bad_alloc) {
+       return malloc(size);
+}
+
+void operator delete[](void *p, size_t size) {
+       free(p);
 }