CVC3

memory_manager_malloc.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file memory_manager_malloc.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Tue Apr 19 14:30:36 2005
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  * Class MemoryManagerMalloc: default implementation of MemoryManager
00019  * using malloc().
00020  * 
00021  * Typical use of this class is to create 
00022  * MemoryManager* mm = new MemoryManager(sizeof(YourClass)); 
00023  * where YourClass has operators new and delete redefined:
00024  * void* YourClass::operator new(size_t, MemoryManager* mm)
00025  * { return mm->newData(); }
00026  * void YourClass::delete(void*) { } // do not deallocate memory here
00027  * Then, create objects with obj = new(mm) YourClass(), and destroy them with
00028  * delete obj; mm->deleteData(obj);
00029  */
00030 /*****************************************************************************/
00031 
00032 #ifndef _cvc3__memory_manager_malloc_h
00033 #define _cvc3__memory_manager_malloc_h
00034 
00035 #include "memory_manager.h"
00036 
00037 namespace CVC3 {
00038 
00039 class MemoryManagerMalloc: public MemoryManager {
00040  public:
00041   // Constructor
00042   MemoryManagerMalloc() { }
00043   // Destructor
00044   ~MemoryManagerMalloc() { }
00045 
00046   void* newData(size_t size) {
00047     return malloc(size);
00048   }
00049 
00050   void deleteData(void* d) {
00051     free(d);
00052   }
00053 }; // end of class MemoryManager
00054 
00055 }
00056 
00057 #endif