summaryrefslogtreecommitdiff
path: root/src/context/context_mm.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/context/context_mm.h')
-rw-r--r--src/context/context_mm.h26
1 files changed, 13 insertions, 13 deletions
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index c4e5aba4f..04b0c8167 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -25,17 +25,16 @@
namespace CVC4 {
namespace context {
-
- /**
- * Region-based memory manager for contexts. Calls to newData provide memory
- * from the current region. This memory will persist until the entire
- * region is deallocated (by calling pop).
- *
- * If push is called, the current region is deactivated and pushed on a
- * stack, and a new current region is created. A subsequent call to pop
- * releases the new region and restores the top region from the stack.
- *
- */
+/**
+ * Region-based memory manager for contexts. Calls to newData provide memory
+ * from the current region. This memory will persist until the entire
+ * region is deallocated (by calling pop).
+ *
+ * If push is called, the current region is deactivated and pushed on a
+ * stack, and a new current region is created. A subsequent call to pop
+ * releases the new region and restores the top region from the stack.
+ *
+ */
class ContextMemoryManager {
/**
@@ -102,6 +101,7 @@ class ContextMemoryManager {
void newChunk();
public:
+
/**
* Constructor - creates an initial region and an empty stack
*/
@@ -110,7 +110,7 @@ class ContextMemoryManager {
/**
* Destructor - deletes all memory in all regions
*/
- ~ContextMemoryManager();
+ ~ContextMemoryManager() throw();
/**
* Allocate size bytes from the current region
@@ -128,7 +128,7 @@ class ContextMemoryManager {
*/
void pop();
-}; /* class ContextMemoryManager */
+};/* class ContextMemoryManager */
}/* CVC4::context namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback