projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
fix conflicts
[model-checker.git]
/
mymemory.h
diff --git
a/mymemory.h
b/mymemory.h
index 05b89be959e0872386d955ebffd09b3b4076ffae..f2a31865ba85a9272794514de14e3179bb2da01e 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);