Checks for mspace move

src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h

@@ -54,6 +54,7 @@ static struct memory_spaces {
   mspace heap_mspace;  /* `public` (application) mspace */
   uintptr_t heap_start; /* least address in application mspace */
   uintptr_t heap_end; /* greatest address in application mspace */
+  uintptr_t heap_mspace_least; /* Initial least address in heap mspace */
 } mem_spaces;
 
 /* While it is possible to generate prefixes using an extra level of
@@ -125,6 +126,9 @@ static void make_memory_spaces(size_t rtl_size, size_t heap_size) {
      mspace header. */
   mem_spaces.heap_start = (uintptr_t)mspace_malloc(mem_spaces.heap_mspace,1);
   mem_spaces.heap_end = mem_spaces.heap_start + heap_size;
+  /* Save initial least address of heap memspace. This address is used later
+     to check whether memspace has been moved. */
+  mem_spaces.heap_mspace_least = (uintptr_t)mspace_least_addr(mem_spaces.heap_mspace);
 }
 
 static void destroy_memory_spaces() {

src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h

@@ -833,6 +833,15 @@ static void mark_readonly_region (uintptr_t addr, long size) {
 static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
     size_t init, const char *function) {
 
+  /* Make sure that heap memspace has not been moved. This is likely if
+     a really large chunk has been requested to be allocated. */
+  vassert(mem_spaces.heap_mspace_least ==
+    (uintptr_t)mspace_least_addr(mem_spaces.heap_mspace),
+    "Exceeded heap allocation limit of %luMB -- heap memory space moved. \n",
+    E_ACSL_HEAP_SIZE);
+
+  /* Similar check, make sure that allocated space does not exceed given
+     allocation limit for mspace */
   uintptr_t max_addr = (uintptr_t)ptr + alloc_size;
   vassert(mem_spaces.heap_end > max_addr,
     "Exceeded heap allocation limit of %luMB\n", E_ACSL_HEAP_SIZE);