-/** The fact that I am not expecting more than a handful requests is implicit in my not using a binary search here*/
-bool DontFree( void * ptr ){
- if( howManyFreed == nextRequest ) return false; //a minor optimization to reduce the number of instructions executed on each free call....
- if( NULL == ptr ) return true;
- for( int i = nextRequest - 1; i >= 0; --i ){
- if( allocatedReqs[ i ] == ( size_t )ptr ) {
- ++howManyFreed;
- return true;
+/** @brief Global mspace reference for the model-checker's snapshotting heap */
+mspace model_snapshot_space = NULL;
+
+#if USE_MPROTECT_SNAPSHOT
+
+/** @brief Global mspace reference for the user's snapshotting heap */
+mspace user_snapshot_space = NULL;
+
+/** Check whether this is bootstrapped memory that we should not free */
+static bool DontFree(void *ptr)
+{
+ return (ptr >= (&bootstrapmemory[0]) && ptr < (&bootstrapmemory[BOOTSTRAPBYTES]));
+}
+
+/**
+ * @brief The allocator function for "user" allocation
+ *
+ * Should only be used for allocations which will not disturb the allocation
+ * patterns of a user thread.
+ */
+static void * user_malloc(size_t size)
+{
+ void *tmp = mspace_malloc(user_snapshot_space, size);
+ ASSERT(tmp);
+ return tmp;
+}
+
+/**
+ * @brief Snapshotting malloc implementation for user programs
+ *
+ * Do NOT call this function from a model-checker context. Doing so may disrupt
+ * the allocation patterns of a user thread.
+ */
+void *malloc(size_t size)
+{
+ if (user_snapshot_space) {
+ if (switch_alloc) {
+ return model_malloc(size);
+ }
+ /* Only perform user allocations from user context */
+ ASSERT(!model || thread_current());
+ return user_malloc(size);
+ } else
+ return HandleEarlyAllocationRequest(size);
+}
+
+/** @brief Snapshotting free implementation for user programs */
+void free(void * ptr)
+{
+ if (!DontFree(ptr)) {
+ if (switch_alloc) {
+ return model_free(ptr);