#define ENOMEM      12  /* Out of memory */

#define NULL (void*)0

extern void *malloc (unsigned long __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;

extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));

__attribute__ ((noinline)) int nondet() { return 42; }

extern void *memcpy (void *__restrict __dest, const void *__restrict __src,
       unsigned long __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));

#define refptr(mod) (mod[0])
#define module_core(mod) (mod[1])

int load_module()
{
  void *hdr;
  void **mod;
  long err = 0;
  void *ptr = NULL;
	
  if ((hdr = malloc(2*sizeof(void*))) == NULL) // (2)
    return -ENOMEM;
	
  mod = (void *)hdr; // (3)

#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP) 
  refptr(mod) = malloc(32);
  if (!refptr(mod))
  {
    err = -ENOMEM;
    goto free_mod;
  }
#endif

  ptr = malloc(512); // (4)
  if (!ptr) {
    err = -ENOMEM;
    goto free_percpu;
  }
  module_core(mod) = ptr; // (5)
  
  while (nondet()) {
    void *dest = module_core(mod); // (6)
    memcpy(dest, mod, sizeof(2*sizeof(void*))); // (7)
    mod = module_core(mod); // (8) `mod' and `module_core(mod)' are aliases
    if (nondet())
      break;
  }

  if (nondet())
    goto free_unload; // (9)

  return 0;

  free_unload:
  free_core:
    free(module_core(mod)); // (10) frees `module_core(mod)' and thus `mod' too
  free_percpu:
#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP)
    free(refptr(mod)); // (11) ERROR: dereferencing already freed `mod'.
#endif
  free_mod:
  free_hdr:
    free(hdr);

  return err;
}

int main(void) {
  load_module(); // (1)
  return 0;
}

diff --git a/simple/6e2b757.c b/simple/6e2b757.c
--- a/simple/6e2b757.c
+++ b/simple/6e2b757.c
@@ -27,15 +27,6 @@
 	
   mod = (void *)hdr; // (3)
 
-#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP) 
-  refptr(mod) = malloc(32);
-  if (!refptr(mod))
-  {
-    err = -ENOMEM;
-    goto free_mod;
-  }
-#endif
-
   ptr = malloc(512); // (4)
   if (!ptr) {
     err = -ENOMEM;
@@ -51,18 +42,28 @@
       break;
   }
 
+#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP) 
+  refptr(mod) = malloc(32);
+  if (!refptr(mod))
+  {
+    err = -ENOMEM;
+    goto free_init;
+  }
+#endif
+
   if (nondet())
     goto free_unload; // (9)
 
   return 0;
 
   free_unload:
+  free_init:
+#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP)
+    free(refptr(mod)); // (11) ERROR: dereferencing already freed `mod'.
+#endif
   free_core:
     free(module_core(mod)); // (10) frees `module_core(mod)' and thus `mod' too
   free_percpu:
-#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP)
-    free(refptr(mod)); // (11) ERROR: dereferencing already freed `mod'.
-#endif
   free_mod:
   free_hdr:
     free(hdr);

#include <errno.h>
#include <stdlib.h>
#include <string.h>

struct module {
  void *refptr;
  void *module_core;
};

int main(int argc, char** argv) {
//  load_module(64 * 1024);
  void *hdr;
  struct module *mod;
  long err = 0;
  void *ptr = NULL;
	
  if ((hdr = malloc(len)) == NULL)
    return -ENOMEM;
	
  mod = (void *)hdr;

#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP)
  mod->refptr = malloc(32);
  if (!mod->refptr) {
    err = -ENOMEM;
    goto free_mod;
  }
#endif

  ptr = malloc(512);
  if (!ptr) {
    err = -ENOMEM;
    goto free_percpu;
  }
  mod->module_core = ptr;
  
  while (1) {
    void *dest = mod->module_core;
    memcpy(dest, mod, sizeof(struct module));
    mod = mod->module_core; 
    break;
  }

  if (rand() % 2)
    goto free_unload;

  return 0;

  free_unload:
  free_core:
    free(mod->module_core);
  free_percpu:
#if defined(CONFIG_MODULE_UNLOAD) && defined(CONFIG_SMP)
    free(mod->refptr); // ERROR
#endif
  free_mod:
  free_hdr:
    free(hdr);

  return 0;
}

. call kernel/module.c:1861:load_module()
. 1888: if (len > 64 * 1024 * 1024 || (hdr = vmalloc(len)) == NULL)
// allocates temporary memory area in hdr
. 1897: if (copy_from_user(hdr, umod, len) != 0) {
// copies module's object code from umod (user mode buffer)
. 1942: modindex = find_sec(hdr, sechdrs, secstrings,
// find the index of the '.gnu.linkonce.this_module' section, which contains an image of the module structure
. 1950: mod = (void *)sechdrs[modindex].sh_addr;
// and make mod point to it
. 2019: mod->refptr = percpu_modalloc(sizeof(local_t), __alignof__(local_t),
. 2045: ptr = module_alloc_update_bounds(mod->core_size);
. 2051: mod->module_core = ptr;
. 2053: ptr = module_alloc_update_bounds(mod->init_size);
. 2059: mod->module_init = ptr;
. 2063: for (i = 0; i < hdr->e_shnum; i++) {
// transfer sections to module_core and module_init
// mod is set to point to the modindex section.
// an init section is identified by INIT_OFFSET_MASK.
// .gnu.linkonce.this_module belongs to core.
. 2091: goto free_unload;
. 2291: module_free(mod, mod->module_init);
. 2293: module_free(mod, mod->module_core);
// mod was pointing to module_core, which is now freed
. ERROR 2298: percpu_modfree(mod->refptr);