From 42c08ddfe049c6722890f0be4fdfba0bc42b3375 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 26 Aug 2026 09:14:10 -0700
Subject: [PATCH 1/3] Treat a size-zero allocation as a real, inaccessible
 block

We adopt the SV-COMP rule -- "malloc and alloca always return a valid
pointer, i.e., the memory allocation never fails" -- which conforms to the
C standard: C11 7.22.3 leaves malloc(0) implementation-defined, a null
pointer or "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.

SMACK's three memory models each did something else. The default,
no-reuse-impls, only assigned the result inside `if (n > 0)`, so for a
size-zero request the out-parameter was never assigned at all and the
program continued with an arbitrary pointer: it could alias a live object,
so a store through it clobbered that object and a free of it was reported
as invalid. The other two returned a null pointer. In the reuse model that
also made the second of two malloc(0) calls unsatisfiable (the result is 0
both times, but the contract requires !old($Alloc[p])), and everything after
it was verified vacuously. The aws-c-common SV-COMP harnesses reach this
through bounded_malloc(cursor->len), bounded_malloc(cap) and
bounded_malloc(list->current_size) with unconstrained sizes.

The n > 0 guards are what gave a size-zero request that treatment, so they
go: every clause of every $$alloc now holds unconditionally. For a positive
size nothing changes -- each clause said exactly this under the guard -- and
for a size-zero request the procedure reserves address space as if the size
were one while recording size zero, so any access is an invalid dereference
under --check=memory-safety and free() is valid.

Two facts have to be stated that the guarded text could not: $CurrAddr
advances strictly, without which a second size-zero request could return the
same address; and $base(p) == p, which the range quantifier over [p, p + n)
cannot give when that range is empty and which $free requires. The reuse
model's disjointness clause is unchanged -- its strict < already places a
size-zero block outside every live block. $malloc counts the block, so
--check=memleak reports it when it leaks and stays balanced when it is
freed. alloca, calloc and realloc go through the same procedure, and the
comment on realloc in stdlib.c works through what the rule means for
realloc(NULL, n) and realloc(p, 0).

The two malloc_nondet tests assumed a nonzero size with a comment saying
malloc(0) "can return anything"; the assumption is really about the
p[x - 1] access and is now stated that way.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 share/smack/lib/smack.c                       | 95 ++++++++++---------
 share/smack/lib/stdlib.c                      | 18 ++++
 test/c/basic/malloc_zero.c                    | 21 ++++
 test/c/basic/malloc_zero_fail.c               | 10 ++
 test/c/memory-safety/alloca_zero_deref_fail.c | 14 +++
 test/c/memory-safety/calloc_zero_deref_fail.c | 13 +++
 test/c/memory-safety/malloc_nondet.c          |  2 +-
 test/c/memory-safety/malloc_nondet_fail.c     |  2 +-
 test/c/memory-safety/malloc_zero.c            | 19 ++++
 test/c/memory-safety/malloc_zero_deref_fail.c | 11 +++
 test/c/memory-safety/malloc_zero_freed.c      | 14 +++
 test/c/memory-safety/malloc_zero_leak_fail.c  | 10 ++
 .../malloc_zero_memcpy_in_fail.c              | 13 +++
 .../malloc_zero_memcpy_out_fail.c             | 13 +++
 .../c/memory-safety/malloc_zero_memset_fail.c | 14 +++
 test/c/memory-safety/malloc_zero_no_access.c  | 21 ++++
 test/c/memory-safety/malloc_zero_read_fail.c  | 12 +++
 .../malloc_zero_wide_deref_fail.c             | 12 +++
 test/c/memory-safety/realloc_grow_zero.c      | 13 +++
 .../c/memory-safety/realloc_zero_deref_fail.c | 14 +++
 test/c/memory-safety/realloc_zero_freed.c     | 16 ++++
 test/c/memory-safety/realloc_zero_leak_fail.c | 16 ++++
 22 files changed, 328 insertions(+), 45 deletions(-)
 create mode 100644 test/c/basic/malloc_zero.c
 create mode 100644 test/c/basic/malloc_zero_fail.c
 create mode 100644 test/c/memory-safety/alloca_zero_deref_fail.c
 create mode 100644 test/c/memory-safety/calloc_zero_deref_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero.c
 create mode 100644 test/c/memory-safety/malloc_zero_deref_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero_freed.c
 create mode 100644 test/c/memory-safety/malloc_zero_leak_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero_memcpy_in_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero_memcpy_out_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero_memset_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero_no_access.c
 create mode 100644 test/c/memory-safety/malloc_zero_read_fail.c
 create mode 100644 test/c/memory-safety/malloc_zero_wide_deref_fail.c
 create mode 100644 test/c/memory-safety/realloc_grow_zero.c
 create mode 100644 test/c/memory-safety/realloc_zero_deref_fail.c
 create mode 100644 test/c/memory-safety/realloc_zero_freed.c
 create mode 100644 test/c/memory-safety/realloc_zero_leak_fail.c

diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index 5cb4e212c..2f3071b72 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");
@@ -1680,18 +1692,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"
@@ -1729,17 +1741,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)} "
@@ -1779,18 +1791,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");
 
@@ -1819,17 +1830,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 +1852,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 +1877,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/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/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;
+}

From 85c0333bc8f548fad87c0b4be3ee430469afce0e Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 26 Aug 2026 09:57:52 -0700
Subject: [PATCH 2/3] Frame the allocation map across free(NULL)

The reuse and no-reuse memory-safety models specify $free by contract, and
every postcondition about $Alloc was guarded by p != 0. For free(NULL),
which C11 7.22.3.3 defines as a no-op, nothing constrained $Alloc after the
call, so the verifier could drop a live block's entry and report the next
free of that block as invalid. free(NULL) and the realloc(NULL, n) idiom
both hit this; so did every free of a malloc(0) result, because those
models used to return NULL for it. With the frame, a legal program that
frees a null pointer and then a live block verifies under all three models.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 share/smack/lib/smack.c                    |  6 ++++++
 test/c/memory-safety/free_null_then_free.c | 19 +++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 test/c/memory-safety/free_null_then_free.c

diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index 2f3071b72..55576a797 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -1766,6 +1766,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 == "
@@ -1813,6 +1816,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 == "
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;
+}

From 88d2bbf75cca497c701ffbe5d14bf1dc3f3998d4 Mon Sep 17 00:00:00 2001
From: Shaobo He <polarishehn@gmail.com>
Date: Wed, 26 Aug 2026 21:58:02 -0700
Subject: [PATCH 3/3] Give a global with no bytes a size of zero

An object whose type is sized but empty -- a zero-length array, an empty
struct -- was recorded with its type's alignment as its size, so an access
into it verified:

    int g[0];
    int main(void) { g[0] = 1; return 0; }

reports no errors under --check=memory-safety in every memory model. The
emitted Boogie says `const {:allocSize 0} g: ref;` and then `$galloc(g, 8)`.

globalDecl computes one number and puts it to two jobs: reserving address
space so that distinct globals get distinct addresses, and recording the
object's size for memory-safety checking. Those part company for an empty
object, which still needs an address of its own but has no byte that may be
accessed, so the fallback that kept the reserved space nonzero was also
inflating the size. Reserve the type's alignment as before and record the
size as it is. An external declaration, whose definition we cannot see, and
an unsized type keep their placeholders, so only a genuinely empty object
changes.

$galloc then needs the fact its range quantifier cannot give when that range
is empty, exactly as $$alloc did: $base(base_addr) == base_addr.

Over 407 test programs x 2 memory models, the emitted Boogie changes in
exactly two ways: the new $galloc fact, one line in each memory-safety
program, and $galloc(g, 8) becoming $galloc(g, 0) for the zero-length global
in the new regression. Nothing else moves.

Fixes #854.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 lib/smack/SmackRep.cpp                        | 32 ++++++++++++++-----
 share/smack/lib/smack.c                       |  3 ++
 test/c/basic/global_zero.c                    | 17 ++++++++++
 test/c/memory-safety/global_zero_deref_fail.c | 14 ++++++++
 test/c/memory-safety/global_zero_no_access.c  | 14 ++++++++
 5 files changed, 72 insertions(+), 8 deletions(-)
 create mode 100644 test/c/basic/global_zero.c
 create mode 100644 test/c/memory-safety/global_zero_deref_fail.c
 create mode 100644 test/c/memory-safety/global_zero_no_access.c

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 55576a797..e20f66d26 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -1682,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"
@@ -1729,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"
@@ -1784,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"
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/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];
+}