@@ -211,6 +211,7 @@ jobs:
             frontend/roslyn/samples/SelfDetachingHandlerSample.cs \
             frontend/roslyn/samples/UsingFieldAcquisitionSample.cs \
             frontend/roslyn/samples/TemplatePartLocalCaptureSample.cs \
+            frontend/roslyn/samples/EmptyDisposeSample.cs \
             -o "$RUNNER_TEMP/facts.json"
           cat "$RUNNER_TEMP/facts.json"
       - name: Check facts through the core
@@ -835,7 +836,20 @@ jobs:
           # ...while the same-named local in the OTHER method must still warn.
           echo "$out" | grep -qE "TemplatePartLocalCaptureSample\.cs:[0-9]+: warning: \[OWN001\].*'SameNameDifferentScopeSubscriber'" \
             || { echo "FAIL: expected OWN001 on the same-named-but-unrelated local in a different method"; exit 1; }
-          echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) + OWN014 (static-event region escape) + DI001 (captive dependency) + DI002 (scoped captured weakly) + DI003 (transient IDisposable captured by a singleton) + DI004 (transient IDisposable service-located from the root provider) + DI005 (scoped service cached from a created scope) + [OwnIgnore] suppression (silent-but-counted, SARIF suppressions) + #218 DP old->new subscription rotation (silent; controls flagged) at the C# location"
+          # issue #225 — a user-defined type whose Dispose() body is provably EMPTY holds no resource,
+          # so a LOCAL of it never disposed is not a leak (extends the named-BCL no-op exemption to any
+          # type). Here the flat (non-flow) name path: a `*Reader`-named empty-Dispose local (ScratchReader)
+          # is silent, while a non-empty `*Reader` local (LeakyReader) still leaks. (The semantic enumerator
+          # form is exercised in the --flow-locals step below.)
+          if echo "$out" | grep -q "'ScratchReader'"; then
+            echo "FAIL: a local of a user type with a provably-empty Dispose() body was wrongly flagged (#225)"; exit 1
+          fi
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'lr'.*'LeakyReader'" \
+            || { echo "FAIL: a non-empty-Dispose local (LeakyReader) must still leak (#225 stays scoped)"; exit 1; }
+          # Codex P2: an empty SYNC Dispose but a real DisposeAsync (a `*Reader` here) must still leak.
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'ar'.*'AsyncReader'" \
+            || { echo "FAIL: a type with a real DisposeAsync (empty sync Dispose) must still leak (#225)"; exit 1; }
+          echo "OK: real C# -> facts -> OWN001 (subscription + timer + field + Subscribe + pool + local) + OWN014 (static-event region escape) + DI001 (captive dependency) + DI002 (scoped captured weakly) + DI003 (transient IDisposable captured by a singleton) + DI004 (transient IDisposable service-located from the root provider) + DI005 (scoped service cached from a created scope) + [OwnIgnore] suppression (silent-but-counted, SARIF suppressions) + #218 DP old->new subscription rotation (silent; controls flagged) + #225 empty-Dispose local exemption (silent; controls flagged) at the C# location"
       - name: Flow-sensitive local IDisposables (--flow-locals, P-016 B0b/B2)
         run: |
           # Path-sensitive flow analysis of local IDisposables — bugs the flat D1
@@ -844,7 +858,8 @@ jobs:
             frontend/roslyn/samples/FlowLocalsSample.cs \
             frontend/roslyn/samples/MemoryOwnerEscapeSample.cs \
             frontend/roslyn/samples/FactoryLeakSample.cs \
-            frontend/roslyn/samples/OverloadSigSample.cs --flow-locals -o "$RUNNER_TEMP/flow.json"
+            frontend/roslyn/samples/OverloadSigSample.cs \
+            frontend/roslyn/samples/EmptyDisposeSample.cs --flow-locals -o "$RUNNER_TEMP/flow.json"
           out=$(python -m ownlang ownir "$RUNNER_TEMP/flow.json" || true)
           echo "$out"
           echo "$out" | grep -q "OWN002" || { echo "FAIL: expected OWN002 (use-after-dispose)"; exit 1; }
@@ -1066,7 +1081,26 @@ jobs:
           for ok in opened probe; do
             if echo "$out" | grep -q "'$ok'"; then echo "FAIL: stage-2 silent case '$ok' was reported"; exit 1; fi
           done
-          echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach/for, try/finally sequential, never-vs-every-path wording, dispose-optional exempt, beyond flat)"
+          # issue #225 (semantic flow path — the real ClosedXML Slice.Enumerator shape): a LOCAL of a
+          # user type whose Dispose() body is provably EMPTY holds no resource, so never disposing it
+          # cannot leak. The three controls STILL leak: a real IDisposable ('r'), a non-empty *Reader
+          # ('lr'), and an empty override over a base that owns a real Dispose ('d').
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'r' is never disposed" \
+            || { echo "FAIL: #225 flow: a real IDisposable local must still leak"; exit 1; }
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'lr' is never disposed" \
+            || { echo "FAIL: #225 flow: a non-empty *Reader local must still leak"; exit 1; }
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'d' is never disposed" \
+            || { echo "FAIL: #225 flow: an empty override over a real base Dispose must still leak"; exit 1; }
+          # Codex P2: an empty SYNC Dispose() but a real DisposeAsync() (IDisposable + IAsyncDisposable)
+          # must NOT be exempted — the real cleanup is async and the flow detector treats it as a release.
+          echo "$out" | grep -qE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN001\].*'ar' is never disposed" \
+            || { echo "FAIL: #225 flow: a type with a real DisposeAsync (empty sync Dispose) must still leak"; exit 1; }
+          # exactly 4 EmptyDisposeSample findings -> the two provably-empty-Dispose locals (the enumerator
+          # and ScratchReader) are SILENT; any leak of them would push the count past 4.
+          n225=$(echo "$out" | grep -cE "EmptyDisposeSample\.cs:[0-9]+:.*\[OWN00")
+          [ "$n225" = "4" ] \
+            || { echo "FAIL: #225 flow: expected exactly 4 EmptyDisposeSample findings (controls only), got $n225"; exit 1; }
+          echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach/for, try/finally sequential, never-vs-every-path wording, dispose-optional exempt, #225 empty-Dispose local exempt, beyond flat)"
       - name: Gallery C#-native bad/ok pairs (examples/gallery/cs/)
         run: |
           # C#-native mirror of examples/gallery/*.own, run through the real extractor ->
 
@@ -644,6 +644,24 @@ type names, a `Dispose()` method whose body is provably empty (no statements)
 is safe to skip regardless of whose type it is — first-party or third-party,
 named allowlist or not.**
 
+**Shipped (issue #225).** `HasEmptyDisposeBody` (extractor) recognises a type
+whose parameterless `Dispose()` is declared in source with a **block body of zero
+statements** *and* whose base chain carries no `Dispose` to cascade to (base is
+`object` / not `IDisposable`), so nothing real is skipped. A **LOCAL** of such a
+type never disposed is then dropped from both the flat (`IsDisposableType`) and the
+`--flow-locals` (`ImplementsIDisposable`) local-disposable paths. Deliberately
+**scoped to locals**: a FIELD keeps its own disposal contract (so the
+`OwnIgnoreSample` `Handle` field stand-in and other field fixtures are untouched).
+Precision guards, each pinned by `EmptyDisposeSample.cs`: a **non-empty** body
+(`RealResource`, `LeakyReader`) still leaks; an **empty override over a base whose
+`Dispose` does real work** (`EmptyOverrideOverRealBase`) still leaks; an
+**expression-bodied / metadata-only** `Dispose` we cannot read as empty is not
+exempted (never a guessed drop). The empty enumerator (`EmptyDisposeEnumerator`,
+the ClosedXML shape) and an empty `*Reader` (`ScratchReader`) stay silent. Two
+existing fixtures that had used an empty `Dispose()` as a modelling shortcut
+(`UnitOfWork`, `PixelOwner`) were made faithful (a real Dispose body) so they
+remain genuine leak fixtures.
+
 ---
 
 ## The through-line
 
@@ -1306,6 +1306,38 @@ static bool IsNoOpDisposeWrapper(BaseObjectCreationExpressionSyntax oce, Semanti
     return arg0 is not null && IsInMemoryDisposableBacking(model.GetTypeInfo(arg0).Type);
 }
 
+// Issue #225 — a user-defined type whose parameterless `Dispose()` body is provably EMPTY holds no
+// resource behind the interface: it implements IDisposable only to satisfy a contract (e.g.
+// `IEnumerator<T>`), so never calling Dispose() cannot leak. Recognised from SOURCE: the type
+// declares `void Dispose()` with a BLOCK body of ZERO statements, and no base in its chain carries a
+// Dispose to cascade to (the base is `object` / not IDisposable), so nothing real is skipped. A body
+// we cannot read (third-party metadata-only, or expression-bodied doing work) is NOT provably empty
+// and stays flagged — never a guessed drop. This generalises the named-BCL IsNoOpDisposeWrapper /
+// IsDisposeOptional idea to any type. Deliberately scoped to LOCAL disposables (the #201-sweep
+// evidence — ClosedXML's `Slice.Enumerator` locals): a FIELD keeps its own disposal contract, so an
+// empty-Dispose field (the OwnIgnoreSample `Handle` stand-in) is unaffected.
+static bool HasEmptyDisposeBody(ITypeSymbol? t)
+{
+    if (t is not INamedTypeSymbol nt)
+        return false;
+    // The base must not own a Dispose we'd be silently skipping — only `object` / a non-IDisposable base.
+    for (var b = nt.BaseType; b is not null && b.SpecialType != SpecialType.System_Object; b = b.BaseType)
+        if (ImplementsIDisposable(b))
+            return false;
+    // A non-empty DisposeAsync() can do the REAL cleanup even when the sync Dispose() is an empty
+    // compatibility no-op (a type implementing both IDisposable AND IAsyncDisposable). The flow
+    // detector already treats DisposeAsync() as a release, so an undisposed local of such a type is a
+    // real leak — conservatively refuse to exempt any type that declares its own DisposeAsync (Codex).
+    if (nt.GetMembers("DisposeAsync").OfType<IMethodSymbol>().Any(m => m.Parameters.Length == 0))
+        return false;
+    var dispose = nt.GetMembers("Dispose").OfType<IMethodSymbol>().FirstOrDefault(
+        m => m.Parameters.Length == 0 && m.ReturnsVoid && m.TypeParameters.Length == 0);
+    if (dispose is null || dispose.DeclaringSyntaxReferences.Length == 0)
+        return false;   // no readable source Dispose (metadata-only) -> cannot prove empty
+    return dispose.DeclaringSyntaxReferences.All(
+        sref => sref.GetSyntax() is MethodDeclarationSyntax { Body.Statements.Count: 0 });
+}
+
 // A type that is System.Windows.Forms.Form or derives from it (semantic, walks the
 // base chain). A modeless `Form.Show()` transfers ownership to the framework, which
 // disposes the form on close — EmitFlowExpr models that show as a release.
@@ -4715,6 +4747,11 @@ when model.GetSymbolInfo(asg.Left).Symbol is IFieldSymbol
                     };
                     if (ctype is null || !IsDisposableType(ctype))
                         continue;
+                    // #225: a user type whose Dispose() body is provably empty holds no resource —
+                    // never disposing a local of it cannot leak (mirrors the flow path's guard).
+                    if (v.Initializer?.Value is { } newExpr
+                        && HasEmptyDisposeBody(model.GetTypeInfo(newExpr).Type))
+                        continue;
                     subs.Add(new
                     {
                         @event = name,
@@ -4758,7 +4795,10 @@ when model.GetSymbolInfo(asg.Left).Symbol is IFieldSymbol
                         if (v.Initializer is { Value: ObjectCreationExpressionSyntax
                                                    or ImplicitObjectCreationExpressionSyntax } init
                             && model.GetTypeInfo(init.Value).Type is { } dt
-                            && ImplementsIDisposable(dt) && !IsDisposeOptional(dt))
+                            && ImplementsIDisposable(dt) && !IsDisposeOptional(dt)
+                            // #225: a user type with a provably-empty Dispose() body holds no
+                            // resource -> never disposing a local of it cannot leak.
+                            && !HasEmptyDisposeBody(dt))
                         {
                             candidates.Add(v.Identifier.Text);
                             newedDisposables.Add(v.Identifier.Text);
 
@@ -0,0 +1,123 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+
+namespace Own.Samples;
+
+// Issue #225 — a user-defined type whose Dispose() body is provably EMPTY holds no resource behind
+// the interface (it implements IDisposable only to satisfy a contract, e.g. IEnumerator<T>), so a
+// LOCAL of it that is never disposed cannot leak. Generalises the named-BCL no-op exemption
+// (field-notes entry 9 / IsNoOpDisposeWrapper) to any type. Mirrors ClosedXML's Slice.Enumerator.
+// Negative controls prove it does not over-widen. A FIELD keeps its own disposal contract (out of
+// scope here), so the OwnIgnoreSample `Handle` field stand-in is unaffected.
+
+// EMPTY Dispose — implements IDisposable only because IEnumerator<T> requires it (the ClosedXML
+// shape). Its Dispose does literally nothing.
+public sealed class EmptyDisposeEnumerator : IEnumerator<int>
+{
+    private int _i;
+    public int Current => _i;
+    object IEnumerator.Current => Current;
+    public bool MoveNext() => ++_i <= 3;
+    public void Reset() => _i = 0;
+    public void Dispose() { }   // literally empty -> no resource
+}
+
+// EMPTY Dispose on a name that ALSO matches the flat (non-flow) name heuristic (`*Reader`), so the
+// non-flow local-disposable path exercises the same exemption.
+public sealed class ScratchReader : IDisposable
+{
+    public int Read() => -1;
+    public void Dispose() { }   // empty -> no resource
+}
+
+// NON-empty Dispose — a real owned resource released in Dispose. A local never disposed LEAKS.
+public sealed class RealResource : IDisposable
+{
+    private bool _closed;
+    public void Touch() { }
+    public void Dispose() { _closed = true; }   // has a statement -> not provably empty
+}
+
+// NON-empty Dispose, name matches the flat heuristic — the flat-path control.
+public sealed class LeakyReader : IDisposable
+{
+    public int Read() => 0;
+    public void Dispose() { GC.SuppressFinalize(this); }   // real work -> stays flagged
+}
+
+// Empty-bodied OVERRIDE, but the BASE owns a real Dispose — skipping this type's empty Dispose would
+// skip the base's cascade, so a local of it must STAY flagged.
+public class BaseWithRealDispose : IDisposable
+{
+    public void Ping() { }
+    public virtual void Dispose() { GC.SuppressFinalize(this); }
+}
+public sealed class EmptyOverrideOverRealBase : BaseWithRealDispose
+{
+    public override void Dispose() { }   // empty, but base.Dispose does real work
+}
+
+// NON-empty cleanup via DisposeAsync, with the sync Dispose() an empty COMPATIBILITY no-op (a type
+// implementing both IDisposable and IAsyncDisposable). The empty sync body must NOT exempt it — the
+// real cleanup lives in DisposeAsync, which the flow detector treats as a release, so an undisposed
+// local still leaks (Codex P2). Name ends `Reader` so both detector paths see it.
+public sealed class AsyncReader : IDisposable, IAsyncDisposable
+{
+    private readonly System.Threading.CancellationTokenSource _cts = new();
+    public int Read() => 0;
+    public void Dispose() { }                                        // empty sync compat no-op
+    public System.Threading.Tasks.ValueTask DisposeAsync()           // REAL cleanup
+    {
+        _cts.Dispose();
+        return default;
+    }
+}
+
+public sealed class EmptyDisposeConsumers
+{
+    // SILENT: an empty-Dispose enumerator local, iterated and never disposed (the ClosedXML shape).
+    public int CountEmpty()
+    {
+        var e = new EmptyDisposeEnumerator();
+        var n = 0;
+        while (e.MoveNext()) n++;   // never disposed -> Dispose is empty -> SILENT
+        return n;
+    }
+
+    // SILENT: an empty-Dispose `*Reader` local (flat-path name match) never disposed.
+    public int UseScratch()
+    {
+        var s = new ScratchReader();
+        return s.Read();           // never disposed -> Dispose is empty -> SILENT
+    }
+
+    // FLAGGED (control): a real IDisposable local never disposed -> OWN001.
+    public void LeakReal()
+    {
+        var r = new RealResource();
+        r.Touch();                 // used, never disposed -> LEAK
+    }
+
+    // FLAGGED (control): a non-empty `*Reader` local never disposed -> OWN001 (flat path).
+    public int LeakReader()
+    {
+        var lr = new LeakyReader();
+        return lr.Read();          // never disposed -> LEAK
+    }
+
+    // FLAGGED (control): empty override, but the base Dispose does real work -> OWN001.
+    public void LeakDerived()
+    {
+        var d = new EmptyOverrideOverRealBase();
+        d.Ping();                  // base.Dispose() is real -> LEAK
+    }
+
+    // FLAGGED (control, Codex P2): empty SYNC Dispose but a real DisposeAsync -> never disposing
+    // (sync or async) leaks; the empty sync body must not exempt it.
+    public int LeakAsync()
+    {
+        var ar = new AsyncReader();
+        return ar.Read();          // never disposed (sync or async) -> LEAK
+    }
+}
@@ -16,7 +16,7 @@ internal sealed class PixelOwner : IMemoryOwner<byte>
 
     public Memory<byte> Memory => this.data;
 
-    public void Dispose() { }
+    public void Dispose() { Array.Clear(this.data, 0, this.data.Length); }   // real work (#225): not a no-op
 }
 
 internal static class MemoryOwnerEscape
 
@@ -99,11 +99,15 @@ public interface IUnitOfWork : IDisposable
     // optional) — which is what makes a leaked local matter.
     public sealed class UnitOfWork : IUnitOfWork
     {
+        // Owns a real IDisposable (a DbContext-like resource) released in Dispose, so a leaked
+        // local genuinely leaks — its Dispose() is NOT a no-op (keeps this fixture faithful under
+        // the #225 empty-Dispose exemption, which only skips a provably-empty body).
+        private readonly System.Threading.CancellationTokenSource _cts = new();
         public UnitOfWork(bool isCatalogs) { }
         public IQueryable<ProductCatalog> ProductCatalogs => Enumerable.Empty<ProductCatalog>().AsQueryable();
         public IQueryable<TempProduct> TempProducts => Enumerable.Empty<TempProduct>().AsQueryable();
         public IGenericRepository<T> GenericRepository<T>() => new GenericRepository<T>();
-        public void Dispose() { }
+        public void Dispose() { _cts.Dispose(); }
     }
 
     public interface IGenericRepository<T>
Original file line number	Diff line number	Diff line change
`@@ -16,7 +16,7 @@ internal sealed class PixelOwner : IMemoryOwner<byte>`
`16`	`16`
`17`	`17`	`public Memory<byte> Memory => this.data;`
`18`	`18`
`19`		`- public void Dispose() { }`
	`19`	`+ public void Dispose() { Array.Clear(this.data, 0, this.data.Length); } // real work (#225): not a no-op`
`20`	`20`	`}`
`21`	`21`
`22`	`22`	`internal static class MemoryOwnerEscape`