projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Annotation Support
[model-checker.git]
/
mymemory.h
diff --git
a/mymemory.h
b/mymemory.h
index 05b89be959e0872386d955ebffd09b3b4076ffae..a62ab83b9ce5cbcd82999bc9463b2949ba7a0394 100644
(file)
--- a/
mymemory.h
+++ b/
mymemory.h
@@
-4,8
+4,8
@@
#ifndef _MY_MEMORY_H
#define _MY_MEMORY_H
#ifndef _MY_MEMORY_H
#define _MY_MEMORY_H
-#include <stdlib.h>
#include <limits>
#include <limits>
+#include <stddef.h>
#include "config.h"
#include "config.h"
@@
-23,6
+23,9
@@
} \
void operator delete[](void *p, size_t size) { \
model_free(p); \
} \
void operator delete[](void *p, size_t size) { \
model_free(p); \
+ } \
+ void * operator new(size_t size, void *p) { /* placement new */ \
+ return p; \
}
/** SNAPSHOTALLOC declares the allocators for a class to allocate
}
/** SNAPSHOTALLOC declares the allocators for a class to allocate
@@
-39,6
+42,9
@@
} \
void operator delete[](void *p, size_t size) { \
snapshot_free(p); \
} \
void operator delete[](void *p, size_t size) { \
snapshot_free(p); \
+ } \
+ void * operator new(size_t size, void *p) { /* placement new */ \
+ return p; \
}
void *model_malloc(size_t size);
}
void *model_malloc(size_t size);
@@
-50,6
+56,9
@@
void * snapshot_calloc(size_t count, size_t size);
void * snapshot_realloc(void *ptr, size_t size);
void snapshot_free(void *ptr);
void * snapshot_realloc(void *ptr, size_t size);
void snapshot_free(void *ptr);
+void * Thread_malloc(size_t size);
+void Thread_free(void *ptr);
+
/** @brief Provides a non-snapshotting allocator for use in STL classes.
*
* The code was adapted from a code example from the book The C++
/** @brief Provides a non-snapshotting allocator for use in STL classes.
*
* The code was adapted from a code example from the book The C++