diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index 7f6c92b77..791b2eed0 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -1267,6 +1267,12 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,
 
   unsigned size = 0;
   bool external = false;
+  // Whether `size` is this object's real size. It is not for an external
+  // declaration, whose definition we cannot see, nor for an unsized type;
+  // both fall back to a placeholder below. An object whose type is sized but
+  // empty -- a zero-length array, an empty struct -- has a real size of zero,
+  // which has to be told apart from those two cases.
+  bool sizeKnown = false;
 
   if (v->isThreadLocal())
     ax.push_back(Attr::attr("treadLocal"));
@@ -1281,15 +1287,19 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,
       if (const PointerType *t = dyn_cast<const PointerType>(g->getType())) {
 
         // in case we can determine the size of the element type ...
-        if (t->getPointerElementType()->isSized())
+        if (t->getPointerElementType()->isSized()) {
           size = storageSize(t->getPointerElementType());
+          sizeKnown = true;
+        }
 
         // otherwise (e.g. for function declarations), use a default size
         else
           size = 1024;
 
-      } else
+      } else {
         size = storageSize(g->getType());
+        sizeKnown = true;
+      }
 
       if (!g->hasName() || !STRING_CONSTANT.match(g->getName().str())) {
         if (numElems > 1)
@@ -1303,22 +1313,28 @@ std::list<Decl *> SmackRep::globalDecl(const llvm::GlobalValue *v,
 
   decls.push_back(Decl::constant(name, Naming::PTR_TYPE, ax, false));
 
-  if (!size)
-    size = targetData->getPrefTypeAlignment(v->getType());
+  // Reserving address space and recording the object's size are two different
+  // jobs, and they part company for an object with no bytes: it still needs an
+  // address of its own, distinct from every other object, but every access to
+  // it is out of bounds. Give it the type's alignment to sit in and record its
+  // size as it is.
+  unsigned reserved =
+      size ? size : targetData->getPrefTypeAlignment(v->getType());
 
   // Add padding between globals to be able to check memory overflows/underflows
   const unsigned globalsPadding = 1024;
   if (external) {
     decls.push_back(Decl::axiom(Expr::eq(
         Expr::id(name), Expr::fn("$add.ref", Expr::id(Naming::GLOBALS_BOTTOM),
-                                 pointerLit(externsOffset -= size)))));
+                                 pointerLit(externsOffset -= reserved)))));
   } else {
-    decls.push_back(Decl::axiom(Expr::eq(
-        Expr::id(name), pointerLit(globalsOffset -= (size + globalsPadding)))));
+    decls.push_back(Decl::axiom(
+        Expr::eq(Expr::id(name),
+                 pointerLit(globalsOffset -= (reserved + globalsPadding)))));
   }
 
   if (!llvm::isa<Function>(v) && allocate)
-    globalAllocations[v] = size;
+    globalAllocations[v] = sizeKnown ? size : reserved;
 
   return decls;
 }
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index 5cb4e212c..e20f66d26 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -1649,13 +1649,25 @@ void __SMACK_decls(void) {
   D("function $base(ref) returns (ref);");
   D("var $allocatedCounter: int;\n");
 
+  // A request of size zero is a real allocation. We adopt the SV-COMP rule
+  // (sv-comp.sosy-lab.org, rules.php, "Definitions": "We assume that the
+  // functions malloc and alloca always return a valid pointer, i.e., the
+  // memory allocation never fails"), which conforms to the C standard: C11
+  // (ISO/IEC 9899:2011, N1570) 7.22.3 paragraph 1 leaves malloc(0)
+  // implementation-defined, "either a null pointer is returned, or the
+  // behavior is as if the size were some nonzero value, except that the
+  // returned pointer shall not be used to access an object", and the rule
+  // selects the second behavior. So every $$alloc below reserves address
+  // space for a size-zero request as if the size were one (the pointer is
+  // nonzero and distinct from every other object), records size zero (any
+  // access is an invalid dereference), and the block is freed and tracked
+  // like any other; before this the default model left the result
+  // unassigned, i.e. an arbitrary pointer.
   D("procedure $malloc(n: ref) returns (p: ref)\n"
     "modifies $allocatedCounter;\n"
     "{\n"
     "  call corral_atomic_begin();\n"
-    "  if ($ne.ref.bool(n, $0.ref)) {\n"
-    "    $allocatedCounter := $allocatedCounter + 1;\n"
-    "  }\n"
+    "  $allocatedCounter := $allocatedCounter + 1;\n"
     "  call p := $$alloc(n);\n"
     "  call corral_atomic_end();\n"
     "}\n");
@@ -1670,6 +1682,7 @@ void __SMACK_decls(void) {
   D("procedure $galloc(base_addr: ref, size: ref)\n"
     "{\n"
     "  assume $Size(base_addr) == size;\n"
+    "  assume $base(base_addr) == base_addr;\n"
     "  assume (forall addr: ref :: {:qid \"smack.galloc.base\"} {$base(addr)} "
     "$sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, "
     "size)) ==> $base(addr) == base_addr);\n"
@@ -1680,18 +1693,18 @@ void __SMACK_decls(void) {
     "modifies $Alloc, $CurrAddr;\n"
     "{\n"
     "  assume $sle.ref.bool($0.ref, n);\n"
-    "  if ($slt.ref.bool($0.ref, n)) {\n"
-    "    p := $CurrAddr;\n"
-    "    havoc $CurrAddr;\n"
-    "    assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
-    "    assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
+    "  p := $CurrAddr;\n"
+    "  havoc $CurrAddr;\n"
+    "  assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
+    "  assume $sgt.ref.bool($CurrAddr, p);\n"
+    "  assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
     "$MALLOC_TOP);\n"
-    "    assume $Size(p) == n;\n"
-    "    assume (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
+    "  assume $Size(p) == n;\n"
+    "  assume $base(p) == p;\n"
+    "  assume (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
     "$sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == "
     "p);\n"
-    "    $Alloc[p] := true;\n"
-    "  }\n"
+    "  $Alloc[p] := true;\n"
     "}\n");
 
   D("procedure $free(p: ref)\n"
@@ -1717,6 +1730,7 @@ void __SMACK_decls(void) {
   D("procedure $galloc(base_addr: ref, size: ref);\n"
     "modifies $Alloc, $Size;\n"
     "ensures $Size[base_addr] == size;\n"
+    "ensures $base(base_addr) == base_addr;\n"
     "ensures (forall addr: ref :: {:qid \"smack.galloc.base\"} {$base(addr)} "
     "$sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, "
     "size)) ==> $base(addr) == base_addr);\n"
@@ -1729,17 +1743,17 @@ void __SMACK_decls(void) {
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
     "modifies $Alloc, $Size;\n"
     "ensures $sle.ref.bool($0.ref, n);\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> $slt.ref.bool($0.ref, p) && "
-    "$slt.ref.bool(p, $sub.ref($MALLOC_TOP, n));\n"
-    "ensures $eq.ref.bool(n, $0.ref) ==> p == $0.ref;\n"
+    "ensures $slt.ref.bool($0.ref, p) && $slt.ref.bool(p, "
+    "$sub.ref($MALLOC_TOP, n));\n"
     "ensures !old($Alloc[p]);\n"
     "ensures (forall q: ref :: {:qid \"smack.alloc.disjoint\"} old($Alloc[q]) "
     "==> ($slt.ref.bool($add.ref(p, n), q) || $slt.ref.bool($add.ref(q, "
     "$Size[q]), p)));\n"
     "ensures $Alloc[p];\n"
     "ensures $Size[p] == n;\n"
-    "ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} "
-    "q != p ==> $Size[q] == old($Size[q]));\n"
+    "ensures $base(p) == p;\n"
+    "ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} q "
+    "!= p ==> $Size[q] == old($Size[q]));\n"
     "ensures (forall q: ref :: {:qid \"smack.alloc.frame.alloc\"} {$Alloc[q]} "
     "q != p ==> $Alloc[q] == old($Alloc[q]));\n"
     "ensures (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
@@ -1754,6 +1768,9 @@ void __SMACK_decls(void) {
     "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: "
     "{:qid \"smack.free.frame.alloc\"} {$Alloc[q]} q != p ==> $Alloc[q] == "
     "old($Alloc[q]));\n"
+    "ensures $eq.ref.bool(p, $0.ref) ==> (forall q: ref :: "
+    "{:qid \"smack.free.null.frame.alloc\"} {$Alloc[q]} $Alloc[q] == "
+    "old($Alloc[q]));\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == "
     "old($allocatedCounter) - 1;\n"
     "ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == "
@@ -1769,6 +1786,7 @@ void __SMACK_decls(void) {
   D("procedure $galloc(base_addr: ref, size: ref);\n"
     "modifies $Alloc;\n"
     "ensures $Size(base_addr) == size;\n"
+    "ensures $base(base_addr) == base_addr;\n"
     "ensures (forall addr: ref :: {:qid \"smack.galloc.base\"} {$base(addr)} "
     "$sle.ref.bool(base_addr, addr) && $slt.ref.bool(addr, $add.ref(base_addr, "
     "size)) ==> $base(addr) == base_addr);\n"
@@ -1779,18 +1797,17 @@ void __SMACK_decls(void) {
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
     "modifies $Alloc, $CurrAddr;\n"
     "ensures $sle.ref.bool($0.ref, n);\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> $sge.ref.bool($sub.ref($CurrAddr, "
-    "n), old($CurrAddr)) && p == old($CurrAddr);\n"
+    "ensures $sge.ref.bool($sub.ref($CurrAddr, n), old($CurrAddr));\n"
+    "ensures $sgt.ref.bool($CurrAddr, old($CurrAddr));\n"
+    "ensures p == old($CurrAddr);\n"
     "ensures $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
     "$MALLOC_TOP);\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> $Size(p) == n;\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> (forall q: ref :: "
-    "{:qid \"smack.alloc.base\"} {$base(q)} $sle.ref.bool(p, q) && "
-    "$slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == p);\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> $Alloc[p];\n"
-    "ensures $eq.ref.bool(n, $0.ref) ==> old($CurrAddr) == $CurrAddr && p == "
-    "$0.ref;\n"
-    "ensures $eq.ref.bool(n, $0.ref)==> $Alloc[p] == old($Alloc)[p];\n"
+    "ensures $Size(p) == n;\n"
+    "ensures $base(p) == p;\n"
+    "ensures (forall q: ref :: {:qid \"smack.alloc.base\"} {$base(q)} "
+    "$sle.ref.bool(p, q) && $slt.ref.bool(q, $add.ref(p, n)) ==> $base(q) == "
+    "p);\n"
+    "ensures $Alloc[p];\n"
     "ensures (forall q: ref :: {:qid \"smack.alloc.frame.alloc\"} {$Alloc[q]} "
     "q != p ==> $Alloc[q] == old($Alloc[q]));\n");
 
@@ -1802,6 +1819,9 @@ void __SMACK_decls(void) {
     "ensures $ne.ref.bool(p, $0.ref) ==> (forall q: ref :: "
     "{:qid \"smack.free.frame.alloc\"} {$Alloc[q]} q != p ==> $Alloc[q] == "
     "old($Alloc[q]));\n"
+    "ensures $eq.ref.bool(p, $0.ref) ==> (forall q: ref :: "
+    "{:qid \"smack.free.null.frame.alloc\"} {$Alloc[q]} $Alloc[q] == "
+    "old($Alloc[q]));\n"
     "ensures $ne.ref.bool(p, $0.ref) ==> $allocatedCounter == "
     "old($allocatedCounter) - 1;\n"
     "ensures $eq.ref.bool(p, $0.ref) ==> $allocatedCounter == "
@@ -1819,17 +1839,17 @@ void __SMACK_decls(void) {
 #if MEMORY_MODEL_NO_REUSE_IMPLS
   D("var $CurrAddr:ref;\n");
 
+  // Size zero: see the memory-safety $malloc above.
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n"
     "modifies $CurrAddr;\n"
     "{\n"
     "  assume $sge.ref.bool(n, $0.ref);\n"
-    "  if ($sgt.ref.bool(n, $0.ref)) {\n"
-    "    p := $CurrAddr;\n"
-    "    havoc $CurrAddr;\n"
-    "    assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
-    "    assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
+    "  p := $CurrAddr;\n"
+    "  havoc $CurrAddr;\n"
+    "  assume $sge.ref.bool($sub.ref($CurrAddr, n), p);\n"
+    "  assume $sgt.ref.bool($CurrAddr, p);\n"
+    "  assume $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
     "$MALLOC_TOP);\n"
-    "  }\n"
     "}\n");
 
   D("procedure $free(p: ref);\n");
@@ -1841,17 +1861,16 @@ void __SMACK_decls(void) {
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
     "modifies $Alloc, $Size;\n"
     "ensures $sle.ref.bool($0.ref, n);\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> $slt.ref.bool($0.ref, p) && "
-    "$slt.ref.bool(p, $sub.ref($MALLOC_TOP, n));\n"
-    "ensures $eq.ref.bool(n, $0.ref) ==> p == $0.ref;\n"
+    "ensures $slt.ref.bool($0.ref, p) && $slt.ref.bool(p, "
+    "$sub.ref($MALLOC_TOP, n));\n"
     "ensures !old($Alloc[p]);\n"
     "ensures (forall q: ref :: {:qid \"smack.alloc.disjoint\"} old($Alloc[q]) "
     "==> ($slt.ref.bool($add.ref(p, n), q) || $slt.ref.bool($add.ref(q, "
     "$Size[q]), p)));\n"
     "ensures $Alloc[p];\n"
     "ensures $Size[p] == n;\n"
-    "ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} "
-    "q != p ==> $Size[q] == old($Size[q]));\n"
+    "ensures (forall q: ref :: {:qid \"smack.alloc.frame.size\"} {$Size[q]} q "
+    "!= p ==> $Size[q] == old($Size[q]));\n"
     "ensures (forall q: ref :: {:qid \"smack.alloc.frame.alloc\"} {$Alloc[q]} "
     "q != p ==> $Alloc[q] == old($Alloc[q]));\n");
 
@@ -1867,12 +1886,11 @@ void __SMACK_decls(void) {
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
     "modifies $CurrAddr;\n"
     "ensures $sle.ref.bool($0.ref, n);\n"
-    "ensures $slt.ref.bool($0.ref, n) ==> $sge.ref.bool($sub.ref($CurrAddr, "
-    "n), old($CurrAddr)) && p == old($CurrAddr);\n"
+    "ensures $sge.ref.bool($sub.ref($CurrAddr, n), old($CurrAddr));\n"
+    "ensures $sgt.ref.bool($CurrAddr, old($CurrAddr));\n"
+    "ensures p == old($CurrAddr);\n"
     "ensures $sgt.ref.bool($CurrAddr, $0.ref) && $slt.ref.bool($CurrAddr, "
-    "$MALLOC_TOP);\n"
-    "ensures $eq.ref.bool(n, $0.ref) ==> old($CurrAddr) == $CurrAddr && p == "
-    "$0.ref;\n");
+    "$MALLOC_TOP);\n");
 
   D("procedure $free(p: ref);\n");
 #endif
diff --git a/share/smack/lib/stdlib.c b/share/smack/lib/stdlib.c
index 99a12cc90..b2b7393e1 100644
--- a/share/smack/lib/stdlib.c
+++ b/share/smack/lib/stdlib.c
@@ -36,6 +36,24 @@ void *calloc(size_t num, size_t size) {
   return ret;
 }
 
+// realloc is modelled as free followed by malloc, which gives the two
+// boundary cases their C11 meaning through the allocation procedures in
+// smack.c rather than by special-casing them here:
+//
+//   realloc(NULL, n) is malloc(n), because free(NULL) is a no-op (7.22.3.3).
+//   realloc(p, 0) frees p and returns a size-zero block. Under the rule
+//   adopted in smack.c -- allocation never fails, and a size-zero request
+//   behaves "as if the size were some nonzero value, except that the
+//   returned pointer shall not be used to access an object" (7.22.3p1) --
+//   that block is a real allocation: it is not null, it may not be
+//   dereferenced, and it must be freed. So a program that drops the result
+//   of realloc(p, 0) leaks it, which test/c/memory-safety/
+//   realloc_zero_leak_fail.c pins. glibc instead frees p and returns null,
+//   and C23 makes the call undefined, so code that uses realloc(p, 0) as a
+//   spelling of free() is reported as a leak here; write free(p) instead.
+//
+// What this model does not do is preserve the contents of the old block
+// across the call, which 7.22.3.5p2 requires.
 void *realloc(void *ptr, size_t size) {
   void *ret;
   __VERIFIER_atomic_begin();
diff --git a/test/c/basic/global_zero.c b/test/c/basic/global_zero.c
new file mode 100644
index 000000000..9c539b8be
--- /dev/null
+++ b/test/c/basic/global_zero.c
@@ -0,0 +1,17 @@
+#include "smack.h"
+
+// @expect verified
+
+// A global with no bytes still gets an address distinct from every other
+// object's.
+int g[0];
+int h[2];
+int k;
+
+int main(void) {
+  __VERIFIER_assert((char *)g != (char *)h);
+  __VERIFIER_assert((char *)g != (char *)&k);
+  h[0] = 7;
+  __VERIFIER_assert(h[0] == 7);
+  return 0;
+}
diff --git a/test/c/basic/malloc_zero.c b/test/c/basic/malloc_zero.c
new file mode 100644
index 000000000..34e002683
--- /dev/null
+++ b/test/c/basic/malloc_zero.c
@@ -0,0 +1,21 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect verified
+
+// Without memory-safety checks the result of malloc(0) is still a fresh
+// non-null pointer, distinct from every other allocation, under every
+// memory model.
+int main(void) {
+  char *p = malloc(0);
+  char *q = malloc(0);
+  int *r = malloc(sizeof(int));
+  __VERIFIER_assert(p != 0);
+  __VERIFIER_assert(q != 0);
+  __VERIFIER_assert(p != q);
+  __VERIFIER_assert((void *)p != (void *)r);
+  free(p);
+  free(q);
+  free(r);
+  return 0;
+}
diff --git a/test/c/basic/malloc_zero_fail.c b/test/c/basic/malloc_zero_fail.c
new file mode 100644
index 000000000..4a6107eca
--- /dev/null
+++ b/test/c/basic/malloc_zero_fail.c
@@ -0,0 +1,10 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+int main(void) {
+  char *p = malloc(0);
+  __VERIFIER_assert(p == 0); // malloc(0) does not return a null pointer
+  return 0;
+}
diff --git a/test/c/memory-safety/alloca_zero_deref_fail.c b/test/c/memory-safety/alloca_zero_deref_fail.c
new file mode 100644
index 000000000..00a7a0b4c
--- /dev/null
+++ b/test/c/memory-safety/alloca_zero_deref_fail.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+// A variable-length array of length zero is a size-zero stack allocation;
+// SV-COMP's rule covers alloca as well as malloc.
+int main(void) {
+  unsigned n = __VERIFIER_nondet_unsigned();
+  __VERIFIER_assume(n == 0);
+  char a[n];
+  a[0] = 1;
+  return 0;
+}
diff --git a/test/c/memory-safety/calloc_zero_deref_fail.c b/test/c/memory-safety/calloc_zero_deref_fail.c
new file mode 100644
index 000000000..7115cd56f
--- /dev/null
+++ b/test/c/memory-safety/calloc_zero_deref_fail.c
@@ -0,0 +1,13 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+// calloc(0, n) allocates zero bytes (SMACK's calloc may also fail, and a
+// null dereference is invalid too).
+int main(void) {
+  int *p = calloc(0, sizeof(int));
+  p[0] = 1;
+  free(p);
+  return 0;
+}
diff --git a/test/c/memory-safety/free_null_then_free.c b/test/c/memory-safety/free_null_then_free.c
new file mode 100644
index 000000000..71716ccc0
--- /dev/null
+++ b/test/c/memory-safety/free_null_then_free.c
@@ -0,0 +1,19 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect verified
+
+// free(NULL) is a no-op (C11 7.22.3.3) and must leave every other block
+// allocated; the spec-only $free of the reuse and no-reuse models used to
+// frame $Alloc only for a non-null argument, so the free of p or q below
+// failed its precondition. realloc(NULL, n) is the same idiom.
+int main(void) {
+  int *p = malloc(sizeof(int));
+  *p = 1;
+  free(0);
+  int *q = realloc(0, sizeof(int));
+  *q = 2;
+  free(p);
+  free(q);
+  return 0;
+}
diff --git a/test/c/memory-safety/global_zero_deref_fail.c b/test/c/memory-safety/global_zero_deref_fail.c
new file mode 100644
index 000000000..614a7d22d
--- /dev/null
+++ b/test/c/memory-safety/global_zero_deref_fail.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+
+// @expect error
+
+// A global with no bytes -- here a zero-length array -- has an address of
+// its own but no byte that may be accessed, exactly like a size-zero heap
+// block.
+int g[0];
+int h[2];
+
+int main(void) {
+  g[0] = 1;
+  return h[0];
+}
diff --git a/test/c/memory-safety/global_zero_no_access.c b/test/c/memory-safety/global_zero_no_access.c
new file mode 100644
index 000000000..b26977feb
--- /dev/null
+++ b/test/c/memory-safety/global_zero_no_access.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+
+// @expect verified
+
+// Its neighbours stay accessible: giving the empty object a real size of
+// zero must not disturb the objects placed around it.
+int g[0];
+int h[2];
+
+int main(void) {
+  h[0] = 1;
+  h[1] = 2;
+  return h[0] + h[1];
+}
diff --git a/test/c/memory-safety/malloc_nondet.c b/test/c/memory-safety/malloc_nondet.c
index 9741ab826..c6f88667c 100644
--- a/test/c/memory-safety/malloc_nondet.c
+++ b/test/c/memory-safety/malloc_nondet.c
@@ -5,7 +5,7 @@
 
 int main(void) {
   int x = __VERIFIER_nondet_int();
-  assume(x != 0); // malloc(0) can return anything
+  assume(x > 0); // p[x - 1] needs at least one byte
   char *p = (char *)malloc(x);
   p[x - 1] = x;
   free(p);
diff --git a/test/c/memory-safety/malloc_nondet_fail.c b/test/c/memory-safety/malloc_nondet_fail.c
index 52214619c..aeb008ff5 100644
--- a/test/c/memory-safety/malloc_nondet_fail.c
+++ b/test/c/memory-safety/malloc_nondet_fail.c
@@ -5,7 +5,7 @@
 
 int main(void) {
   int x = __VERIFIER_nondet_int();
-  assume(x != 0); // malloc(0) can return anything
+  assume(x > 0); // p[x - 1] needs at least one byte
   char *p = (char *)malloc(x);
   p[x] = x;
   free(p);
diff --git a/test/c/memory-safety/malloc_zero.c b/test/c/memory-safety/malloc_zero.c
new file mode 100644
index 000000000..06e9cfdb1
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero.c
@@ -0,0 +1,19 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect verified
+
+// malloc(0) never fails (SV-COMP) and, per C11 7.22.3, behaves as if the
+// size were nonzero except that the pointer must not be used to access an
+// object: freeing it is valid (basic/malloc_zero.c checks it is non-null
+// and distinct; assertions are not checked under --check=memory-safety).
+int main(void) {
+  char *p = malloc(0);
+  char *q = malloc(0);
+  char *r = malloc(1);
+  r[0] = 1;
+  free(p);
+  free(q);
+  free(r);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_deref_fail.c b/test/c/memory-safety/malloc_zero_deref_fail.c
new file mode 100644
index 000000000..9fda3745f
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_deref_fail.c
@@ -0,0 +1,11 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+int main(void) {
+  char *p = malloc(0);
+  p[0] = 1; // a size-zero block cannot be accessed
+  free(p);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_freed.c b/test/c/memory-safety/malloc_zero_freed.c
new file mode 100644
index 000000000..b2f9b5600
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_freed.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @flag --check=memleak
+// @expect verified
+
+int main(void) {
+  char *p = malloc(0);
+  char *q = calloc(0, 4);
+  free(p);
+  if (q != 0)
+    free(q);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_leak_fail.c b/test/c/memory-safety/malloc_zero_leak_fail.c
new file mode 100644
index 000000000..618befab0
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_leak_fail.c
@@ -0,0 +1,10 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @flag --check=memleak
+// @expect error
+
+int main(void) {
+  char *p = malloc(0);
+  return 0; // a size-zero block is allocated memory and must be freed
+}
diff --git a/test/c/memory-safety/malloc_zero_memcpy_in_fail.c b/test/c/memory-safety/malloc_zero_memcpy_in_fail.c
new file mode 100644
index 000000000..b25022937
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_memcpy_in_fail.c
@@ -0,0 +1,13 @@
+#include "smack.h"
+#include <stdlib.h>
+#include <string.h>
+
+// @expect error
+
+int main(void) {
+  char src[1] = {1};
+  char *p = malloc(0);
+  memcpy(p, src, 1); // one byte into a block with none
+  free(p);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_memcpy_out_fail.c b/test/c/memory-safety/malloc_zero_memcpy_out_fail.c
new file mode 100644
index 000000000..7a78b9060
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_memcpy_out_fail.c
@@ -0,0 +1,13 @@
+#include "smack.h"
+#include <stdlib.h>
+#include <string.h>
+
+// @expect error
+
+int main(void) {
+  char dst[1];
+  char *p = malloc(0);
+  memcpy(dst, p, 1); // one byte out of a block with none
+  free(p);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_memset_fail.c b/test/c/memory-safety/malloc_zero_memset_fail.c
new file mode 100644
index 000000000..1f6160e1c
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_memset_fail.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+#include <stdlib.h>
+#include <string.h>
+
+// @expect error
+
+// A one-byte memset touches the block; a library call is checked like a
+// direct access.
+int main(void) {
+  char *p = malloc(0);
+  memset(p, 0, 1);
+  free(p);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_no_access.c b/test/c/memory-safety/malloc_zero_no_access.c
new file mode 100644
index 000000000..f89dbc8a0
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_no_access.c
@@ -0,0 +1,21 @@
+#include "smack.h"
+#include <stdlib.h>
+#include <string.h>
+
+// @expect verified
+
+// Operations that touch no byte of the block are valid: zero-length memset
+// and memcpy in either direction, forming p + 0, comparing the pointer.
+int main(void) {
+  char *p = malloc(0);
+  char *q = malloc(4);
+  memset(p, 0, 0);
+  memcpy(q, p, 0);
+  memcpy(p, q, 0);
+  char *end = p + 0;
+  if (end == q)
+    q[0] = 1;
+  free(p);
+  free(q);
+  return 0;
+}
diff --git a/test/c/memory-safety/malloc_zero_read_fail.c b/test/c/memory-safety/malloc_zero_read_fail.c
new file mode 100644
index 000000000..2a6072857
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_read_fail.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+// Reading from a size-zero block is as invalid as writing to it.
+int main(void) {
+  char *p = malloc(0);
+  char c = p[0];
+  free(p);
+  return c;
+}
diff --git a/test/c/memory-safety/malloc_zero_wide_deref_fail.c b/test/c/memory-safety/malloc_zero_wide_deref_fail.c
new file mode 100644
index 000000000..9812535b2
--- /dev/null
+++ b/test/c/memory-safety/malloc_zero_wide_deref_fail.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+// A wider access does not change the picture: the block has no bytes.
+int main(void) {
+  int *p = malloc(0);
+  *p = 1;
+  free(p);
+  return 0;
+}
diff --git a/test/c/memory-safety/realloc_grow_zero.c b/test/c/memory-safety/realloc_grow_zero.c
new file mode 100644
index 000000000..505438482
--- /dev/null
+++ b/test/c/memory-safety/realloc_grow_zero.c
@@ -0,0 +1,13 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect verified
+
+// Growing a size-zero block through realloc yields an ordinary block.
+int main(void) {
+  char *p = malloc(0);
+  char *q = realloc(p, 4);
+  q[3] = 1;
+  free(q);
+  return 0;
+}
diff --git a/test/c/memory-safety/realloc_zero_deref_fail.c b/test/c/memory-safety/realloc_zero_deref_fail.c
new file mode 100644
index 000000000..1e17f04f4
--- /dev/null
+++ b/test/c/memory-safety/realloc_zero_deref_fail.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @expect error
+
+// realloc(p, 0) frees p and returns a size-zero block; neither the old
+// pointer nor the new one may be accessed.
+int main(void) {
+  char *p = malloc(4);
+  char *q = realloc(p, 0);
+  q[0] = 1;
+  free(q);
+  return 0;
+}
diff --git a/test/c/memory-safety/realloc_zero_freed.c b/test/c/memory-safety/realloc_zero_freed.c
new file mode 100644
index 000000000..b807bfef4
--- /dev/null
+++ b/test/c/memory-safety/realloc_zero_freed.c
@@ -0,0 +1,16 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @flag --check=memleak
+// @expect verified
+
+// Freeing the size-zero block realloc(p, 0) returns, and the one
+// realloc(NULL, 0) returns, accounts for both.
+int main(void) {
+  char *p = malloc(4);
+  char *q = realloc(p, 0);
+  char *r = realloc(0, 0);
+  free(q);
+  free(r);
+  return 0;
+}
diff --git a/test/c/memory-safety/realloc_zero_leak_fail.c b/test/c/memory-safety/realloc_zero_leak_fail.c
new file mode 100644
index 000000000..244511193
--- /dev/null
+++ b/test/c/memory-safety/realloc_zero_leak_fail.c
@@ -0,0 +1,16 @@
+#include "smack.h"
+#include <stdlib.h>
+
+// @flag --check=memleak
+// @expect error
+
+// realloc(p, 0) frees p and returns a size-zero block, which is a real
+// allocation and must itself be freed; using the call as a spelling of
+// free() leaks that block. See the comment on realloc in
+// share/smack/lib/stdlib.c.
+int main(void) {
+  char *p = malloc(4);
+  p[0] = 1;
+  realloc(p, 0);
+  return 0;
+}