diff --git a/include/analysis/ownership/OwnershipEngine.hpp b/include/analysis/ownership/OwnershipEngine.hpp
index 750384b5..d8a79d14 100644
--- a/include/analysis/ownership/OwnershipEngine.hpp
+++ b/include/analysis/ownership/OwnershipEngine.hpp
@@ -48,6 +48,20 @@ namespace ctrace::stack::analysis::ownership
         const OwnershipFacts& facts, const OwnershipResult& result, std::uint32_t block,
         const std::function<void(std::uint32_t, const AbstractState&, const AbstractState&)>& cb);
 
+    /// A Use event that may read a released resource.
+    struct ReleasedUse
+    {
+        const Event* use = nullptr; // points into the facts
+        ResourceId resource = 0;
+        std::uint32_t reservedPadding = 0;
+    };
+
+    /// Every (Use, resource) where the resource the Use's `src` may hold may be Released and is
+    /// not uncertain, or is Released on every path where it exists (uncertain or not), read off
+    /// the stabilised states (edges included). Empty when incomplete.
+    std::vector<ReleasedUse> releasedUses(const OwnershipFacts& facts,
+                                          const OwnershipResult& result);
+
     /// Union of t[s] over the states s in `in`.
     StateSet applyTransformer(const ParamTransformer& t, StateSet in);
 
diff --git a/include/analysis/ownership/OwnershipFacts.hpp b/include/analysis/ownership/OwnershipFacts.hpp
index c77abcf7..a2415ba1 100644
--- a/include/analysis/ownership/OwnershipFacts.hpp
+++ b/include/analysis/ownership/OwnershipFacts.hpp
@@ -120,6 +120,9 @@ namespace ctrace::stack::analysis::ownership
     {
         ExitTransformer normal;
         ExitTransformer exceptional;
+        // Sorted indices of the pointer arguments a Use of the function may reach: the function
+        // may need what they point to alive, even when it also releases them.
+        std::vector<unsigned> usedArgs;
         bool incomplete = false;
         std::uint8_t reservedPadding[7] = {};
     };
@@ -152,7 +155,10 @@ namespace ctrace::stack::analysis::ownership
                            // lists locations whose resources are uncertain *at this exit*
             // Edge event: the conditional contract of acquisition `site` is decided here;
             // unknownValue = true means "did not acquire" (resource NotOwned, holders null).
-            ContractResolved
+            ContractResolved,
+            // The resource `src` holds must be live here (state unchanged); `dst` is the
+            // location to name it by (the slot the pointer was read from).
+            Use
         };
 
         std::vector<LocationId> args;
diff --git a/run_test.py b/run_test.py
index fa541804..a14c5f68 100755
--- a/run_test.py
+++ b/run_test.py
@@ -2448,6 +2448,39 @@ def check_ownership_cross_tu() -> bool:
             if outputs[0] != outputs[1]:
                 print(f"  ❌ {name}: cached run differs from the first run")
                 ok = False
+        # Callees that release their argument: the call after a release is a use when the callee
+        # also accesses it (after the release, or on another path), not when it only releases
+        # it. Same result with Z3, and when the summaries are read back from the cache: the
+        # second run may still recompute intermediate rounds of the fixpoint, the third reads
+        # every summary from it.
+        files = [
+            str(fixtures / "cross-tu-use-then-release-def.c"),
+            str(fixtures / "cross-tu-use-then-release-use.c"),
+        ]
+        expected_uses = [
+            f"at line {line}, column {column}\n\t[!!!Error] potential use-after-release: 'HeapAlloc' handle 'p'"
+            for line, column in ((18, 32), (26, 30))
+        ]
+        smt_args = [
+            "--smt=on",
+            "--smt-backend=z3",
+            "--smt-mode=single",
+            f"--smt-rules={','.join(_all_smt_rules())}",
+            f"--smt-timeout-ms={SMT_FIXTURE_TIMEOUT_MS}",
+        ]
+        for mode, extra in (("default", []), ("smt-z3", smt_args)):
+            args = files + common[:-1] + [f"--resource-summary-cache-dir={tmpdir / f'use-then-release-{mode}'}"]
+            for run in ("first", "second", "third"):
+                result = run_analyzer_uncached(args + extra)
+                output = result.stdout or ""
+                if (
+                    result.returncode != 0
+                    or output.count("use-after-release") != len(expected_uses)
+                    or not all(use in output for use in expected_uses)
+                ):
+                    print(f"  ❌ use-then-release ({mode}, {run}): expected the use-after-release at lines 18 and 26 only")
+                    print(output + (result.stderr or ""))
+                    ok = False
     if ok:
         print("  ✅ resource ownership cross-TU transformers OK\n")
     return ok
@@ -2511,7 +2544,7 @@ def checked_output(inputs):
         if checked_output(inputs) != first:
             return fail_check("obsolete summaries changed the wrapper diagnostics")
         # Intermediate fixpoint keys need not be reused; active keys must be rewritten.
-        if not any(json.loads(path.read_text())["schema"] == "resource-summary-cache-v5" for path in cache_files):
+        if not any(json.loads(path.read_text())["schema"] == "resource-summary-cache-v6" for path in cache_files):
             return fail_check("obsolete ownership summaries were not rebuilt")
     print("  ✅ ownership wrapper metadata preserved locally, across TUs and in the cache\n")
     return True
diff --git a/src/analysis/ResourceLifetimeAnalysis.cpp b/src/analysis/ResourceLifetimeAnalysis.cpp
index 089db923..34ec3040 100644
--- a/src/analysis/ResourceLifetimeAnalysis.cpp
+++ b/src/analysis/ResourceLifetimeAnalysis.cpp
@@ -13,8 +13,10 @@
 #include <iostream>
 #include <limits>
 #include <map>
+#include <set>
 #include <sstream>
 #include <string>
+#include <tuple>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
@@ -22,7 +24,6 @@
 #include <llvm/ADT/SmallPtrSet.h>
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/ADT/StringMap.h>
-#include <llvm/Analysis/CFG.h>
 #include <llvm/Analysis/CaptureTracking.h>
 #include <llvm/Analysis/ValueTracking.h>
 #include <llvm/IR/Argument.h>
@@ -92,7 +93,6 @@ namespace ctrace::stack::analysis
             std::string resourceKind;
             std::string funcName;
             const llvm::Instruction* firstAcquireInst = nullptr;
-            std::vector<const llvm::Instruction*> releaseInsts;
             int acquires = 0;
             int releases = 0;
             OwnershipState ownership = OwnershipState::Unknown;
@@ -1032,28 +1032,8 @@ namespace ctrace::stack::analysis
                    name == "read";
         }
 
-        static bool callArgumentIsDirectReleaseArg(const llvm::CallBase& CB,
-                                                   const llvm::Function* callee,
-                                                   const ResourceModel& model, unsigned argIndex)
-        {
-            if (!callee)
-                return false;
-
-            for (const ResourceRule& rule : model.rules)
-            {
-                if (rule.action != RuleAction::ReleaseArg)
-                    continue;
-                if (rule.argIndex != argIndex)
-                    continue;
-                if (ruleMatchesFunction(rule, *callee))
-                    return true;
-            }
-
-            return false;
-        }
-
-        static bool callArgumentLikelyDereferenced(const llvm::CallBase& CB,
-                                                   const llvm::Function* callee, unsigned argIndex)
+        bool callArgumentLikelyDereferenced(const llvm::CallBase& CB, const llvm::Function* callee,
+                                            unsigned argIndex)
         {
             if (argIndex >= CB.arg_size())
                 return false;
@@ -1086,135 +1066,6 @@ namespace ctrace::stack::analysis
             return false;
         }
 
-        static bool instructionMayReach(const llvm::Instruction& from, const llvm::Instruction& to)
-        {
-            if (from.getFunction() != to.getFunction())
-                return false;
-            if (&from == &to)
-                return true;
-            if (from.getParent() == to.getParent())
-                return from.comesBefore(&to);
-            return llvm::isPotentiallyReachable(&from, &to);
-        }
-
-        static bool
-        valueFeedsOnlyDirectReleaseArgs(const llvm::Value* value, const ResourceModel& model,
-                                        llvm::SmallPtrSet<const llvm::Value*, 32>& visited,
-                                        bool& sawReleaseUse, unsigned depth = 0)
-        {
-            if (!value || depth > 10)
-                return false;
-
-            value = value->stripPointerCasts();
-            if (!visited.insert(value).second)
-                return true;
-
-            bool sawMeaningfulUse = false;
-            for (const llvm::Use& U : value->uses())
-            {
-                const llvm::User* user = U.getUser();
-                if (const auto* II = llvm::dyn_cast<llvm::IntrinsicInst>(user))
-                {
-                    if (llvm::isa<llvm::DbgInfoIntrinsic>(II) ||
-                        llvm::isa<llvm::LifetimeIntrinsic>(II))
-                    {
-                        continue;
-                    }
-                }
-
-                if (const auto* CB = llvm::dyn_cast<llvm::CallBase>(user))
-                {
-                    const llvm::Function* callee = directCallee(*CB);
-                    if (!callee)
-                        return false;
-
-                    bool callUseIsReleaseOnly = false;
-                    for (unsigned argIdx = 0; argIdx < CB->arg_size(); ++argIdx)
-                    {
-                        if (CB->getArgOperand(argIdx)->stripPointerCasts() != value)
-                            continue;
-
-                        sawMeaningfulUse = true;
-                        if (!callArgumentIsDirectReleaseArg(*CB, callee, model, argIdx))
-                            return false;
-
-                        callUseIsReleaseOnly = true;
-                        sawReleaseUse = true;
-                    }
-                    if (!callUseIsReleaseOnly)
-                        return false;
-                    continue;
-                }
-
-                if (const auto* CI = llvm::dyn_cast<llvm::CastInst>(user))
-                {
-                    sawMeaningfulUse = true;
-                    if (!valueFeedsOnlyDirectReleaseArgs(CI, model, visited, sawReleaseUse,
-                                                         depth + 1))
-                    {
-                        return false;
-                    }
-                    continue;
-                }
-                if (const auto* BC = llvm::dyn_cast<llvm::BitCastOperator>(user))
-                {
-                    sawMeaningfulUse = true;
-                    if (!valueFeedsOnlyDirectReleaseArgs(BC, model, visited, sawReleaseUse,
-                                                         depth + 1))
-                    {
-                        return false;
-                    }
-                    continue;
-                }
-                if (const auto* GEP = llvm::dyn_cast<llvm::GEPOperator>(user))
-                {
-                    sawMeaningfulUse = true;
-                    if (!valueFeedsOnlyDirectReleaseArgs(GEP, model, visited, sawReleaseUse,
-                                                         depth + 1))
-                    {
-                        return false;
-                    }
-                    continue;
-                }
-                if (const auto* PN = llvm::dyn_cast<llvm::PHINode>(user))
-                {
-                    sawMeaningfulUse = true;
-                    if (!valueFeedsOnlyDirectReleaseArgs(PN, model, visited, sawReleaseUse,
-                                                         depth + 1))
-                    {
-                        return false;
-                    }
-                    continue;
-                }
-                if (const auto* Sel = llvm::dyn_cast<llvm::SelectInst>(user))
-                {
-                    sawMeaningfulUse = true;
-                    if (!valueFeedsOnlyDirectReleaseArgs(Sel, model, visited, sawReleaseUse,
-                                                         depth + 1))
-                    {
-                        return false;
-                    }
-                    continue;
-                }
-
-                // Any store/comparison/arithmetic or unknown use means this load
-                // participates in logic other than a pure release call path.
-                return false;
-            }
-
-            return sawMeaningfulUse && sawReleaseUse;
-        }
-
-        static bool loadFeedsOnlyDirectReleaseArgs(const llvm::LoadInst& load,
-                                                   const ResourceModel& model)
-        {
-            llvm::SmallPtrSet<const llvm::Value*, 32> visited;
-            bool sawReleaseUse = false;
-            if (!valueFeedsOnlyDirectReleaseArgs(&load, model, visited, sawReleaseUse))
-                return false;
-            return sawReleaseUse;
-        }
-
         static const llvm::AllocaInst*
         findOwnerLocalPointerSlotForReleasedHandleArg(const llvm::Value* handleArg,
                                                       const llvm::DataLayout& DL)
@@ -2406,11 +2257,11 @@ namespace ctrace::stack::analysis
     namespace
     {
         /// Runs the ownership engine on one function and turns its stabilised states into
-        /// MissingRelease / ReferenceLost / AnalysisIncomplete issues (spec §8).
-        void analyzeMissingReleaseWithEngine(const llvm::Function& F, const ResourceModel& model,
-                                             const ownership::SummaryLookup& summaries,
-                                             const llvm::DataLayout& DL,
-                                             std::vector<ResourceLifetimeIssue>& issues)
+        /// UseAfterRelease / MissingRelease / ReferenceLost / AnalysisIncomplete issues (spec §8).
+        void analyzeWithOwnershipEngine(const llvm::Function& F, const ResourceModel& model,
+                                        const ownership::SummaryLookup& summaries,
+                                        const llvm::DataLayout& DL,
+                                        std::vector<ResourceLifetimeIssue>& issues)
         {
             using namespace ownership;
 
@@ -2470,6 +2321,23 @@ namespace ctrace::stack::analysis
                 return;
             }
 
+            // A use of a resource that may be released: one issue per site and source line.
+            std::set<std::tuple<std::uint32_t, unsigned, const llvm::Instruction*>> usedAt;
+            for (const ReleasedUse& u : releasedUses(collected.facts, result))
+            {
+                const llvm::Instruction* at = collected.eventInstructions[u.use->instructionIndex];
+                const llvm::DebugLoc loc = at->getDebugLoc();
+                if (!usedAt.insert({u.resource / 2u, loc ? loc.getLine() : 0u, loc ? nullptr : at})
+                         .second)
+                    continue;
+                ResourceLifetimeIssue issue =
+                    issueFor(u.resource, ResourceLifetimeIssueKind::UseAfterRelease);
+                issue.inst = at;
+                if (collected.locationIsSlot[u.use->dst])
+                    issue.handleName = collected.locationNames[u.use->dst];
+                issues.push_back(std::move(issue));
+            }
+
             const std::size_t resourceCount = entry.resources.size();
             // One issue per acquisition site (spec §8): both instances of a site share it.
             std::vector<bool> reportedSite(collected.facts.siteCount, false);
@@ -2629,7 +2497,6 @@ namespace ctrace::stack::analysis
             std::unordered_map<std::string, LocalHandleState> localStates;
             std::unordered_map<const llvm::AllocaInst*, bool> unknownAcquireEscapeCache;
             std::unordered_set<std::string> interprocUncertaintyReported;
-            std::unordered_set<std::string> useAfterReleaseReported;
             std::unordered_set<std::string> releasedEscapeReported;
             auto trackAcquire = [&](const StorageKey& storage, const std::string& resourceKind,
                                     const llvm::Instruction* anchorInst)
@@ -2663,76 +2530,6 @@ namespace ctrace::stack::analysis
                 }
             };
 
-            auto sameLocalStorage = [&](const StorageKey& lhs, const StorageKey& rhs)
-            {
-                if (lhs.scope != StorageScope::Local || rhs.scope != StorageScope::Local)
-                    return false;
-                if (lhs.key == rhs.key)
-                    return true;
-                return lhs.localAlloca && rhs.localAlloca && lhs.localAlloca == rhs.localAlloca &&
-                       lhs.offset == rhs.offset;
-            };
-
-            auto reportUseAfterReleaseIfNeeded =
-                [&](const StorageKey& storage, const llvm::Instruction* anchorInst)
-            {
-                if (!storage.valid() || storage.scope != StorageScope::Local || !anchorInst)
-                    return;
-
-                for (const auto& entry : localStates)
-                {
-                    const LocalHandleState& state = entry.second;
-                    if (!sameLocalStorage(state.storage, storage))
-                        continue;
-                    if (state.acquires <= 0)
-                        continue;
-                    if (state.releases <= 0)
-                        continue;
-
-                    bool reachableRelease = false;
-                    for (const llvm::Instruction* releaseInst : state.releaseInsts)
-                    {
-                        if (!releaseInst)
-                            continue;
-                        if (instructionMayReach(*releaseInst, *anchorInst))
-                        {
-                            reachableRelease = true;
-                            break;
-                        }
-                    }
-                    if (!reachableRelease)
-                        continue;
-
-                    std::ostringstream dedupKey;
-                    if (state.storage.localAlloca)
-                    {
-                        dedupKey << static_cast<const void*>(state.storage.localAlloca) << ":"
-                                 << state.storage.offset;
-                    }
-                    else
-                    {
-                        dedupKey << state.storage.key;
-                    }
-                    dedupKey << "|";
-                    if (const llvm::DebugLoc loc = anchorInst->getDebugLoc())
-                        dedupKey << loc.getLine();
-                    else
-                        dedupKey << static_cast<const void*>(anchorInst);
-                    if (!useAfterReleaseReported.insert(dedupKey.str()).second)
-                        continue;
-
-                    ResourceLifetimeIssue issue;
-                    issue.funcName = F.getName().str();
-                    issue.resourceKind = state.resourceKind;
-                    issue.handleName = state.storage.displayName.empty()
-                                           ? std::string("<unknown>")
-                                           : state.storage.displayName;
-                    issue.inst = anchorInst;
-                    issue.kind = ResourceLifetimeIssueKind::UseAfterRelease;
-                    issues.push_back(std::move(issue));
-                }
-            };
-
             auto reportReleasedHandleEscapesIfNeeded = [&](const llvm::Value* releasedHandleValue,
                                                            const std::string& resourceKind,
                                                            const llvm::Instruction* anchorInst)
@@ -2812,8 +2609,6 @@ namespace ctrace::stack::analysis
                 }
 
                 state.releases += 1;
-                if (anchorInst)
-                    state.releaseInsts.push_back(anchorInst);
                 if (state.releases > state.acquires)
                 {
                     if (state.acquires == 0 && state.storage.localAlloca)
@@ -2914,34 +2709,6 @@ namespace ctrace::stack::analysis
             {
                 for (llvm::Instruction& I : BB)
                 {
-                    if (const auto* LI = llvm::dyn_cast<llvm::LoadInst>(&I))
-                    {
-                        if (loadFeedsOnlyDirectReleaseArgs(*LI, model))
-                            continue;
-                        StorageKey storage =
-                            resolveHandleStorage(LI->getPointerOperand(), F, DL, methodInfo);
-                        reportUseAfterReleaseIfNeeded(storage, &I);
-                    }
-                    else if (const auto* SI = llvm::dyn_cast<llvm::StoreInst>(&I))
-                    {
-                        StorageKey storage =
-                            resolveHandleStorage(SI->getPointerOperand(), F, DL, methodInfo);
-                        reportUseAfterReleaseIfNeeded(storage, &I);
-                    }
-                    else if (const auto* MI = llvm::dyn_cast<llvm::MemIntrinsic>(&I))
-                    {
-                        StorageKey dstStorage =
-                            resolveHandleStorage(MI->getDest(), F, DL, methodInfo);
-                        reportUseAfterReleaseIfNeeded(dstStorage, &I);
-
-                        if (const auto* MTI = llvm::dyn_cast<llvm::MemTransferInst>(MI))
-                        {
-                            StorageKey srcStorage =
-                                resolveHandleStorage(MTI->getSource(), F, DL, methodInfo);
-                            reportUseAfterReleaseIfNeeded(srcStorage, &I);
-                        }
-                    }
-
                     auto* CB = llvm::dyn_cast<llvm::CallBase>(&I);
                     if (!CB)
                         continue;
@@ -2950,20 +2717,6 @@ namespace ctrace::stack::analysis
                     if (!callee)
                         continue;
 
-                    for (unsigned argIdx = 0; argIdx < CB->arg_size(); ++argIdx)
-                    {
-                        const llvm::Value* arg = CB->getArgOperand(argIdx);
-                        if (!arg || !arg->getType()->isPointerTy())
-                            continue;
-                        if (callArgumentIsDirectReleaseArg(*CB, callee, model, argIdx))
-                            continue;
-                        if (!callArgumentLikelyDereferenced(*CB, callee, argIdx))
-                            continue;
-
-                        StorageKey storage = resolveHandleStorage(arg, F, DL, methodInfo);
-                        reportUseAfterReleaseIfNeeded(storage, &I);
-                    }
-
                     bool matchedDirectRule = false;
                     for (const ResourceRule& rule : model.rules)
                     {
@@ -3096,7 +2849,6 @@ namespace ctrace::stack::analysis
                         continue;
 
                     StorageKey storage = resolveHandleStorage(retVal, F, DL, methodInfo);
-                    reportUseAfterReleaseIfNeeded(storage, RI);
                     for (auto& entry : localStates)
                     {
                         LocalHandleState& state = entry.second;
@@ -3133,9 +2885,9 @@ namespace ctrace::stack::analysis
                 }
             }
 
-            // MissingRelease comes from the ownership engine (spec §8); the counters
-            // above keep serving the other rules.
-            analyzeMissingReleaseWithEngine(F, model, ownershipLookup, DL, issues);
+            // UseAfterRelease and MissingRelease come from the ownership engine (spec §8); the
+            // counters above keep serving the other rules.
+            analyzeWithOwnershipEngine(F, model, ownershipLookup, DL, issues);
 
             if (methodInfo.isDtor && !methodInfo.className.empty())
             {
diff --git a/src/analysis/ResourceLifetimeInternal.hpp b/src/analysis/ResourceLifetimeInternal.hpp
index 2515179c..bfc20549 100644
--- a/src/analysis/ResourceLifetimeInternal.hpp
+++ b/src/analysis/ResourceLifetimeInternal.hpp
@@ -63,4 +63,10 @@ namespace ctrace::stack::analysis::lifetime_detail
                                      std::uint64_t offset, bool viaPointerSlot,
                                      const llvm::Function& caller, const llvm::DataLayout& DL,
                                      const MethodClassInfo& callerMethodInfo);
+    /// Whether `callee` likely reads or writes through pointer argument `argIndex`: the
+    /// parameter's attributes say so, the callee is a known libc accessor, or it is an
+    /// external declaration (conservative). False for a defined callee without such
+    /// attributes and for an indirect call (callee null).
+    bool callArgumentLikelyDereferenced(const llvm::CallBase& CB, const llvm::Function* callee,
+                                        unsigned argIndex);
 } // namespace ctrace::stack::analysis::lifetime_detail
diff --git a/src/analysis/ownership/OwnershipEngine.cpp b/src/analysis/ownership/OwnershipEngine.cpp
index 31577958..fd6dbf31 100644
--- a/src/analysis/ownership/OwnershipEngine.cpp
+++ b/src/analysis/ownership/OwnershipEngine.cpp
@@ -33,6 +33,26 @@ namespace ctrace::stack::analysis::ownership
             }
         }
 
+        /// Hands what `held` names over to someone else (a global, the caller): a live resource
+        /// becomes Escaped; a released one stays Released, since a new owner does not make freed
+        /// memory live again. Strong only when the contents name exactly one resource.
+        void handOver(AbstractState& s, const Contents& held)
+        {
+            for (const ResourceId r : held.resources)
+            {
+                StateSet next = s.resources[r];
+                if (next.has(OwnState::Owned) || next.has(OwnState::Escaped))
+                {
+                    next.bits &= static_cast<std::uint8_t>(~StateSet::of(OwnState::Owned).bits);
+                    next |= StateSet::of(OwnState::Escaped);
+                }
+                if (held.isExactly(r))
+                    s.resources[r] = next;
+                else
+                    s.resources[r] |= next;
+            }
+        }
+
         void retargetLocations(AbstractState& s, ResourceId from, ResourceId to)
         {
             for (Contents& c : s.locations)
@@ -154,7 +174,7 @@ namespace ctrace::stack::analysis::ownership
                 dst.merge(src);
             const LocationKind kind = facts.locations[e.dst].kind;
             if (kind == LocationKind::NonLocal || kind == LocationKind::ArgPointee)
-                markHeld(s, src, StateSet::of(OwnState::Escaped), /*guaranteed=*/true);
+                handOver(s, src);
             break;
         }
 
@@ -176,7 +196,7 @@ namespace ctrace::stack::analysis::ownership
         case Event::Kind::Return:
         {
             const Contents held = s.locations[e.src];
-            markHeld(s, held, StateSet::of(OwnState::Escaped), /*guaranteed=*/true);
+            handOver(s, held);
             break;
         }
 
@@ -198,6 +218,11 @@ namespace ctrace::stack::analysis::ownership
             {
                 for (const ResourceId r : s.locations[loc].resources)
                 {
+                    // Unknown code may release or keep a live resource; it cannot make a
+                    // released one live again, nor one that was never acquired exist.
+                    if (!s.resources[r].has(OwnState::Owned) &&
+                        !s.resources[r].has(OwnState::Escaped))
+                        continue;
                     s.resources[r] |=
                         StateSet::of(OwnState::Released) | StateSet::of(OwnState::Escaped);
                     s.uncertain[r] = true;
@@ -263,10 +288,67 @@ namespace ctrace::stack::analysis::ownership
         }
 
         case Event::Kind::Exit:
+        case Event::Kind::Use:
             break;
         }
     }
 
+    namespace
+    {
+        /// Calls visit(useEvent, stateBefore) for each Use of every reached block and of its
+        /// outgoing edges, replayed from the stabilised in-states.
+        template <typename Visit>
+        void forEachUse(const OwnershipFacts& facts, const OwnershipResult& result, Visit visit)
+        {
+            const auto step = [&](const Event& e, AbstractState& s)
+            {
+                if (e.kind == Event::Kind::Use)
+                    visit(e, static_cast<const AbstractState&>(s));
+                applyEvent(facts, e, s);
+            };
+            for (std::uint32_t block = 0; block < facts.blocks.size(); ++block)
+            {
+                if (block >= result.in.size() || !result.in[block].reached)
+                    continue;
+                AbstractState state = result.in[block];
+                for (const Event& e : facts.blocks[block].events)
+                    step(e, state);
+                for (const Edge& edge : facts.edges)
+                {
+                    if (edge.from != block)
+                        continue;
+                    AbstractState along = state;
+                    for (const Event& e : edge.events)
+                        step(e, along);
+                }
+            }
+        }
+    } // namespace
+
+    std::vector<ReleasedUse> releasedUses(const OwnershipFacts& facts,
+                                          const OwnershipResult& result)
+    {
+        std::vector<ReleasedUse> found;
+        if (result.incomplete)
+            return found;
+        forEachUse(facts, result,
+                   [&](const Event& e, const AbstractState& s)
+                   {
+                       for (const ResourceId r : s.locations[e.src].resources)
+                       {
+                           // Released on every path where it exists: a certain release through
+                           // an exact handle came last, whatever was uncertain before it.
+                           StateSet existing = s.resources[r];
+                           existing.bits &=
+                               static_cast<std::uint8_t>(~StateSet::of(OwnState::NotOwned).bits);
+                           if (s.resources[r].has(OwnState::Released) &&
+                               (!s.uncertain[r] || existing.isOnly(OwnState::Released)))
+                               found.push_back({&e, r});
+                       }
+                   });
+        return found;
+    }
+
     OwnershipResult solve(const OwnershipFacts& facts, const AbstractState& entry,
                           unsigned iterationLimit)
     {
@@ -571,8 +653,23 @@ namespace ctrace::stack::analysis::ownership
             }
         }
 
-        // Fresh resources: read off the solve with every parameter Owned.
+        // Fresh resources and used arguments: read off the solve with every parameter Owned.
         const ResourceId paramResourceLowerBound = newInstanceOf(paramSiteBase);
+        forEachUse(facts, res,
+                   [&](const Event& e, const AbstractState& s)
+                   {
+                       for (const ResourceId r : s.locations[e.src].resources)
+                       {
+                           if (r < paramResourceLowerBound)
+                               continue; // one of the function's own resources
+                           const std::size_t p = r / 2u - paramSiteBase;
+                           if (p < facts.paramLocations.size())
+                               summary.usedArgs.push_back(facts.paramLocations[p].first);
+                       }
+                   });
+        std::sort(summary.usedArgs.begin(), summary.usedArgs.end());
+        summary.usedArgs.erase(std::unique(summary.usedArgs.begin(), summary.usedArgs.end()),
+                               summary.usedArgs.end());
         summary.normal.returns.certainty = freshResourceCertainty(
             facts, res, false, LocationKind::Return, ArgPath{}, paramResourceLowerBound);
         summary.normal.returns.kind = freshResourceKind(facts, res, false, LocationKind::Return,
@@ -610,8 +707,8 @@ namespace ctrace::stack::analysis::ownership
             return x.present == y.present && x.returns == y.returns && x.outArgs == y.outArgs &&
                    x.params == y.params && x.pointeeParams == y.pointeeParams;
         };
-        return a.incomplete == b.incomplete && sameExit(a.normal, b.normal) &&
-               sameExit(a.exceptional, b.exceptional);
+        return a.incomplete == b.incomplete && a.usedArgs == b.usedArgs &&
+               sameExit(a.normal, b.normal) && sameExit(a.exceptional, b.exceptional);
     }
 
     std::vector<FunctionOwnershipSummary> computeSummaryFixpoint(
diff --git a/src/analysis/ownership/ResourceFactCollector.cpp b/src/analysis/ownership/ResourceFactCollector.cpp
index 6e5ec8a5..bcdb2579 100644
--- a/src/analysis/ownership/ResourceFactCollector.cpp
+++ b/src/analysis/ownership/ResourceFactCollector.cpp
@@ -18,6 +18,7 @@
 #include <llvm/IR/Instructions.h>
 #include <llvm/IR/IntrinsicInst.h>
 
+#include <algorithm>
 #include <map>
 #include <optional>
 #include <string>
@@ -165,6 +166,7 @@ namespace ctrace::stack::analysis::ownership
                     case Event::Kind::Overwrite:
                     case Event::Kind::Return:
                     case Event::Kind::Exit:
+                    case Event::Kind::Use:
                         break;
                     default:
                         return;
@@ -385,8 +387,100 @@ namespace ctrace::stack::analysis::ownership
 
             // ---- instruction mapping ---------------------------------------------------
 
+            /// What `I` needs alive: memory accessed through a pointer, a pointer argument the
+            /// callee likely dereferences, a pointer handed back to the caller. A copy, a
+            /// comparison, a reassignment or an argument the call only releases moves or
+            /// inspects the pointer value: no Use.
+            void emitUses(const llvm::Instruction& I)
+            {
+                if (const auto* load = llvm::dyn_cast<llvm::LoadInst>(&I))
+                    use(I, load->getPointerOperand());
+                else if (const auto* store = llvm::dyn_cast<llvm::StoreInst>(&I))
+                    use(I, store->getPointerOperand());
+                else if (const auto* rmw = llvm::dyn_cast<llvm::AtomicRMWInst>(&I))
+                    use(I, rmw->getPointerOperand());
+                else if (const auto* cas = llvm::dyn_cast<llvm::AtomicCmpXchgInst>(&I))
+                    use(I, cas->getPointerOperand());
+                else if (const auto* mem = llvm::dyn_cast<llvm::MemIntrinsic>(&I))
+                {
+                    use(I, mem->getDest());
+                    if (const auto* transfer = llvm::dyn_cast<llvm::MemTransferInst>(mem))
+                        use(I, transfer->getSource());
+                }
+                else if (const auto* ret = llvm::dyn_cast<llvm::ReturnInst>(&I))
+                {
+                    // Named by the resource: the slot of a merged return is no handle.
+                    if (const llvm::Value* v = ret->getReturnValue();
+                        v && v->getType()->isPointerTy())
+                        use(I, v, /*atRead=*/false);
+                }
+                else if (const auto* call = llvm::dyn_cast<llvm::CallBase>(&I);
+                         call && !llvm::isa<llvm::IntrinsicInst>(call) && !call->isInlineAsm())
+                {
+                    const llvm::Function* callee = directCallee(*call);
+                    const std::vector<unsigned> released =
+                        callee ? releasedArgs(*call, *callee, /*knownOnly=*/true)
+                               : std::vector<unsigned>{};
+                    for (unsigned i = 0; i < call->arg_size(); ++i)
+                    {
+                        // A released argument is still used when the callee's summary shows a
+                        // Use of it (`*p = 1; free(p);`), not when the callee only releases it.
+                        const bool isReleased =
+                            std::find(released.begin(), released.end(), i) != released.end();
+                        if (isReleased ? summaryUses(callee, i) : argumentUsed(*call, callee, i))
+                            use(I, call->getArgOperand(i));
+                    }
+                }
+            }
+
+            /// Whether the call may need what argument `i` points to alive. Attributes and the
+            /// library list decide first (a declaration is a use). Otherwise an unknown callee
+            /// (called through a pointer, or defined without a summary) is a use, and a defined
+            /// one is when a Use in its body may reach that parameter.
+            bool argumentUsed(const llvm::CallBase& call, const llvm::Function* callee,
+                              unsigned i) const
+            {
+                if (lifetime_detail::callArgumentLikelyDereferenced(call, callee, i))
+                    return true;
+                if (!call.getArgOperand(i)->getType()->isPointerTy() ||
+                    call.paramHasAttr(i, llvm::Attribute::ReadNone))
+                    return false;
+                if (!callee)
+                    return true;
+                if (callee->doesNotAccessMemory())
+                    return false;
+                const FunctionOwnershipSummary* summary = summaries_.byFunction(*callee);
+                return !summary || summary->incomplete || summaryUses(callee, i);
+            }
+
+            /// Whether the summary of `callee` lists a Use of its parameter `i`.
+            bool summaryUses(const llvm::Function* callee, unsigned i) const
+            {
+                const FunctionOwnershipSummary* summary =
+                    callee ? summaries_.byFunction(*callee) : nullptr;
+                return summary &&
+                       std::binary_search(summary->usedArgs.begin(), summary->usedArgs.end(), i);
+            }
+
+            /// A Use of the pointer `ptr` is based on, unless that is a local slot, a global or a
+            /// constant: those hold no resource themselves. With `atRead`, a pointer just read
+            /// from a slot is reported where it was read, under the slot's name.
+            void use(const llvm::Instruction& I, const llvm::Value* ptr, bool atRead = true)
+            {
+                const llvm::Value* base = llvm::getUnderlyingObject(ptr);
+                if (llvm::isa<llvm::AllocaInst>(base) || llvm::isa<llvm::Constant>(base))
+                    return;
+                const auto* load = atRead ? llvm::dyn_cast<llvm::LoadInst>(base) : nullptr;
+                const auto from = load ? loadedFrom_.find(load) : loadedFrom_.end();
+                Event e = make(Event::Kind::Use, from != loadedFrom_.end() ? *load : I);
+                e.src = valueLocation(base);
+                e.dst = from != loadedFrom_.end() ? from->second : e.src;
+                emit(std::move(e));
+            }
+
             void visit(const llvm::Instruction& I)
             {
+                emitUses(I);
                 if (const auto* store = llvm::dyn_cast<llvm::StoreInst>(&I))
                 {
                     visitStore(*store);
@@ -398,6 +492,7 @@ namespace ctrace::stack::analysis::ownership
                         return;
                     if (const auto slot = slotOf(load->getPointerOperand()))
                     {
+                        loadedFrom_[load] = *slot;
                         Event e = make(Event::Kind::Copy, I);
                         e.dst = valueLocation(load);
                         e.src = *slot;
@@ -488,9 +583,11 @@ namespace ctrace::stack::analysis::ownership
                     e.unknownValue = !llvm::isa<llvm::ConstantPointerNull>(stripped);
                     return e;
                 }
+                // An address computed from a pointer (p + 1, &p->field) points into the same
+                // resource: copy from the pointer it is computed from.
                 Event e = make(Event::Kind::Copy, I);
                 e.dst = dst;
-                e.src = valueLocation(value);
+                e.src = valueLocation(llvm::getUnderlyingObject(stripped));
                 e.strong = strong;
                 return e;
             }
@@ -672,32 +769,50 @@ namespace ctrace::stack::analysis::ownership
                 emitOnEdge(invoke.getParent(), invoke.getUnwindDest(), std::move(weak));
             }
 
-            /// Locations whose resource this call may release (model rule or summary).
-            std::vector<LocationId> releaseTargets(const llvm::CallBase& call,
-                                                   const llvm::Function* callee)
+            static bool releases(const ParamTransformer& t)
             {
-                std::vector<LocationId> targets;
-                if (!callee)
-                    return targets;
+                return t[static_cast<std::size_t>(OwnState::Owned)].has(OwnState::Released);
+            }
+
+            /// Arguments this call may release as passed (model rule or summary). With
+            /// `knownOnly`, a summary counts only where that release is not uncertain: a callee
+            /// that hands the argument to unknown code may also use it.
+            std::vector<unsigned> releasedArgs(const llvm::CallBase& call,
+                                               const llvm::Function& callee,
+                                               bool knownOnly = false) const
+            {
+                std::vector<unsigned> args;
                 for (const ResourceRule& rule : model_.rules)
                 {
-                    if (rule.action != RuleAction::ReleaseArg ||
-                        !ruleMatchesFunction(rule, *callee) || rule.argIndex >= call.arg_size())
-                        continue;
-                    targets.push_back(valueLocation(call.getArgOperand(rule.argIndex)));
+                    if (rule.action == RuleAction::ReleaseArg &&
+                        ruleMatchesFunction(rule, callee) && rule.argIndex < call.arg_size())
+                        args.push_back(rule.argIndex);
                 }
-                if (const FunctionOwnershipSummary* summary = summaries_.byFunction(*callee))
+                if (const FunctionOwnershipSummary* summary = summaries_.byFunction(callee))
                 {
-                    const auto releases = [](const ParamTransformer& t)
-                    {
-                        return t[static_cast<std::size_t>(OwnState::Owned)].has(OwnState::Released);
-                    };
                     for (const auto& [argIndex, transformer] : summary->normal.params)
                     {
                         if (argIndex < call.arg_size() && releases(transformer) &&
+                            (!knownOnly ||
+                             !transformer.isUncertain(StateSet::of(OwnState::Owned))) &&
                             call.getArgOperand(argIndex)->getType()->isPointerTy())
-                            targets.push_back(valueLocation(call.getArgOperand(argIndex)));
+                            args.push_back(argIndex);
                     }
+                }
+                return args;
+            }
+
+            /// Locations whose resource this call may release (model rule or summary).
+            std::vector<LocationId> releaseTargets(const llvm::CallBase& call,
+                                                   const llvm::Function* callee)
+            {
+                std::vector<LocationId> targets;
+                if (!callee)
+                    return targets;
+                for (const unsigned i : releasedArgs(call, *callee))
+                    targets.push_back(valueLocation(call.getArgOperand(i)));
+                if (const FunctionOwnershipSummary* summary = summaries_.byFunction(*callee))
+                {
                     for (const auto& [path, transformer] : summary->normal.pointeeParams)
                     {
                         if (!releases(transformer))
@@ -1008,6 +1123,7 @@ namespace ctrace::stack::analysis::ownership
                 edgeIndex_;
             std::map<std::string, LocationId> slotIds_;
             llvm::DenseMap<const llvm::Value*, LocationId> valueIds_;
+            llvm::DenseMap<const llvm::LoadInst*, LocationId> loadedFrom_; // the slot read
             std::map<const llvm::CallBase*, Event> exceptionalSummaryEvents_;
             std::optional<LocationId> unknownTarget_;
             LocationId returnLocation_ = 0;
diff --git a/src/app/AnalyzerApp.cpp b/src/app/AnalyzerApp.cpp
index 1c2f2670..54f3e66a 100644
--- a/src/app/AnalyzerApp.cpp
+++ b/src/app/AnalyzerApp.cpp
@@ -1633,6 +1633,10 @@ encodeOwnershipSummary(const ctrace::stack::analysis::ownership::FunctionOwnersh
 {
     llvm::json::Object obj;
     obj["incomplete"] = s.incomplete;
+    llvm::json::Array usedArgs;
+    for (const unsigned i : s.usedArgs)
+        usedArgs.push_back(static_cast<int64_t>(i));
+    obj["usedArgs"] = std::move(usedArgs);
     obj["normal"] = encodeExitTransformer(s.normal);
     obj["exceptional"] = encodeExitTransformer(s.exceptional);
     return obj;
@@ -1734,11 +1738,19 @@ decodeOwnershipSummary(const llvm::json::Object& obj,
                        ctrace::stack::analysis::ownership::FunctionOwnershipSummary& out)
 {
     const auto incomplete = obj.getBoolean("incomplete");
+    const auto* usedArgs = obj.getArray("usedArgs");
     const auto* normal = obj.getObject("normal");
     const auto* exceptional = obj.getObject("exceptional");
-    if (!incomplete || !normal || !exceptional)
+    if (!incomplete || !usedArgs || !normal || !exceptional)
         return false;
     out.incomplete = *incomplete;
+    for (const auto& value : *usedArgs)
+    {
+        const auto i = value.getAsInteger();
+        if (!i || *i < 0 || (!out.usedArgs.empty() && *i <= out.usedArgs.back()))
+            return false; // sorted and distinct: the collector searches it
+        out.usedArgs.push_back(static_cast<unsigned>(*i));
+    }
     return decodeExitTransformer(*normal, out.normal) &&
            decodeExitTransformer(*exceptional, out.exceptional);
 }
@@ -1832,7 +1844,7 @@ static bool writeSummaryCacheFile(const std::filesystem::path& cacheFile,
     }
 
     llvm::json::Object root;
-    root["schema"] = "resource-summary-cache-v5";
+    root["schema"] = "resource-summary-cache-v6";
     root["functions"] = std::move(functionArray);
 
     std::ofstream out(cacheFile, std::ios::out | std::ios::trunc | std::ios::binary);
@@ -1863,7 +1875,7 @@ readSummaryCacheFile(const std::filesystem::path& cacheFile)
     if (!obj)
         return std::nullopt;
     auto schema = obj->getString("schema");
-    if (!schema || *schema != "resource-summary-cache-v5")
+    if (!schema || *schema != "resource-summary-cache-v6")
         return std::nullopt;
 
     const auto* functions = obj->getArray("functions");
@@ -1979,8 +1991,10 @@ struct ResourceSummaryOperations
 
     std::string cacheKey(std::size_t module, const std::string& externalHash) const
     {
-        // Keep the schema and key components identical: this refactor changes no summaries.
-        return md5Hex("cross-tu-resource-summary-v5|" + modelHash + "|" + externalHash + "|" +
+        // The version moves with the file schema whenever the analyzer computes different
+        // summaries (v6: handing a released resource over leaves it released, and a summary
+        // lists the arguments the function uses).
+        return md5Hex("cross-tu-resource-summary-v6|" + modelHash + "|" + externalHash + "|" +
                       filterHash + "|" + compileArgsHashes[module] + "|" + irHashes[module]);
     }
     bool usesDiskCache() const
diff --git a/test/resource-lifetime/cross-tu-use-then-release-def.c b/test/resource-lifetime/cross-tu-use-then-release-def.c
new file mode 100644
index 00000000..e2638ffb
--- /dev/null
+++ b/test/resource-lifetime/cross-tu-use-then-release-def.c
@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: Apache-2.0
+// Driven by check_ownership_cross_tu(): callees that release their argument, after or beside an
+// access through it, or without one.
+#include <stdlib.h>
+
+void writes_then_frees_cross_tu(int* p)
+{
+    *p = 42;
+    free(p);
+}
+
+void frees_or_writes_cross_tu(int* p, int c)
+{
+    if (c)
+        free(p);
+    else
+        *p = 1;
+}
+
+void frees_cross_tu(int* p)
+{
+    free(p);
+}
diff --git a/test/resource-lifetime/cross-tu-use-then-release-use.c b/test/resource-lifetime/cross-tu-use-then-release-use.c
new file mode 100644
index 00000000..3bba2f64
--- /dev/null
+++ b/test/resource-lifetime/cross-tu-use-then-release-use.c
@@ -0,0 +1,56 @@
+// SPDX-License-Identifier: Apache-2.0
+// Driven by check_ownership_cross_tu(): the callees defined in cross-tu-use-then-release-def.c
+// release their argument. The call after a release is a use when the callee also accesses the
+// argument (lines 18 and 26), not when it only releases it. The live_ functions report no use.
+#include <stdlib.h>
+
+extern void writes_then_frees_cross_tu(int* p);
+extern void frees_or_writes_cross_tu(int* p, int c);
+extern void frees_cross_tu(int* p);
+
+// strict-diagnostic-count: false
+void released_writes_then_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    writes_then_frees_cross_tu(p);
+}
+void released_frees_or_writes(int c)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    frees_or_writes_cross_tu(p, c);
+}
+void released_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    frees_cross_tu(p); /* a double release, not a use */
+}
+void live_writes_then_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    writes_then_frees_cross_tu(p);
+}
+void live_frees_or_writes(int c)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    frees_or_writes_cross_tu(p, c);
+}
+void live_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    frees_cross_tu(p);
+}
diff --git a/test/resource-lifetime/delete-twice-with-destructor.cpp b/test/resource-lifetime/delete-twice-with-destructor.cpp
new file mode 100644
index 00000000..9f1085bd
--- /dev/null
+++ b/test/resource-lifetime/delete-twice-with-destructor.cpp
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: Apache-2.0
+// resource-model: models/resource-lifetime/generic.txt
+// Unlike new-double-delete.cpp, the second delete runs a destructor on the released object: a
+// use after release as well as a double release.
+struct Obj
+{
+    int* data;
+    ~Obj();
+};
+
+void delete_twice()
+{
+    Obj* o = new Obj();
+    delete o;
+    delete o;
+}
+
+// at line 15, column 5
+// [!!!Error] potential double release: 'CppHeap' handle 'o' is released without a matching acquire in this function
+
+// at line 15, column 12
+// [!!!Error] potential use-after-release: 'CppHeap' handle 'o' is used after a release in this function
diff --git a/test/resource-lifetime/new-double-delete.cpp b/test/resource-lifetime/new-double-delete.cpp
index ab75876a..e6c2cbff 100644
--- a/test/resource-lifetime/new-double-delete.cpp
+++ b/test/resource-lifetime/new-double-delete.cpp
@@ -8,8 +8,10 @@ int new_double_delete()
     return 0;
 }
 
-// at line 6, column 5
+// at line 7, column 5
 // [!!!Error] potential double release: 'CppHeap' handle 'p' is released without a matching acquire in this function
 
-// at line 6, column 12
-// [!!!Error] potential use-after-release: 'CppHeap' handle 'p' is used after a release in this function
+// The second `delete p` releases the memory again (the error above); its null test reads only
+// the pointer value, not the released memory. delete-twice-with-destructor.cpp keeps both
+// diagnostics, because there the destructor runs on the released object.
+// not contains: potential use-after-release: 'CppHeap' handle 'p' is used after a release in this function
diff --git a/test/resource-lifetime/use-after-release-alias.c b/test/resource-lifetime/use-after-release-alias.c
new file mode 100644
index 00000000..a7472415
--- /dev/null
+++ b/test/resource-lifetime/use-after-release-alias.c
@@ -0,0 +1,113 @@
+// SPDX-License-Identifier: Apache-2.0
+// resource-model: models/resource-lifetime/generic.txt
+// A copy of a handle keeps naming the released memory; clearing or reassigning the owner, or
+// comparing the pointer, reads no released memory.
+#include <stdlib.h>
+
+extern void consume(int* p);
+extern int* other_ptr(void);
+
+void alias_then_null(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    int* q = p;
+    free(p);
+    p = NULL; /* not a use */
+    *q = 42;  /* use after release */
+}
+
+void alias_no_null(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    int* q = p;
+    free(p);
+    *q = 42;
+}
+
+int alias_read(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return 0;
+    *p = 1;
+    int* q = p;
+    free(p);
+    return *q;
+}
+
+void null_only(void)
+{
+    int* p = malloc(sizeof *p);
+    free(p);
+    p = NULL;
+}
+
+void reassigned_before_use(void)
+{
+    int* p = malloc(sizeof *p);
+    free(p);
+    p = malloc(sizeof *p);
+    if (!p)
+        return;
+    *p = 1;
+    free(p);
+}
+
+int compare_after_release(const int* other)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return 0;
+    free(p);
+    return p == other;
+}
+
+void pass_to_external(void)
+{
+    int* h = malloc(sizeof *h);
+    if (!h)
+        return;
+    free(h);
+    consume(h);
+}
+
+void use_after_external_then_release(void)
+{
+    int* s = malloc(sizeof *s);
+    if (!s)
+        return;
+    consume(s); /* may keep or release it: unknown */
+    free(s);    /* released for certain */
+    *s = 1;     /* use after release */
+}
+
+void reassigned_from_unmodelled_callee(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    p = other_ptr(); /* not a use: the slot now holds another pointer */
+    consume(p);
+}
+
+// at line 18, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'q' is used after a release in this function
+
+// at line 28, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'q' is used after a release in this function
+
+// at line 39, column 13
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'q' is used after a release in this function
+
+// at line 75, column 13
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'h' is used after a release in this function
+
+// at line 85, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 's' is used after a release in this function
+
+// not contains: potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
diff --git a/test/resource-lifetime/use-after-release-escape-offset.c b/test/resource-lifetime/use-after-release-escape-offset.c
new file mode 100644
index 00000000..27118d82
--- /dev/null
+++ b/test/resource-lifetime/use-after-release-escape-offset.c
@@ -0,0 +1,148 @@
+// SPDX-License-Identifier: Apache-2.0
+// resource-model: models/resource-lifetime/generic.txt
+#include <stdlib.h>
+
+// Handing a released pointer over (to a global, an out parameter, a heap object, unknown code)
+// does not make the memory live again, and an address computed from it (p + 1, p++, &t->b) still
+// names the released memory. The use is the access through the pointer; the copy or the
+// computation is not. Each live_ function does the same before the release, or without one: no
+// diagnostic.
+
+struct Holder
+{
+    int* q;
+};
+struct Pair
+{
+    int a;
+    int b;
+};
+int* global;
+extern void ext_keep(int* p);
+
+void released_to_global(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    global = p;
+    *p = 42;
+}
+void released_to_out_param(int** out)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    *out = p;
+    *p = 42;
+}
+void released_to_heap_field(struct Holder* h)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    h->q = p;
+    *p = 42;
+}
+void released_then_offset(void)
+{
+    int* p = malloc(2 * sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    p = p + 1;
+    *p = 42;
+}
+void released_then_increment(void)
+{
+    int* p = malloc(2 * sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    p++;
+    *p = 42;
+}
+void released_field_address(void)
+{
+    struct Pair* t = malloc(sizeof *t);
+    if (!t)
+        return;
+    free(t);
+    int* b = &t->b;
+    *b = 42;
+}
+void released_to_unknown_code(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    ext_keep(p); /* a use: unknown code may read it */
+    *p = 42;     /* still released: the callee cannot make it live again */
+}
+
+void live_to_global(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    global = p;
+    *p = 42;
+}
+void live_to_out_param(int** out)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    *out = p;
+    *p = 42;
+}
+void live_offset(void)
+{
+    int* p = malloc(2 * sizeof *p);
+    if (!p)
+        return;
+    int* q = p + 1;
+    *q = 42;
+    free(p);
+}
+void live_field_address(void)
+{
+    struct Pair* t = malloc(sizeof *t);
+    if (!t)
+        return;
+    int* b = &t->b;
+    *b = 42;
+    free(t);
+}
+
+// Reported at the access through the pointer (and at the call that hands it to unknown code),
+// not at the copy or the address computation; the strict count checks that the live_ functions
+// report nothing.
+
+// at line 30, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 39, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 48, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 57, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 66, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 75, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'b' is used after a release in this function
+
+// at line 83, column 14
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 84, column 6
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
diff --git a/test/resource-lifetime/use-after-release-through-callee.c b/test/resource-lifetime/use-after-release-through-callee.c
new file mode 100644
index 00000000..88a2ac0a
--- /dev/null
+++ b/test/resource-lifetime/use-after-release-through-callee.c
@@ -0,0 +1,242 @@
+// SPDX-License-Identifier: Apache-2.0
+// resource-model: models/resource-lifetime/generic.txt
+#include <stdlib.h>
+
+// A call after a release is a use when the callee may need the memory alive: it writes or reads
+// through the pointer (maybe on some paths only), hands it to unknown code, or passes it on. A
+// callee that only keeps the pointer is not a use. Each live_ function makes the same call before
+// the release: no diagnostic.
+
+extern void ext_sink(int* p);
+int* kept;
+
+void writes(int* p)
+{
+    *p = 42;
+}
+int reads(const int* p)
+{
+    return *p;
+}
+void writes_if(int* p, int c)
+{
+    if (c)
+        *p = 1;
+}
+void forwards_to_external(int* p)
+{
+    ext_sink(p);
+}
+void forwards_to_local(int* p)
+{
+    writes(p);
+}
+void keeps(int* p)
+{
+    kept = p;
+}
+
+void released_writes(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    writes(p);
+}
+int released_reads(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return 0;
+    free(p);
+    return reads(p);
+}
+void released_writes_if(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    writes_if(p, 1);
+}
+void released_forwards_to_external(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    forwards_to_external(p);
+}
+void released_forwards_to_local(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    forwards_to_local(p);
+}
+void released_indirect(void (*fp)(int*))
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    fp(p);
+}
+void released_keeps(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    keeps(p); /* only keeps the pointer: not a use */
+}
+
+void live_writes(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    writes(p);
+    free(p);
+}
+int live_reads(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return 0;
+    const int v = reads(p);
+    free(p);
+    return v;
+}
+void live_writes_if(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    writes_if(p, 1);
+    free(p);
+}
+void live_forwards_to_local(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    forwards_to_local(p);
+    free(p);
+}
+void live_indirect(void (*fp)(int*))
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    fp(p);
+    free(p);
+}
+
+// A callee that releases the pointer is still a use when it also accesses it, on the same path
+// or on another one. A callee that only releases it is no use: the second release is reported
+// as a double release only.
+void writes_then_frees(int* p)
+{
+    *p = 42;
+    free(p);
+}
+void frees_or_writes(int* p, int c)
+{
+    if (c)
+        free(p);
+    else
+        *p = 1;
+}
+void frees(int* p)
+{
+    free(p);
+}
+
+void released_writes_then_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    writes_then_frees(p);
+}
+void released_frees_or_writes(int c)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    frees_or_writes(p, c);
+}
+void released_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    free(p);
+    frees(p); /* a double release, not a use */
+}
+void live_writes_then_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    writes_then_frees(p);
+}
+void live_frees_or_writes(int c)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    frees_or_writes(p, c);
+}
+void live_frees(void)
+{
+    int* p = malloc(sizeof *p);
+    if (!p)
+        return;
+    frees(p);
+}
+
+// Reported at the argument of each released_ call except released_keeps and released_frees;
+// the strict count checks that those and the live_ functions report nothing else. The only
+// other diagnostics are the double releases and the leak live_frees_or_writes may cause.
+
+// at line 45, column 12
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 53, column 18
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 61, column 15
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 69, column 26
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 77, column 23
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 85, column 8
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 164, column 23
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 164, column 5
+// [!!!Error] potential double release: 'HeapAlloc' handle 'p' is released without a matching acquire in this function
+
+// at line 172, column 21
+// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
+
+// at line 172, column 5
+// [!!!Error] potential double release: 'HeapAlloc' handle 'p' is released without a matching acquire in this function
+
+// at line 180, column 5
+// [!!!Error] potential double release: 'HeapAlloc' handle 'p' is released without a matching acquire in this function
+
+// at line 191, column 14
+// [ !!Warn ] potential resource leak: 'HeapAlloc' acquired in handle 'p' may leave the function without being released
diff --git a/test/security/null-dereference/05_null_deref.c b/test/security/null-dereference/05_null_deref.c
index cde098f1..ab8848f5 100644
--- a/test/security/null-dereference/05_null_deref.c
+++ b/test/security/null-dereference/05_null_deref.c
@@ -68,10 +68,6 @@ int main(void)
 // [!!!Error] potential null pointer dereference on '<pointer>'
 // ↳ a preceding local-slot store sets the pointer to null before use
 
-// at line 31, column 7
-// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
-// ↳ a later dereference/call argument use may access invalid memory
-
-// at line 32, column 27
-// [!!!Error] potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
-// ↳ a later dereference/call argument use may access invalid memory
+// vuln_null_after_free: `p = NULL` overwrites the handle and reads no released memory; `*p` then
+// dereferences null (the error above), not the released allocation.
+// not contains: potential use-after-release: 'HeapAlloc' handle 'p' is used after a release in this function
diff --git a/test/unit/analyzer_module_unit_tests.cpp b/test/unit/analyzer_module_unit_tests.cpp
index f1e8ca0f..82fa8b97 100644
--- a/test/unit/analyzer_module_unit_tests.cpp
+++ b/test/unit/analyzer_module_unit_tests.cpp
@@ -16,6 +16,7 @@
 #include "analysis/Reachability.hpp"
 #include "analysis/ResourceLifetimeAnalysis.hpp"
 #include "analysis/ResourceModel.hpp"
+#include "analysis/ownership/OwnershipEngine.hpp"
 #include "analysis/ownership/ResourceFactCollector.hpp"
 #include "analysis/StackBufferAnalysis.hpp"
 #include "analysis/UninitializedVarAnalysis.hpp"
@@ -1416,6 +1417,139 @@ namespace
             report.expect(count(blocks, Kind::AddressEscape) == 1,
                           "OwnershipCollector: passing &h to an unmodelled callee");
         }
+        // The Use events of a function, by the name of the slot each one is read from.
+        const auto usesOf = [&](const char* name, const SummaryLookup& summaries)
+        {
+            std::vector<std::string> names;
+            llvm::Function* fn = loaded.module->getFunction(name);
+            if (!fn)
+                return names;
+            const CollectedFunction c =
+                collectOwnershipFacts(*fn, model, summaries, loaded.module->getDataLayout());
+            const auto add = [&](const Event& e)
+            {
+                if (e.kind == Kind::Use)
+                    names.push_back(c.locationIsSlot[e.dst] ? c.locationNames[e.dst]
+                                                            : std::string("<value>"));
+            };
+            for (const Block& b : c.facts.blocks)
+                for (const Event& e : b.events)
+                    add(e);
+            for (const Edge& edge : c.facts.edges)
+                for (const Event& e : edge.events)
+                    add(e);
+            return names;
+        };
+        report.expect(usesOf("use_kinds", noSummaries) == std::vector<std::string>{"p", "q", "p"},
+                      "OwnershipCollector: a store through the pointer, a memset and an external "
+                      "callee are uses; a copy, a comparison, the released argument and a "
+                      "reassignment are not");
+        report.expect(usesOf("use_return", noSummaries) == std::vector<std::string>{"<value>"},
+                      "OwnershipCollector: returning the pointer is a use, named by its resource");
+
+        // A call to a defined function is a use of the arguments its summary uses; without a
+        // summary, or through a pointer, the callee is unknown and the call is a use.
+        FunctionOwnershipSummary usesFirst;
+        usesFirst.usedArgs = {0};
+        FunctionOwnershipSummary keepsOnly;
+        const SummaryLookup bodies{[&](const llvm::Function& fn) -> const FunctionOwnershipSummary*
+                                   {
+                                       if (fn.getName() == "callee_uses")
+                                           return &usesFirst;
+                                       if (fn.getName() == "callee_keeps")
+                                           return &keepsOnly;
+                                       return nullptr;
+                                   }};
+        report.expect(usesOf("use_callees", bodies) == std::vector<std::string>{"p", "p"},
+                      "OwnershipCollector: a defined callee that uses the argument and an "
+                      "indirect call are uses; a callee that only keeps the pointer is not");
+        report.expect(usesOf("use_callees", noSummaries) == std::vector<std::string>{"p", "p", "p"},
+                      "OwnershipCollector: a defined callee without a summary is a use");
+        keepsOnly.incomplete = true;
+        report.expect(usesOf("use_callees", bodies) == std::vector<std::string>{"p", "p", "p"},
+                      "OwnershipCollector: a defined callee with an incomplete summary is a use");
+        const auto usedArgsOf = [&](const char* name)
+        {
+            const llvm::Function* fn = loaded.module->getFunction(name);
+            if (!fn)
+                return std::vector<unsigned>{99};
+            return computeSummary(collectOwnershipFacts(*fn, model, noSummaries,
+                                                        loaded.module->getDataLayout())
+                                      .facts)
+                .usedArgs;
+        };
+        report.expect(usedArgsOf("callee_uses") == std::vector<unsigned>{0},
+                      "OwnershipSummary: a store through the parameter uses it");
+        report.expect(usedArgsOf("callee_keeps").empty(),
+                      "OwnershipSummary: storing the parameter somewhere does not use it");
+        if (const llvm::Function* fn = loaded.module->getFunction("callee_forwards"))
+        {
+            const FunctionOwnershipSummary forwards = computeSummary(
+                collectOwnershipFacts(*fn, model, noSummaries, loaded.module->getDataLayout())
+                    .facts);
+            const SummaryLookup forwarding{
+                [&](const llvm::Function& callee) -> const FunctionOwnershipSummary*
+                { return callee.getName() == "callee_forwards" ? &forwards : nullptr; }};
+            report.expect(usesOf("use_wrapped", forwarding) == std::vector<std::string>{"p"},
+                          "OwnershipCollector: an argument a callee hands to unknown code is a "
+                          "use, though that callee may release it");
+        }
+        else
+        {
+            report.expect(false, "OwnershipCollector: callee_forwards collected");
+        }
+
+        // p = p + 1 keeps the resource in p: releasing p then releases it.
+        if (const llvm::Function* fn = loaded.module->getFunction("offset_reassign"))
+        {
+            const CollectedFunction c =
+                collectOwnershipFacts(*fn, model, noSummaries, loaded.module->getDataLayout());
+            const OwnershipResult res = solve(
+                c.facts, AbstractState::entry(2u * c.facts.siteCount, c.facts.locations.size()));
+            report.expect(
+                res.exits.size() == 1 &&
+                    res.exits[0].state.resources[newInstanceOf(0)].isOnly(OwnState::Released),
+                "OwnershipCollector: an address computed from the handle carries its "
+                "resource");
+        }
+        else
+        {
+            report.expect(false, "OwnershipCollector: offset_reassign collected");
+        }
+
+        // Releasing an argument does not hide a use of it in the same callee.
+        const auto summaryOf = [&](const char* name)
+        {
+            const llvm::Function* fn = loaded.module->getFunction(name);
+            return fn ? computeSummary(collectOwnershipFacts(*fn, model, noSummaries,
+                                                             loaded.module->getDataLayout())
+                                           .facts)
+                      : FunctionOwnershipSummary{};
+        };
+        const FunctionOwnershipSummary usesThenReleases = summaryOf("callee_uses_then_releases");
+        const FunctionOwnershipSummary releasesOnly = summaryOf("callee_releases");
+        const auto releasesFirstArg = [](const FunctionOwnershipSummary& s)
+        {
+            const auto it = s.normal.params.find(0);
+            return it != s.normal.params.end() &&
+                   it->second[static_cast<std::size_t>(OwnState::Owned)].has(OwnState::Released);
+        };
+        report.expect(releasesFirstArg(usesThenReleases) && releasesFirstArg(releasesOnly) &&
+                          usesThenReleases.usedArgs == std::vector<unsigned>{0} &&
+                          releasesOnly.usedArgs.empty(),
+                      "OwnershipSummary: both callees release the argument, one also uses it");
+        const SummaryLookup releasing{
+            [&](const llvm::Function& fn) -> const FunctionOwnershipSummary*
+            {
+                if (fn.getName() == "callee_uses_then_releases")
+                    return &usesThenReleases;
+                if (fn.getName() == "callee_releases")
+                    return &releasesOnly;
+                return nullptr;
+            }};
+        report.expect(usesOf("use_releasing_callees", releasing) == std::vector<std::string>{"p"},
+                      "OwnershipCollector: a callee that uses the argument it releases is a use; "
+                      "one that only releases it is not");
         return report.failures == 0;
     }
     bool testOwnershipCollectorExceptions(const std::filesystem::path& repoRoot, TestReport& report)
diff --git a/test/unit/ownership_collector_input.c b/test/unit/ownership_collector_input.c
index 3b1ca581..c5a8ccca 100644
--- a/test/unit/ownership_collector_input.c
+++ b/test/unit/ownership_collector_input.c
@@ -42,3 +42,82 @@ void unknown_call(void)
     unknown_sink(h);
     unknown_out(&h);
 }
+
+/* Which uses of a pointer are Use events. */
+int use_kinds(char* other)
+{
+    char* p = acquire_ret();
+    char* q = p;    /* copy into a slot: not a use */
+    if (p == other) /* comparison: not a use */
+        return 0;
+    *p = 1;                    /* store through the pointer: a use */
+    __builtin_memset(q, 0, 1); /* memory intrinsic: a use */
+    unknown_sink(p);           /* external callee: a use (conservative) */
+    release_handle(p);         /* the released argument: not a use */
+    p = 0;                     /* reassignment: not a use */
+    return 1;
+}
+
+char* use_return(void)
+{
+    char* p = acquire_ret();
+    release_handle(p);
+    return p; /* the pointer leaves the function: a use */
+}
+
+/* Calls to defined functions: a use when the callee's body may use the argument. */
+static char* kept;
+void callee_uses(char* p)
+{
+    *p = 1; /* a use of the parameter */
+}
+void callee_keeps(char* p)
+{
+    kept = p; /* only stores the pointer: no use */
+}
+int use_callees(void (*fp)(char*))
+{
+    char* p = acquire_ret();
+    callee_uses(p);  /* a use: the callee's summary says it uses the argument */
+    callee_keeps(p); /* not a use: the callee only keeps it */
+    fp(p);           /* indirect call: an unknown callee, a use */
+    release_handle(p);
+    return 0;
+}
+
+void callee_forwards(char* p)
+{
+    unknown_sink(p); /* unknown code: may use the pointer, may release it */
+}
+void use_wrapped(void)
+{
+    char* p = acquire_ret();
+    callee_forwards(p); /* a use, though the callee's summary says it may release */
+}
+
+/* An address computed from the handle carries its resource. */
+void offset_reassign(void)
+{
+    char* p = acquire_ret();
+    p = p + 1;
+    release_handle(p);
+}
+
+/* A callee that uses its argument and also releases it still uses it; one that only releases
+   it does not. */
+void callee_uses_then_releases(char* p)
+{
+    *p = 1;
+    release_handle(p);
+}
+void callee_releases(char* p)
+{
+    release_handle(p);
+}
+void use_releasing_callees(void)
+{
+    char* p = acquire_ret();
+    callee_uses_then_releases(p); /* a use, though the callee also releases it */
+    char* q = acquire_ret();
+    callee_releases(q); /* not a use: the callee only releases it */
+}
diff --git a/test/unit/ownership_engine_unit_tests.cpp b/test/unit/ownership_engine_unit_tests.cpp
index b3150cda..360c6c2f 100644
--- a/test/unit/ownership_engine_unit_tests.cpp
+++ b/test/unit/ownership_engine_unit_tests.cpp
@@ -139,6 +139,16 @@ namespace
         e.call.params.push_back({loc, t});
         return e;
     }
+    /// A use of what `src` holds; `id` stands for the instruction, to tell uses apart.
+    Event use(LocationId src, std::uint32_t id)
+    {
+        Event e;
+        e.kind = Event::Kind::Use;
+        e.src = src;
+        e.dst = src;
+        e.instructionIndex = id;
+        return e;
+    }
 
     OwnershipFacts facts(std::size_t blocks, std::vector<Edge> edges, std::size_t locations,
                          std::uint32_t sites)
@@ -981,6 +991,197 @@ namespace
         }
         return r.failures == 0;
     }
+    // Location 0 is the owner `p`, location 1 an alias `q`.
+    bool testUses(TestReport& r)
+    {
+        using Ids = std::vector<std::uint32_t>;
+        const ResourceId n0 = newInstanceOf(0);
+        const ResourceId o0 = oldInstancesOf(0);
+        const auto reported = [](const OwnershipFacts& f, unsigned limit = 0)
+        {
+            const OwnershipResult res = solve(f, entryOf(f), limit);
+            std::vector<std::pair<std::uint32_t, ResourceId>> out;
+            for (const ReleasedUse& u : releasedUses(f, res))
+                out.push_back({u.use->instructionIndex, u.resource});
+            return out;
+        };
+        const auto ids = [&](const OwnershipFacts& f)
+        {
+            Ids out;
+            for (const auto& [id, resource] : reported(f))
+                out.push_back(id);
+            return out;
+        };
+
+        {
+            OwnershipFacts with = facts(1, {}, 1, 1);
+            with.blocks[0].events = {acquire(0, 0), use(0, 1), release(0), use(0, 2), exit()};
+            OwnershipFacts without = facts(1, {}, 1, 1);
+            without.blocks[0].events = {acquire(0, 0), release(0), exit()};
+            const OwnershipResult a = solve(with, entryOf(with));
+            const OwnershipResult b = solve(without, entryOf(without));
+            r.expect(a.out == b.out && a.exits.size() == 1 && a.exits[0].state == b.exits[0].state,
+                     "Uses: a use leaves the state unchanged");
+        }
+        {
+            OwnershipFacts f = facts(1, {}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0), use(0, 1), release(0), use(0, 2), exit()};
+            const auto found = reported(f);
+            r.expect(found.size() == 1 && found[0].first == 2 && found[0].second == n0,
+                     "Uses: only the use after the release is reported");
+        }
+        {
+            // q = p; free(p); p = NULL; use p; use q.
+            OwnershipFacts f = facts(1, {}, 2, 1);
+            f.blocks[0].events = {acquire(0, 0), copy(1, 0), release(0), overwrite(0),
+                                  use(0, 1),     use(1, 2),  exit()};
+            r.expect(ids(f) == Ids{2},
+                     "Uses: the alias still holds the released resource, the cleared owner not");
+        }
+        {
+            // free(p); p = acquire(); use p.
+            OwnershipFacts f = facts(1, {}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0), release(0), acquire(0, 0), use(0, 1), exit()};
+            r.expect(ids(f).empty(), "Uses: a reacquired owner holds the new, live instance");
+        }
+        {
+            // saved = p; p = acquire(); free(saved); use saved.
+            OwnershipFacts f = facts(1, {}, 2, 1);
+            f.blocks[0].events = {acquire(0, 0), copy(1, 0), acquire(0, 0),
+                                  release(1),    use(1, 1),  exit()};
+            const auto found = reported(f);
+            r.expect(found.size() == 1 && found[0].first == 1 && found[0].second == o0,
+                     "Uses: an older instance released through its alias is reported");
+        }
+        {
+            // Loop body: p = acquire(); use p; free(p). Only earlier instances are released.
+            OwnershipFacts f = facts(3, {edge(0, 1), edge(1, 1), edge(1, 2)}, 1, 1);
+            f.blocks[1].events = {acquire(0, 0), use(0, 1), release(0)};
+            f.blocks[2].events = {exit()};
+            r.expect(ids(f).empty(), "Uses: an instance released on an earlier iteration is "
+                                     "not the one used");
+        }
+        {
+            // 0 → 1 (free) → 3, 0 → 2 → 3; 3: use p.
+            OwnershipFacts f =
+                facts(4, {edge(0, 1, {release(0)}), edge(0, 2), edge(1, 3), edge(2, 3)}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0)};
+            f.blocks[3].events = {use(0, 1), exit()};
+            r.expect(ids(f) == Ids{1}, "Uses: a release on one path is a potential use after "
+                                       "release");
+        }
+        {
+            OwnershipFacts f = facts(1, {}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0), addressEscape(0), release(0), use(0, 1), exit()};
+            r.expect(ids(f).empty(), "Uses: an uncertain resource is not judged");
+        }
+        {
+            Event unknown;
+            unknown.kind = Event::Kind::UnknownCall;
+            unknown.args = {0};
+            OwnershipFacts f = facts(1, {}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0), unknown, use(0, 1), exit()};
+            r.expect(ids(f).empty(),
+                     "Uses: an unknown call that may release does not make later uses reported");
+            f.blocks[0].events = {acquire(0, 0), unknown, release(0), use(0, 1), exit()};
+            r.expect(ids(f) == Ids{1},
+                     "Uses: a certain release is judged even after an unknown call");
+            f.blocks[0].events = {acquire(0, 0), release(0), unknown, use(0, 1), exit()};
+            r.expect(ids(f) == Ids{1},
+                     "Uses: unknown code handed a released pointer cannot make it live again");
+        }
+        {
+            // A merged return block split onto its incoming edge.
+            OwnershipFacts f = facts(2, {edge(0, 1, {use(0, 1)})}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0), release(0)};
+            f.blocks[1].events = {exit()};
+            r.expect(ids(f) == Ids{1}, "Uses: a use on an edge is judged with the edge's state");
+        }
+        {
+            OwnershipFacts f = facts(2, {}, 1, 1);
+            f.blocks[0].events = {acquire(0, 0), release(0), exit()};
+            f.blocks[1].events = {use(0, 1)};
+            r.expect(ids(f).empty(), "Uses: an unreachable use is not reported");
+        }
+        {
+            OwnershipFacts f = facts(3, {edge(0, 1), edge(1, 1), edge(1, 2)}, 1, 1);
+            f.blocks[1].events = {acquire(0, 0), release(0), use(0, 1)};
+            f.blocks[2].events = {exit()};
+            r.expect(reported(f, /*limit=*/1).empty(),
+                     "Uses: nothing is reported from an incomplete solve");
+        }
+        {
+            // free(p); global = p; use p. Location 1 is a global, then an out parameter.
+            OwnershipFacts f = facts(1, {}, 2, 1);
+            f.locations[1].kind = LocationKind::NonLocal;
+            f.blocks[0].events = {acquire(0, 0), release(0), copy(1, 0), use(0, 1), exit()};
+            r.expect(ids(f) == Ids{1},
+                     "Uses: a released resource copied into a global stays released");
+            f.locations[1].kind = LocationKind::ArgPointee;
+            r.expect(ids(f) == Ids{1},
+                     "Uses: a released resource stored through an out parameter stays released");
+        }
+        {
+            // Released on one path, then global = p: handed over where it was live only.
+            OwnershipFacts f =
+                facts(4, {edge(0, 1, {release(0)}), edge(0, 2), edge(1, 3), edge(2, 3)}, 2, 1);
+            f.locations[1].kind = LocationKind::NonLocal;
+            f.blocks[0].events = {acquire(0, 0)};
+            f.blocks[3].events = {copy(1, 0), use(0, 1), exit()};
+            const StateSet st = solve(f, entryOf(f)).exits.at(0).state.resources[n0];
+            r.expect(st.has(OwnState::Escaped) && st.has(OwnState::Released) &&
+                         !st.has(OwnState::Owned),
+                     "Uses: handing a resource over keeps the path where it was released");
+            r.expect(ids(f) == Ids{1}, "Uses: a use after that hand-over is still judged");
+        }
+        {
+            // free(p); return p.
+            OwnershipFacts f = facts(1, {}, 2, 1);
+            f.blocks[0].events = {acquire(0, 0), release(0), copy(1, 0), ret(1), exit()};
+            r.expect(
+                solve(f, entryOf(f)).exits.at(0).state.resources[n0].isOnly(OwnState::Released),
+                "Uses: returning a released resource leaves it released");
+        }
+        return r.failures == 0;
+    }
+
+    // Which arguments a function may use, read off its summary.
+    bool testUsedArgs(TestReport& r)
+    {
+        using Args = std::vector<unsigned>;
+        {
+            // Argument 2 at location 1, copied to location 2, used on one path only.
+            OwnershipFacts f = facts(3, {edge(0, 1), edge(0, 2)}, 3, 0);
+            f.paramLocations = {{0, 0}, {2, 1}};
+            f.blocks[0].events = {copy(2, 1)};
+            f.blocks[1].events = {use(2, 1), exit()};
+            f.blocks[2].events = {exit()};
+            r.expect(computeSummary(f).usedArgs == Args{2},
+                     "UsedArgs: a use through a copy, on one path, of argument 2 only");
+        }
+        {
+            OwnershipFacts f = facts(2, {}, 1, 0);
+            f.paramLocations = {{0, 0}};
+            f.blocks[0].events = {exit()};
+            f.blocks[1].events = {use(0, 1)};
+            r.expect(computeSummary(f).usedArgs.empty(),
+                     "UsedArgs: an unreachable use does not count");
+        }
+        {
+            OwnershipFacts f = facts(1, {}, 2, 1);
+            f.paramLocations = {{0, 0}};
+            f.blocks[0].events = {acquire(0, 1), use(1, 1), exit()};
+            r.expect(computeSummary(f).usedArgs.empty(),
+                     "UsedArgs: a use of the function's own resource is no argument's");
+        }
+        {
+            FunctionOwnershipSummary a;
+            FunctionOwnershipSummary b;
+            b.usedArgs = {0};
+            r.expect(!sameSummary(a, b), "UsedArgs: two summaries differ by their used arguments");
+        }
+        return r.failures == 0;
+    }
 } // namespace
 
 int main(int, char**)
@@ -988,6 +1189,8 @@ int main(int, char**)
     TestReport report;
     (void)testDomain(report);
     (void)testEngine(report);
+    (void)testUses(report);
+    (void)testUsedArgs(report);
     (void)testContracts(report);
     (void)testEdgeExits(report);
     (void)testExitUncertainty(report);