diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36ea3489..a401800e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,21 @@ Notable changes are grouped by release. See [all releases](https://github.com/Co
 
 ## Unreleased
 
+- An index-bounds pilot bounds `buf[i]` on a stack array, indexed directly rather than through
+  a pointer, with ScalarEvolution. It works on a copy of the function whose local variables live
+  in registers; the analyzed IR is unchanged. An index the copy proves in bounds no longer gets a
+  report, such as `buf[i + 1]` in `for (i = 0; i < 10; i += 2)`. An index that leaves the array
+  on every run of the function that returns is a Warning under the new rules
+  `StackBufferOverflow.EveryRun` and `NegativeStackIndex.EveryRun`, and its message no longer
+  says "potential". A range that only may leave the array is still a "potential" Warning, now
+  also found when a parameter guarded before the loop sets its count. An access in a loop that
+  runs no iteration gets the "this access appears unreachable" note. Where the copy does not
+  bound the index, the existing result stays.
+- Stack buffer overflow checks no longer take the store of an element's address, such as
+  `char* end = &buf[10]` or the end of a range-based `for`, for a write to that element.
+  Forming a pointer one past the end is valid C and C++. A write through such a pointer kept in
+  a local variable is not reported either: it used to be reported only by that mistake, on the
+  line that formed the address.
 - VLA sizes, local stack sizes and the "this access appears unreachable" note on buffer
   overflows read a local variable from the store that last wrote it, as MemorySSA finds it, and
   apply casts to it. They used to take the last constant stored anywhere in the function. A
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 516ff4c8..0b17b515 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -92,6 +92,7 @@ set(STACK_ANALYZER_SOURCES
     src/analysis/NullDerefAnalysis.cpp
     src/analysis/OOBReadAnalysis.cpp
     src/analysis/ParameterDebugBinding.cpp
+    src/analysis/PromotedValues.cpp
     src/analysis/ResourceLifetimeAnalysis.cpp
     src/analysis/Reachability.cpp
     src/analysis/SizeMinusKWrites.cpp
@@ -227,6 +228,7 @@ else()
       core
       irreader
       support
+      transformutils
     )
     target_link_libraries(stack_usage_analyzer_lib
         PUBLIC
diff --git a/include/analysis/FunctionFacts.hpp b/include/analysis/FunctionFacts.hpp
index 9b409102..7094d319 100644
--- a/include/analysis/FunctionFacts.hpp
+++ b/include/analysis/FunctionFacts.hpp
@@ -31,8 +31,7 @@ namespace ctrace::stack::analysis
     /// ScalarEvolution is deliberately absent. The analyzer reads -O0 IR, where a loop
     /// counter lives in a multiply-assigned alloca that SCEV cannot see through, and the
     /// arithmetic it would bound carries nsw, which @ref computeIntRanges refuses on purpose.
-    /// Wiring it in changed no result on any fixture; add it back only alongside a pass that
-    /// promotes locals to registers.
+    /// @ref PromotedValues runs it on a promoted, sanitized copy of the module instead.
     class FunctionFacts final
     {
       public:
diff --git a/include/analysis/PromotedValues.hpp b/include/analysis/PromotedValues.hpp
new file mode 100644
index 00000000..79cdf77a
--- /dev/null
+++ b/include/analysis/PromotedValues.hpp
@@ -0,0 +1,80 @@
+// SPDX-License-Identifier: Apache-2.0
+#pragma once
+
+#include <cstdint>
+#include <functional>
+#include <memory>
+
+namespace llvm
+{
+    class Function;
+    class Instruction;
+    class Module;
+    class Value;
+} // namespace llvm
+
+namespace ctrace::stack::analysis
+{
+    /// @brief The values an index takes where its access runs.
+    struct IndexValues
+    {
+        enum class Kind : std::uint32_t
+        {
+            Unknown,   ///< Nothing is established, or the case is outside the conditions.
+            NeverRuns, ///< The access never runs: a loop around it runs no iteration.
+            Range,     ///< Every value the index takes where the access runs is in [min, max].
+        };
+
+        std::int64_t min = 0;
+        std::int64_t max = 0;
+        Kind kind = Kind::Unknown;
+        /// Range only: on every run of the function that returns, the access runs with the
+        /// index equal to this endpoint.
+        std::uint32_t minOnEveryRun : 1 = false;
+        std::uint32_t maxOnEveryRun : 1 = false;
+        std::uint32_t reservedFlags : 30 = 0;
+    };
+
+    /// @brief Value queries about the original IR, answered on a copy of the module where
+    /// promotable locals live in registers, so ScalarEvolution sees loop counters.
+    ///
+    /// The original IR stays the input of every analysis: the copy only answers questions about
+    /// the values original instructions compute. It is sanitized so that its facts hold for the
+    /// original program:
+    /// - each promotable slot starts with an opaque value, so a read that may be uninitialized
+    ///   stays unknown instead of taking the value of a later store;
+    /// - the wrap and poison flags (nsw, nuw, exact, inbounds, nneg, disjoint, samesign),
+    ///   optnone, the mustprogress and willreturn attributes and the loop metadata are dropped,
+    ///   so no fact rests on undefined behavior or on a forward-progress promise;
+    /// - functions with lifetime markers are left out.
+    ///
+    /// Index ranges use the endpoint method: they cover affine recurrences whose no-wrap
+    /// ScalarEvolution proves, in loops that exit only from their header, with every input
+    /// bounded by the program rather than by its type. Anything else is Kind::Unknown.
+    class PromotedValues final
+    {
+      public:
+        /// Copies the declarations of @p module. A function @p shouldCopy accepts is copied and
+        /// promoted on its first query; only the last function queried is kept.
+        PromotedValues(const llvm::Module& module,
+                       const std::function<bool(const llvm::Function&)>& shouldCopy);
+        ~PromotedValues();
+
+        PromotedValues(const PromotedValues&) = delete;
+        PromotedValues& operator=(const PromotedValues&) = delete;
+
+        /// Values @p index takes where @p access runs. Both belong to the original IR. Pass the
+        /// load or store itself, not the address it uses: the conditions it runs on count.
+        [[nodiscard]] IndexValues indexValuesAt(const llvm::Instruction& access,
+                                                const llvm::Value& index);
+
+        /// Whether ScalarEvolution proves @p lower <= @p index < @p upper wherever @p access
+        /// runs, reading the index as signed.
+        [[nodiscard]] bool provesWithin(const llvm::Instruction& access, const llvm::Value& index,
+                                        std::int64_t lower, std::int64_t upper);
+
+      private:
+        struct Impl;
+        std::unique_ptr<Impl> impl_;
+    };
+} // namespace ctrace::stack::analysis
diff --git a/include/analysis/StackBufferAnalysis.hpp b/include/analysis/StackBufferAnalysis.hpp
index af1062d5..77a90c95 100644
--- a/include/analysis/StackBufferAnalysis.hpp
+++ b/include/analysis/StackBufferAnalysis.hpp
@@ -39,7 +39,12 @@ namespace ctrace::stack::analysis
         std::uint64_t indexIsConstant : 1 = false;
         // Violation based on a lower bound (index potentially negative)
         std::uint64_t isLowerBoundViolation : 1 = false;
-        std::uint64_t reservedFlags : 61 = 0;
+        // The access runs with the index at the reported bound on every run of the function
+        // that returns.
+        std::uint64_t reachedOnEveryRun : 1 = false;
+        // A loop around the access runs no iteration, so the access never runs.
+        std::uint64_t neverRuns : 1 = false;
+        std::uint64_t reservedFlags : 59 = 0;
         // Optional : helper for sync string <- vector
         void rebuildAliasPathString(const std::string& sep = " -> ")
         {
diff --git a/src/analysis/PromotedValues.cpp b/src/analysis/PromotedValues.cpp
new file mode 100644
index 00000000..3fb87149
--- /dev/null
+++ b/src/analysis/PromotedValues.cpp
@@ -0,0 +1,409 @@
+// SPDX-License-Identifier: Apache-2.0
+#include "analysis/PromotedValues.hpp"
+
+#include <optional>
+#include <string>
+#include <vector>
+
+#include <llvm/ADT/STLExtras.h>
+#include <llvm/ADT/SmallVector.h>
+#include <llvm/Analysis/AssumptionCache.h>
+#include <llvm/Analysis/LoopInfo.h>
+#include <llvm/Analysis/PostDominators.h>
+#include <llvm/Analysis/ScalarEvolution.h>
+#include <llvm/Analysis/ScalarEvolutionExpressions.h>
+#include <llvm/Analysis/TargetLibraryInfo.h>
+#include <llvm/IR/ConstantRange.h>
+#include <llvm/IR/Dominators.h>
+#include <llvm/IR/IRBuilder.h>
+#include <llvm/IR/InstIterator.h>
+#include <llvm/IR/Instructions.h>
+#include <llvm/IR/Module.h>
+#include <llvm/Support/raw_ostream.h>
+#include <llvm/TargetParser/Triple.h>
+#include <llvm/Transforms/Utils/Cloning.h>
+#include <llvm/Transforms/Utils/PromoteMemToReg.h>
+
+namespace ctrace::stack::analysis
+{
+    namespace
+    {
+        using namespace llvm;
+
+        /// Analyses of one promoted function of the copy.
+        struct PromotedFunction final
+        {
+            PromotedFunction(Function& f, const TargetLibraryInfoImpl& libraryInfoImpl)
+                : function(f), libraryInfo(libraryInfoImpl, &f), assumptions(f), dominators(f),
+                  loops(dominators), postDominators(f),
+                  scev(f, libraryInfo, assumptions, dominators, loops)
+            {
+            }
+
+            Function& function;
+            TargetLibraryInfo libraryInfo;
+            AssumptionCache assumptions;
+            DominatorTree dominators;
+            LoopInfo loops;
+            PostDominatorTree postDominators;
+            ScalarEvolution scev;
+        };
+
+        bool hasLifetimeMarkers(const Function& function)
+        {
+            return any_of(instructions(function),
+                          [](const Instruction& I) { return I.isLifetimeStartOrEnd(); });
+        }
+
+        /// Drops what lets LLVM derive facts from undefined behavior or from a promise of
+        /// forward progress, which the original program does not keep.
+        void sanitize(Function& function)
+        {
+            function.removeFnAttr(Attribute::OptimizeNone);
+            function.removeFnAttr(Attribute::MustProgress);
+            function.removeFnAttr(Attribute::WillReturn);
+            for (Instruction& I : instructions(function))
+            {
+                I.dropPoisonGeneratingFlags();
+                if (auto* compare = dyn_cast<ICmpInst>(&I))
+                    compare->setSameSign(false);
+                I.setMetadata(LLVMContext::MD_loop, nullptr);
+            }
+        }
+
+        /// Promotes the promotable slots to registers, each starting from an opaque value: with
+        /// none, mem2reg would give a read that may be uninitialized the value of a later store.
+        void promote(Function& function)
+        {
+            std::vector<AllocaInst*> slots;
+            for (Instruction& I : function.getEntryBlock())
+            {
+                if (auto* slot = dyn_cast<AllocaInst>(&I); slot && isAllocaPromotable(slot))
+                    slots.push_back(slot);
+            }
+            if (slots.empty())
+                return;
+
+            Module& module = *function.getParent();
+            for (AllocaInst* slot : slots)
+            {
+                Type* type = slot->getAllocatedType();
+                std::string name = "ct.unknown.";
+                raw_string_ostream nameStream(name);
+                type->print(nameStream);
+                const FunctionCallee unknown =
+                    module.getOrInsertFunction(name, FunctionType::get(type, false));
+                IRBuilder<> builder(slot->getNextNode());
+                builder.CreateStore(builder.CreateCall(unknown), slot);
+            }
+
+            DominatorTree dominators(function);
+            PromoteMemToReg(slots, dominators);
+        }
+
+        /// True when @p block provably never runs: a loop around it exits in its header
+        /// before any iteration. With another exit (a break), a zero backedge count does not
+        /// mean the body never ran, so only the header-exit shape counts.
+        bool neverRuns(ScalarEvolution& scev, const LoopInfo& loops, const BasicBlock* block)
+        {
+            for (const Loop* loop = loops.getLoopFor(block); loop; loop = loop->getParentLoop())
+            {
+                if (block == loop->getHeader() || loop->getExitingBlock() != loop->getHeader())
+                    continue;
+                if (scev.getBackedgeTakenCount(loop)->isZero())
+                    return true;
+            }
+            return false;
+        }
+
+        /// The values of @p value at its first and last iteration, for each loop it recurs in,
+        /// where @p block runs. False when they do not bound the values soundly.
+        bool endpoints(ScalarEvolution& scev, const LoopInfo& loops, const SCEV* value,
+                       const BasicBlock* block, SmallVectorImpl<const SCEV*>& out)
+        {
+            const auto* recurrence = dyn_cast<SCEVAddRecExpr>(value);
+            if (!recurrence)
+            {
+                // A value that varies in the loop but is not a recurrence has no endpoints. One
+                // that holds a recurrence of a loop around another block, such as the value a
+                // previous loop left, has no endpoint here either: its range is that of every
+                // iteration of that loop.
+                if (scev.containsAddRecurrence(value))
+                    return false;
+                for (const Loop* loop = loops.getLoopFor(block); loop; loop = loop->getParentLoop())
+                {
+                    if (!scev.isLoopInvariant(value, loop))
+                        return false;
+                }
+                out.push_back(value);
+                return true;
+            }
+
+            const Loop* loop = recurrence->getLoop();
+            // The shape the method covers: one exit, tested in the header, access in the loop.
+            if (!recurrence->isAffine() || loop->getExitingBlock() != loop->getHeader() ||
+                !loop->contains(block))
+                return false;
+            // The endpoints bound the sequence only if no iteration wraps, as a signed value.
+            if (!recurrence->hasNoSignedWrap())
+                return false;
+            const SCEV* count = scev.getBackedgeTakenCount(loop);
+            if (isa<SCEVCouldNotCompute>(count) ||
+                scev.getTypeSizeInBits(count->getType()) >
+                    scev.getTypeSizeInBits(recurrence->getType()))
+                return false;
+
+            // The header runs on iterations 0 .. count, the other blocks on 0 .. count - 1.
+            const SCEV* one = scev.getOne(count->getType());
+            const SCEV* last = block == loop->getHeader()
+                                   ? count
+                                   : scev.getMinusSCEV(scev.getUMaxExpr(count, one), one);
+            const SCEV* lastValue = recurrence->evaluateAtIteration(
+                scev.getNoopOrZeroExtend(last, recurrence->getType()), scev);
+            return endpoints(scev, loops, recurrence->getStart(), block, out) &&
+                   endpoints(scev, loops, lastValue, block, out);
+        }
+
+        /// True when @p block runs on every iteration of every loop around it, with a constant
+        /// iteration count, on every run of the function that returns.
+        bool runsOnEveryIteration(PromotedFunction& promoted, const BasicBlock* block)
+        {
+            const BasicBlock* current = block;
+            for (const Loop* loop = promoted.loops.getLoopFor(block); loop;
+                 loop = loop->getParentLoop())
+            {
+                const auto* count =
+                    dyn_cast<SCEVConstant>(promoted.scev.getBackedgeTakenCount(loop));
+                if (!count || loop->getExitingBlock() != loop->getHeader())
+                    return false;
+                if (current != loop->getHeader())
+                {
+                    const BasicBlock* latch = loop->getLoopLatch();
+                    if (!latch || count->getValue()->isZero() ||
+                        !promoted.dominators.dominates(current, latch))
+                        return false;
+                }
+                current = loop->getHeader();
+            }
+            return promoted.postDominators.dominates(current, &promoted.function.getEntryBlock());
+        }
+
+        /// An input of @p value (an argument, a load, a call result) that is not an integer of
+        /// at least 3 bits, so @ref ClampInputs cannot clamp it.
+        bool hasUnclampableInput(const SCEV* value)
+        {
+            return SCEVExprContains(value,
+                                    [](const SCEV* node)
+                                    {
+                                        const auto* input = dyn_cast<SCEVUnknown>(node);
+                                        return input &&
+                                               (!input->getType()->isIntegerTy() ||
+                                                input->getType()->getIntegerBitWidth() < 3);
+                                    });
+        }
+
+        /// Clamps every input of width N to [0, 2^(N-2)]. A range that changes under it reaches
+        /// as far as an input's type allows, so it states the type, not the program.
+        class ClampInputs final : public SCEVRewriteVisitor<ClampInputs>
+        {
+          public:
+            using SCEVRewriteVisitor::SCEVRewriteVisitor;
+
+            const SCEV* visitUnknown(const SCEVUnknown* input)
+            {
+                const unsigned width = input->getType()->getIntegerBitWidth();
+                const SCEV* cap = SE.getConstant(APInt::getOneBitSet(width, width - 2));
+                return SE.getSMaxExpr(SE.getSMinExpr(input, cap), SE.getZero(input->getType()));
+            }
+        };
+
+        /// The signed range of @p value, or nullopt when it rests on the type of an input.
+        std::optional<ConstantRange> programRange(ScalarEvolution& scev, const SCEV* value)
+        {
+            if (hasUnclampableInput(value))
+                return std::nullopt;
+            const ConstantRange range = scev.getSignedRange(value);
+            ClampInputs clamp(scev);
+            if (scev.getSignedRange(clamp.visit(value)) != range)
+                return std::nullopt;
+            return range;
+        }
+
+        const Loop* outermost(const Loop* loop)
+        {
+            while (loop && loop->getParentLoop())
+                loop = loop->getParentLoop();
+            return loop;
+        }
+    } // namespace
+
+    struct PromotedValues::Impl final
+    {
+        // The copy starts with declarations only: a function body is copied on its first
+        // query and dropped at the next function's, so the copy costs one function at a time.
+        Impl(const Module& module, const std::function<bool(const Function&)>& shouldCopy)
+            : libraryInfo(Triple(module.getTargetTriple())),
+              copy(CloneModule(module, valueMap, [](const GlobalValue*) { return false; })),
+              shouldCopy(shouldCopy)
+        {
+        }
+
+        ~Impl()
+        {
+            release();
+        }
+
+        Impl(const Impl&) = delete;
+        Impl& operator=(const Impl&) = delete;
+
+        /// The copy of @p value, or null when it has none. Plain data constants (integers,
+        /// null) are shared by both modules; a function or a global is a constant too, but
+        /// has its own copy.
+        const Value* copyOf(const Value* value) const
+        {
+            if (isa<ConstantData>(value))
+                return value;
+            const auto found = valueMap.find(value);
+            return found == valueMap.end() ? nullptr : static_cast<const Value*>(found->second);
+        }
+
+        /// The promoted copy of @p original with its analyses, or null when it is left out.
+        // ponytail: one function at a time, fine while queries come function by function;
+        // keep several copies if a consumer interleaves them.
+        PromotedFunction* promoted(const Function& original)
+        {
+            if (current == &original)
+                return function.get();
+            release();
+            current = &original;
+            if (original.isDeclaration() || !shouldCopy(original) || hasLifetimeMarkers(original))
+                return nullptr;
+
+            auto* copied = const_cast<Function*>(dyn_cast_or_null<Function>(copyOf(&original)));
+            if (!copied)
+                return nullptr;
+            auto copiedArgument = copied->arg_begin();
+            for (const Argument& argument : original.args())
+                valueMap[&argument] = &*copiedArgument++;
+            SmallVector<ReturnInst*, 8> returns;
+            CloneFunctionInto(copied, &original, valueMap, CloneFunctionChangeType::ClonedModule,
+                              returns);
+            body = copied;
+
+            sanitize(*copied);
+            promote(*copied);
+            function = std::make_unique<PromotedFunction>(*copied, libraryInfo);
+            return function.get();
+        }
+
+        /// Drops the analyses and the copied body of the current function.
+        void release()
+        {
+            function.reset();
+            if (!body)
+                return;
+            body->deleteBody();
+            body = nullptr;
+            for (const Argument& argument : current->args())
+                valueMap.erase(&argument);
+            for (const BasicBlock& block : *current)
+            {
+                valueMap.erase(&block);
+                for (const Instruction& instruction : block)
+                    valueMap.erase(&instruction);
+            }
+        }
+
+        TargetLibraryInfoImpl libraryInfo;
+        ValueToValueMapTy valueMap;
+        std::unique_ptr<Module> copy;
+        std::function<bool(const Function&)> shouldCopy;
+        const Function* current = nullptr;
+        Function* body = nullptr; // the copy of `current` while it has a body
+        std::unique_ptr<PromotedFunction> function;
+    };
+
+    PromotedValues::PromotedValues(const llvm::Module& module,
+                                   const std::function<bool(const llvm::Function&)>& shouldCopy)
+        : impl_(std::make_unique<Impl>(module, shouldCopy))
+    {
+    }
+
+    PromotedValues::~PromotedValues() = default;
+
+    IndexValues PromotedValues::indexValuesAt(const llvm::Instruction& access,
+                                              const llvm::Value& index)
+    {
+        IndexValues out;
+        PromotedFunction* promoted = impl_->promoted(*access.getFunction());
+        const auto* at = dyn_cast_or_null<Instruction>(impl_->copyOf(&access));
+        const Value* value = impl_->copyOf(&index);
+        if (!promoted || !at || !value || !value->getType()->isIntegerTy() ||
+            value->getType()->getIntegerBitWidth() > 64)
+            return out;
+
+        ScalarEvolution& scev = promoted->scev;
+        const BasicBlock* block = at->getParent();
+        if (neverRuns(scev, promoted->loops, block))
+        {
+            out.kind = IndexValues::Kind::NeverRuns;
+            return out;
+        }
+
+        // Outside a loop, the value is the one the loop exits with.
+        const Loop* loop = promoted->loops.getLoopFor(block);
+        const SCEV* indexValue = scev.getSCEVAtScope(scev.getSCEV(const_cast<Value*>(value)), loop);
+        SmallVector<const SCEV*, 8> ends;
+        if (!endpoints(scev, promoted->loops, indexValue, block, ends))
+            return out;
+
+        const Loop* outer = outermost(loop);
+        const bool everyRun = runsOnEveryIteration(*promoted, block);
+        ConstantRange range = ConstantRange::getEmpty(64);
+        SmallVector<std::int64_t, 8> taken;
+        for (const SCEV* end : ends)
+        {
+            if (const auto* constant = dyn_cast<SCEVConstant>(end); constant && everyRun)
+                taken.push_back(constant->getAPInt().getSExtValue());
+            const std::optional<ConstantRange> endRange =
+                programRange(scev, outer ? scev.applyLoopGuards(end, outer) : end);
+            if (!endRange)
+                return out;
+            range = range.unionWith(endRange->sextOrTrunc(64), ConstantRange::Signed);
+        }
+        if (range.isEmptySet() || range.isFullSet())
+            return out;
+
+        out.kind = IndexValues::Kind::Range;
+        out.min = range.getSignedMin().getSExtValue();
+        out.max = range.getSignedMax().getSExtValue();
+        out.minOnEveryRun = is_contained(taken, out.min);
+        out.maxOnEveryRun = is_contained(taken, out.max);
+        return out;
+    }
+
+    bool PromotedValues::provesWithin(const llvm::Instruction& access, const llvm::Value& index,
+                                      std::int64_t lower, std::int64_t upper)
+    {
+        PromotedFunction* promoted = impl_->promoted(*access.getFunction());
+        const auto* at = dyn_cast_or_null<Instruction>(impl_->copyOf(&access));
+        const Value* value = impl_->copyOf(&index);
+        if (!promoted || !at || !value || !value->getType()->isIntegerTy())
+            return false;
+
+        // Both bounds must be values of the index type, or the comparison would read others.
+        const unsigned width = value->getType()->getIntegerBitWidth();
+        if (width > 64 || (width < 64 && (lower < APInt::getSignedMinValue(width).getSExtValue() ||
+                                          upper > APInt::getSignedMaxValue(width).getSExtValue())))
+            return false;
+
+        ScalarEvolution& scev = promoted->scev;
+        const SCEV* indexValue = scev.getSCEVAtScope(scev.getSCEV(const_cast<Value*>(value)),
+                                                     promoted->loops.getLoopFor(at->getParent()));
+        Type* type = value->getType();
+        return scev.isKnownPredicateAt(ICmpInst::ICMP_SGE, indexValue,
+                                       scev.getConstant(type, lower, /*isSigned=*/true), at) &&
+               scev.isKnownPredicateAt(ICmpInst::ICMP_SLT, indexValue,
+                                       scev.getConstant(type, upper, /*isSigned=*/true), at);
+    }
+} // namespace ctrace::stack::analysis
diff --git a/src/analysis/StackBufferAnalysis.cpp b/src/analysis/StackBufferAnalysis.cpp
index b07b96c8..56027b87 100644
--- a/src/analysis/StackBufferAnalysis.cpp
+++ b/src/analysis/StackBufferAnalysis.cpp
@@ -25,6 +25,7 @@
 #include "analysis/IntRanges.hpp"
 #include "analysis/FunctionFacts.hpp"
 #include "analysis/IRValueUtils.hpp"
+#include "analysis/PromotedValues.hpp"
 #include "analysis/smt/SmtEncoding.hpp"
 #include "analysis/smt/SmtRefinement.hpp"
 
@@ -879,11 +880,27 @@ namespace ctrace::stack::analysis
                                                      &facts) == SmtFeasibility::Infeasible;
         }
 
-        static void
-        analyzeStackBufferOverflowsInFunction(llvm::Function& F,
-                                              std::vector<StackBufferOverflowIssue>& out,
-                                              const AnalysisComplexityBudgets& budgets,
-                                              const StackBufferConstraintEvaluator& evaluator)
+        /// The index-bounds pilot covers `buf[i]` on a stack array alone: a GEP straight on the
+        /// array's alloca, with indices [0, i]. Aliases, struct fields and globals keep the
+        /// existing heuristics.
+        static bool isIndexBoundsPilotAccess(const llvm::GetElementPtrInst& gep,
+                                             const llvm::AllocaInst* array)
+        {
+            using namespace llvm;
+            if (!array || array->isArrayAllocation() || gep.getPointerOperand() != array ||
+                gep.getNumIndices() != 2 ||
+                gep.getSourceElementType() != array->getAllocatedType() ||
+                !isa<ArrayType>(gep.getSourceElementType()))
+                return false;
+            const auto* first = dyn_cast<ConstantInt>(gep.idx_begin()->get());
+            return first && first->isZero();
+        }
+
+        static void analyzeStackBufferOverflowsInFunction(
+            llvm::Function& F, std::vector<StackBufferOverflowIssue>& out,
+            const AnalysisComplexityBudgets& budgets,
+            const StackBufferConstraintEvaluator& evaluator,
+            const std::function<PromotedValues&()>& promotedValues)
         {
             using namespace llvm;
 
@@ -1057,6 +1074,35 @@ namespace ctrace::stack::analysis
                             GV->hasName() ? GV->getName().str() : std::string("<unnamed-global>");
                     }
 
+                    // The loads and stores through the GEP, each reported on its own. A store of
+                    // the address itself (char* p = &buf[i]) accesses nothing.
+                    SmallVector<Instruction*, 4> accesses;
+                    for (User* GU : GEP->users())
+                    {
+                        const auto* store = dyn_cast<StoreInst>(GU);
+                        if (isa<LoadInst>(GU) || (store && store->getPointerOperand() == GEP))
+                            accesses.push_back(cast<Instruction>(GU));
+                    }
+                    const bool pilotAccess = isIndexBoundsPilotAccess(*GEP, AI);
+                    const auto newReport = [&](Instruction& access)
+                    {
+                        StackBufferOverflowIssue report;
+                        report.funcName = F.getName().str();
+                        report.varName = varName;
+                        report.arraySize = arraySize;
+                        report.isWrite = isa<StoreInst>(access);
+                        report.storageClass = storageClass;
+                        report.inst = &access;
+                        // The index-bounds pilot may show that the access never runs: its
+                        // reports then carry the unreachable-code note.
+                        report.neverRuns =
+                            pilotAccess && promotedValues().indexValuesAt(access, *idxVal).kind ==
+                                               IndexValues::Kind::NeverRuns;
+                        report.aliasPathVec = aliasPath;
+                        report.aliasPath = buildAliasPathString(aliasPath);
+                        return report;
+                    };
+
                     // "baseIdxVal" = loop variable "i" without casts (sext/zext...). The cast
                     // applied to the variable itself says how the index reads it: a zext reads
                     // it as unsigned.
@@ -1075,44 +1121,71 @@ namespace ctrace::stack::analysis
                         auto idxValue = CIdx->getSExtValue();
                         if (idxValue < 0 || static_cast<StackSize>(idxValue) >= arraySize)
                         {
-                            for (User* GU : GEP->users())
+                            for (Instruction* access : accesses)
                             {
-                                if (auto* S = dyn_cast<StoreInst>(GU))
-                                {
-                                    StackBufferOverflowIssue report;
-                                    report.funcName = F.getName().str();
-                                    report.varName = varName;
-                                    report.arraySize = arraySize;
-                                    report.indexOrUpperBound = static_cast<StackSize>(idxValue);
-                                    report.isWrite = true;
-                                    report.indexIsConstant = true;
-                                    report.storageClass = storageClass;
-                                    report.inst = S;
-                                    report.aliasPathVec = aliasPath;
-                                    report.aliasPath = buildAliasPathString(aliasPath);
-                                    out.push_back(std::move(report));
-                                }
-                                else if (auto* L = dyn_cast<LoadInst>(GU))
-                                {
-                                    StackBufferOverflowIssue report;
-                                    report.funcName = F.getName().str();
-                                    report.varName = varName;
-                                    report.arraySize = arraySize;
-                                    report.indexOrUpperBound = static_cast<StackSize>(idxValue);
-                                    report.isWrite = false;
-                                    report.indexIsConstant = true;
-                                    report.storageClass = storageClass;
-                                    report.inst = L;
-                                    report.aliasPathVec = aliasPath;
-                                    report.aliasPath = buildAliasPathString(aliasPath);
-                                    out.push_back(std::move(report));
-                                }
+                                StackBufferOverflowIssue report = newReport(*access);
+                                report.indexOrUpperBound = static_cast<StackSize>(idxValue);
+                                report.indexIsConstant = true;
+                                out.push_back(std::move(report));
                             }
                         }
                         continue;
                     }
 
-                    // 5) Variable index case: test[i] / ptr[i]
+                    // 5) Variable index case. At each access it covers, the index-bounds pilot
+                    // decides whenever it establishes the index values there, under the
+                    // conditions the access runs on: a proof that the index stays in bounds, or
+                    // the range it takes. The heuristics below decide the other accesses.
+                    const bool pilotDecides =
+                        pilotAccess && arraySize <= static_cast<StackSize>(
+                                                        std::numeric_limits<std::int64_t>::max());
+                    SmallVector<Instruction*, 4> undecided;
+                    for (Instruction* access : accesses)
+                    {
+                        IndexValues values;
+                        if (pilotDecides)
+                        {
+                            PromotedValues& promoted = promotedValues();
+                            values = promoted.indexValuesAt(*access, *idxVal);
+                            if (values.kind != IndexValues::Kind::NeverRuns &&
+                                promoted.provesWithin(*access, *idxVal, 0,
+                                                      static_cast<std::int64_t>(arraySize)))
+                                continue;
+                        }
+                        if (values.kind != IndexValues::Kind::Range)
+                        {
+                            undecided.push_back(access);
+                            continue;
+                        }
+
+                        // A potential report yields to a solver proof, as the heuristics'
+                        // reports do; one the index reaches on every run does not.
+                        const auto solverProvesInBounds = [&]
+                        {
+                            return isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *access,
+                                                        facts);
+                        };
+                        if (values.max >= 0 && static_cast<StackSize>(values.max) >= arraySize &&
+                            (values.maxOnEveryRun || !solverProvesInBounds()))
+                        {
+                            StackBufferOverflowIssue report = newReport(*access);
+                            report.indexOrUpperBound = static_cast<StackSize>(values.max);
+                            report.reachedOnEveryRun = values.maxOnEveryRun;
+                            out.push_back(std::move(report));
+                        }
+                        if (values.min < 0 && (values.minOnEveryRun || !solverProvesInBounds()))
+                        {
+                            StackBufferOverflowIssue report = newReport(*access);
+                            report.isLowerBoundViolation = true;
+                            report.lowerBound = values.min;
+                            report.reachedOnEveryRun = values.minOnEveryRun;
+                            out.push_back(std::move(report));
+                        }
+                    }
+                    if (undecided.empty())
+                        continue;
+
+                    // Heuristics: test[i] / ptr[i]
                     // An index computed as x + C or x - C has the bounds of x shifted by C: look
                     // for those of x, and shift them once found.
                     const auto* offsetOp = dyn_cast<BinaryOperator>(baseIdxVal);
@@ -1194,98 +1267,27 @@ namespace ctrace::stack::analysis
                         else
                             ub = static_cast<StackSize>(R.lower);
 
-                        for (User* GU : GEP->users())
+                        for (Instruction* access : undecided)
                         {
-                            if (auto* S = dyn_cast<StoreInst>(GU))
-                            {
-                                if (isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *S, facts))
-                                {
-                                    continue;
-                                }
-
-                                StackBufferOverflowIssue report;
-                                report.funcName = F.getName().str();
-                                report.varName = varName;
-                                report.arraySize = arraySize;
-                                report.indexOrUpperBound = ub;
-                                report.isWrite = true;
-                                report.indexIsConstant = false;
-                                report.storageClass = storageClass;
-                                report.inst = S;
-                                report.aliasPathVec = aliasPath;
-                                report.aliasPath = buildAliasPathString(aliasPath);
-                                out.push_back(std::move(report));
-                            }
-                            else if (auto* L = dyn_cast<LoadInst>(GU))
-                            {
-                                if (isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *L, facts))
-                                {
-                                    continue;
-                                }
-
-                                StackBufferOverflowIssue report;
-                                report.funcName = F.getName().str();
-                                report.varName = varName;
-                                report.arraySize = arraySize;
-                                report.indexOrUpperBound = ub;
-                                report.isWrite = false;
-                                report.indexIsConstant = false;
-                                report.storageClass = storageClass;
-                                report.inst = L;
-                                report.aliasPathVec = aliasPath;
-                                report.aliasPath = buildAliasPathString(aliasPath);
-                                out.push_back(std::move(report));
-                            }
+                            if (isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *access, facts))
+                                continue;
+                            StackBufferOverflowIssue report = newReport(*access);
+                            report.indexOrUpperBound = ub;
+                            out.push_back(std::move(report));
                         }
                     }
 
                     // 5.b) Negative lower bound: LB < 0  => potentially negative index
                     if (R.hasLower && R.lower < 0)
                     {
-                        for (User* GU : GEP->users())
+                        for (Instruction* access : undecided)
                         {
-                            if (auto* S = dyn_cast<StoreInst>(GU))
-                            {
-                                if (isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *S, facts))
-                                {
-                                    continue;
-                                }
-
-                                StackBufferOverflowIssue report;
-                                report.funcName = F.getName().str();
-                                report.varName = varName;
-                                report.arraySize = arraySize;
-                                report.isWrite = true;
-                                report.indexIsConstant = false;
-                                report.storageClass = storageClass;
-                                report.inst = S;
-                                report.isLowerBoundViolation = true;
-                                report.lowerBound = R.lower;
-                                report.aliasPathVec = aliasPath;
-                                report.aliasPath = buildAliasPathString(aliasPath);
-                                out.push_back(std::move(report));
-                            }
-                            else if (auto* L = dyn_cast<LoadInst>(GU))
-                            {
-                                if (isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *L, facts))
-                                {
-                                    continue;
-                                }
-
-                                StackBufferOverflowIssue report;
-                                report.funcName = F.getName().str();
-                                report.varName = varName;
-                                report.arraySize = arraySize;
-                                report.isWrite = false;
-                                report.indexIsConstant = false;
-                                report.storageClass = storageClass;
-                                report.inst = L;
-                                report.isLowerBoundViolation = true;
-                                report.lowerBound = R.lower;
-                                report.aliasPathVec = aliasPath;
-                                report.aliasPath = buildAliasPathString(aliasPath);
-                                out.push_back(std::move(report));
-                            }
+                            if (isIndexInBoundsBySmt(evaluator, idxVal, arraySize, *access, facts))
+                                continue;
+                            StackBufferOverflowIssue report = newReport(*access);
+                            report.isLowerBoundViolation = true;
+                            report.lowerBound = R.lower;
+                            out.push_back(std::move(report));
                         }
                     }
                     // If R.hasUpper && R.upper < arraySize and (no problematic LB),
@@ -1423,6 +1425,14 @@ namespace ctrace::stack::analysis
         std::vector<StackBufferOverflowIssue> out;
         const AnalysisComplexityBudgets budgets = buildAnalysisComplexityBudgets(config);
         const StackBufferConstraintEvaluator evaluator(config);
+        // The promoted copy of the module, built on the first access the pilot asks about.
+        std::optional<PromotedValues> promoted;
+        const std::function<PromotedValues&()> promotedValues = [&]() -> PromotedValues&
+        {
+            if (!promoted)
+                promoted.emplace(mod, shouldAnalyze);
+            return *promoted;
+        };
 
         for (llvm::Function& F : mod)
         {
@@ -1430,7 +1440,7 @@ namespace ctrace::stack::analysis
                 continue;
             if (!shouldAnalyze(F))
                 continue;
-            analyzeStackBufferOverflowsInFunction(F, out, budgets, evaluator);
+            analyzeStackBufferOverflowsInFunction(F, out, budgets, evaluator, promotedValues);
         }
 
         return out;
diff --git a/src/analyzer/DiagnosticEmitter.cpp b/src/analyzer/DiagnosticEmitter.cpp
index 8e37f32c..7755d831 100644
--- a/src/analyzer/DiagnosticEmitter.cpp
+++ b/src/analyzer/DiagnosticEmitter.cpp
@@ -370,7 +370,11 @@ namespace ctrace::stack::analyzer
         for (const auto& issue : bufferIssues)
         {
             const ResolvedLocation loc = resolveFromInstruction(issue.inst, true);
-            const bool isUnreachable = analysis::isStaticallyUnreachableStackAccess(issue);
+            const bool isUnreachable =
+                issue.neverRuns || analysis::isStaticallyUnreachableStackAccess(issue);
+            // Shown by the index-bounds pilot: the access goes out of bounds on every run that
+            // returns, so the report is not "potential".
+            const bool everyRun = issue.reachedOnEveryRun;
 
             std::ostringstream body;
             DiagnosticBuilder builder;
@@ -379,23 +383,32 @@ namespace ctrace::stack::analyzer
             {
                 builder.errCode(DescriptiveErrorCode::NegativeStackIndex)
                     .cwe(issue.isWrite ? "CWE-124" : "CWE-127");
-                body << "  [!!] potential negative index on variable '" << issue.varName
-                     << "' (size " << issue.arraySize << ")\n";
+                if (everyRun)
+                    builder.ruleId("NegativeStackIndex.EveryRun");
+                body << "  [!!] " << (everyRun ? "" : "potential ")
+                     << "negative index on variable '" << issue.varName << "' (size "
+                     << issue.arraySize << ")\n";
                 if (!issue.aliasPath.empty())
                     body << "\t\t ↳ alias path: " << issue.aliasPath << "\n";
-                body << "\t\t ↳ inferred lower bound for index expression: " << issue.lowerBound
-                     << " (index may be < 0)\n";
+                if (everyRun)
+                    body << "\t\t ↳ index reaches " << issue.lowerBound
+                         << " on every run of the function that returns\n";
+                else
+                    body << "\t\t ↳ inferred lower bound for index expression: " << issue.lowerBound
+                         << " (index may be < 0)\n";
             }
             else
             {
                 builder.errCode(DescriptiveErrorCode::StackBufferOverflow);
+                if (everyRun)
+                    builder.ruleId("StackBufferOverflow.EveryRun");
                 const bool isGlobalStorage =
                     issue.storageClass == analysis::BufferStorageClass::Global;
                 if (!issue.isWrite)
                     builder.cwe("CWE-125");
                 else
                     builder.cwe(isGlobalStorage ? "CWE-787" : "CWE-121");
-                body << "\t[ !!Warn ] potential "
+                body << "\t[ !!Warn ] " << (everyRun ? "" : "potential ")
                      << (isGlobalStorage ? "buffer overflow on global variable '"
                                          : "stack buffer overflow on variable '")
                      << issue.varName << "' (size " << issue.arraySize << ")\n";
@@ -407,6 +420,12 @@ namespace ctrace::stack::analyzer
                          << " is out of bounds (0.." << (issue.arraySize ? issue.arraySize - 1 : 0)
                          << ")\n";
                 }
+                else if (everyRun)
+                {
+                    body << "\t\t ↳ index reaches " << issue.indexOrUpperBound
+                         << " on every run of the function that returns (array last valid index: "
+                         << (issue.arraySize ? issue.arraySize - 1 : 0) << ")\n";
+                }
                 else
                 {
                     body << "\t\t ↳ index variable may go up to " << issue.indexOrUpperBound
diff --git a/src/report/ReportSerialization.cpp b/src/report/ReportSerialization.cpp
index d78514dc..821f5efd 100644
--- a/src/report/ReportSerialization.cpp
+++ b/src/report/ReportSerialization.cpp
@@ -641,6 +641,10 @@ namespace ctrace::stack
             {"NegativeStackIndex",
              {"Negative stack index", "An index into a stack array that may be negative, so that "
                                       "the access lands before the array."}},
+            {"NegativeStackIndex.EveryRun",
+             {"Negative stack index on every run",
+              "A read or a write before the start of a stack array that every run of the "
+              "function performs, if the run returns."}},
             {"NullPointerDereference",
              {"Null pointer dereference", "A pointer that may be null is dereferenced."}},
             {"OutOfBoundsRead", {"Out-of-bounds read", "A read past the end of a buffer."}},
@@ -691,6 +695,10 @@ namespace ctrace::stack
             {"StackBufferOverflow",
              {"Stack buffer overflow",
               "A read or a write at an index that may be past the end of a stack array."}},
+            {"StackBufferOverflow.EveryRun",
+             {"Stack buffer overflow on every run",
+              "A read or a write past the end of a stack array that every run of the function "
+              "performs, if the run returns."}},
             {"StackFrameTooLarge",
              {"Stack frame too large",
               "A function whose stack frame exceeds the configured limit."}},
diff --git a/test/bound-storage/bound-storage-for-statement.c b/test/bound-storage/bound-storage-for-statement.c
index 9e8dc272..3ddc9835 100644
--- a/test/bound-storage/bound-storage-for-statement.c
+++ b/test/bound-storage/bound-storage-for-statement.c
@@ -31,15 +31,15 @@ int main(void)
 }
 
 // at line 8, column 17
-// [ !!Warn ] potential stack buffer overflow on variable 'test' (size 10)
+// [ !!Warn ] stack buffer overflow on variable 'test' (size 10)
 // ↳ alias path: test
-// ↳ index variable may go up to 19 (array last valid index: 9)
+// ↳ index reaches 19 on every run of the function that returns (array last valid index: 9)
 // ↳ (this is a write access)
 
 // at line 12, column 17
-// [ !!Warn ] potential stack buffer overflow on variable 'test' (size 10)
+// [ !!Warn ] stack buffer overflow on variable 'test' (size 10)
 // ↳ alias path: test
-// ↳ index variable may go up to 10 (array last valid index: 9)
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
 // ↳ (this is a write access)
 
 // at line 22, column 16
diff --git a/test/bound-storage/bound-storage-if-statement.c b/test/bound-storage/bound-storage-if-statement.c
index ec1ff27b..85b436da 100644
--- a/test/bound-storage/bound-storage-if-statement.c
+++ b/test/bound-storage/bound-storage-if-statement.c
@@ -18,7 +18,7 @@ int main(void)
     // at line 25, column 18
     // [ !!Warn ] potential stack buffer overflow on variable 'test1' (size 10)
     // ↳ alias path: test1
-    // ↳ index variable may go up to 10 (array last valid index: 9)
+    // ↳ index variable may go up to 11 (array last valid index: 9)
     // ↳ (this is a write access)
     // ↳ [info] this access appears unreachable at runtime (condition is always false for this branch)
     char test1[10];
diff --git a/test/bound-storage/element-address-is-not-a-write.c b/test/bound-storage/element-address-is-not-a-write.c
new file mode 100644
index 00000000..820511cf
--- /dev/null
+++ b/test/bound-storage/element-address-is-not-a-write.c
@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: Apache-2.0
+// Storing the address of an element in a pointer does not access the array, and C allows the
+// address one past the end. Only the pointers are written here.
+int end_pointer(void)
+{
+    char buf[10] = {0};
+    const char* end = &buf[10];
+    int sum = 0;
+    for (const char* p = buf; p != end; ++p)
+        sum += *p;
+    return sum;
+}
+
+void address_in_loop(void)
+{
+    char buf[10];
+    for (int i = 0; i <= 10; ++i)
+    {
+        char* p = &buf[i];
+        if (i < 10)
+            *p = 42;
+    }
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
+// not contains: negative index
diff --git a/test/bound-storage/indirection-profonde-aliasing.c b/test/bound-storage/indirection-profonde-aliasing.c
index e7e546ae..dfaf28f3 100644
--- a/test/bound-storage/indirection-profonde-aliasing.c
+++ b/test/bound-storage/indirection-profonde-aliasing.c
@@ -20,9 +20,9 @@ int main(void)
     (*pp)[15] = 'a';
 
     // at line 28, column 17
-    // [ !!Warn ] potential stack buffer overflow on variable 'test' (size 10)
+    // [ !!Warn ] stack buffer overflow on variable 'test' (size 10)
     // ↳ alias path: test
-    // ↳ index variable may go up to 19 (array last valid index: 9)
+    // ↳ index reaches 19 on every run of the function that returns (array last valid index: 9)
     // ↳ (this is a write access)
     for (int i = 0; i < 20; i++)
     {
@@ -30,9 +30,9 @@ int main(void)
     }
 
     // at line 37, column 17
-    // [ !!Warn ] potential stack buffer overflow on variable 'test' (size 10)
+    // [ !!Warn ] stack buffer overflow on variable 'test' (size 10)
     // ↳ alias path: test
-    // ↳ index variable may go up to 10 (array last valid index: 9)
+    // ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
     // ↳ (this is a write access)
     for (int i = 0; i != 11; ++i)
         test[i] = 'a';
diff --git a/test/bound-storage/loop-index-bounds/address-and-access-bad.c b/test/bound-storage/loop-index-bounds/address-and-access-bad.c
new file mode 100644
index 00000000..4a7f92e3
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/address-and-access-bad.c
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: Apache-2.0
+// Forming &buf[10] is allowed, writing buf[10] is not: only the write is reported.
+void address_and_access_bad(void)
+{
+    char buf[10];
+    char* last = buf;
+    for (int i = 0; i <= 10; ++i)
+    {
+        last = &buf[i];
+        buf[i] = 'a';
+    }
+    (void)last;
+}
+
+// strict-expectation-details: true
+
+// at line 10, column 16
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/after-loop-bad.c b/test/bound-storage/loop-index-bounds/after-loop-bad.c
new file mode 100644
index 00000000..834fa8b0
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/after-loop-bad.c
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: Apache-2.0
+// The access after the loop runs with i == 10, the value the loop exits with.
+void after_loop_bad(void)
+{
+    char buf[10];
+    int i;
+    for (i = 0; i < 10; i++)
+    {
+    }
+    buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 10, column 12
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/below-zero-bad.c b/test/bound-storage/loop-index-bounds/below-zero-bad.c
new file mode 100644
index 00000000..6011b6e4
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/below-zero-bad.c
@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: Apache-2.0
+// A loop counting down to -1: its last iteration writes buf[-1] on every run.
+void below_zero_bad(void)
+{
+    char buf[10];
+    for (int i = 9; i >= -1; i--)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 7, column 16
+// [!!] negative index on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches -1 on every run of the function that returns
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/break-first-bad.c b/test/bound-storage/loop-index-bounds/break-first-bad.c
new file mode 100644
index 00000000..c59e32f0
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/break-first-bad.c
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: Apache-2.0
+// A constant index past the end, reached on the first iteration before a
+// break. The existing report stays: the loop has two exits.
+void break_first_bad(void)
+{
+    char buf[10];
+    for (int i = 0; i < 10; ++i)
+        if (i == 0)
+        {
+            buf[10] = 'a';
+            break;
+        }
+}
+
+// strict-expectation-details: true
+
+// at line 10, column 21
+// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ constant index 10 is out of bounds (0..9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/conditional-access-bad.c b/test/bound-storage/loop-index-bounds/conditional-access-bad.c
new file mode 100644
index 00000000..b3622589
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/conditional-access-bad.c
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: Apache-2.0
+// i reaches 10 in the loop and the access may run with it, but not on every
+// iteration: the report is potential.
+void conditional_access_bad(void)
+{
+    char buf[10];
+    for (int i = 0; i <= 10; i++)
+        if (i % 2 == 0)
+            buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: on every run
+
+// at line 9, column 20
+// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index variable may go up to 10 (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/conditional-ok.c b/test/bound-storage/loop-index-bounds/conditional-ok.c
new file mode 100644
index 00000000..80bf9c85
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/conditional-ok.c
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: Apache-2.0
+// i reaches 10 in the loop, but i != 10 guards the access.
+void conditional_ok(void)
+{
+    char buf[10];
+    for (int i = 0; i < 11; ++i)
+        if (i != 10)
+            buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/derived-bad.c b/test/bound-storage/loop-index-bounds/derived-bad.c
new file mode 100644
index 00000000..f20103bc
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/derived-bad.c
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: Apache-2.0
+// An index derived from the counter: k = i + 1 reaches 10 on every run.
+void derived_bad(void)
+{
+    char buf[10];
+    for (int i = 0; i < 10; i++)
+    {
+        int k = i + 1;
+        buf[k] = 'a';
+    }
+}
+
+// strict-expectation-details: true
+
+// at line 9, column 16
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/derived-ok.c b/test/bound-storage/loop-index-bounds/derived-ok.c
new file mode 100644
index 00000000..10e9d5da
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/derived-ok.c
@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: Apache-2.0
+// An index derived from the counter: k = i + 1 stays in 1..9.
+void derived_ok(void)
+{
+    char buf[10];
+    for (int i = 0; i < 9; i++)
+    {
+        int k = i + 1;
+        buf[k] = 'a';
+    }
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/down-bad.c b/test/bound-storage/loop-index-bounds/down-bad.c
new file mode 100644
index 00000000..dfa48760
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/down-bad.c
@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: Apache-2.0
+// A loop counting down from 10: its first iteration writes buf[10] on every run.
+void down_bad(void)
+{
+    char buf[10];
+    for (int i = 10; i >= 0; i--)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 7, column 16
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/down-ok.c b/test/bound-storage/loop-index-bounds/down-ok.c
new file mode 100644
index 00000000..98a8732b
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/down-ok.c
@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: Apache-2.0
+// A loop counting down from 9 to 0.
+void down_ok(void)
+{
+    char buf[10];
+    for (int i = 9; i >= 0; i--)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/guarded-ok.c b/test/bound-storage/loop-index-bounds/guarded-ok.c
new file mode 100644
index 00000000..672235fd
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/guarded-ok.c
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: Apache-2.0
+// i + 1 reaches 10 in the loop, but the guard keeps the access below it.
+void guarded_ok(void)
+{
+    char buf[10];
+    for (int i = 0; i < 10; i++)
+        if (i + 1 < 10)
+            buf[i + 1] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/header-access-bad.c b/test/bound-storage/loop-index-bounds/header-access-bad.c
new file mode 100644
index 00000000..3954ff9b
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/header-access-bad.c
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: Apache-2.0
+// An access in the loop test runs once more than the body, with i == 10.
+void header_access_bad(void)
+{
+    char buf[10];
+    int i;
+    for (i = 0; (buf[i] = 'a', i < 10); i++)
+    {
+    }
+}
+
+// strict-expectation-details: true
+
+// at line 7, column 25
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/index-from-previous-loop.c b/test/bound-storage/loop-index-bounds/index-from-previous-loop.c
new file mode 100644
index 00000000..fcd2222c
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/index-from-previous-loop.c
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: Apache-2.0
+// k leaves the first loop with a value only its type bounds. The second loop starts from it,
+// so the pilot adds nothing there.
+void index_from_previous_loop(const int* more)
+{
+    char buf[4];
+    int k = 0;
+    while (*more++)
+        k++;
+    while (k < 4)
+        buf[k++] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
+// not contains: negative index
diff --git a/test/bound-storage/loop-index-bounds/maybe-uninitialized-index.c b/test/bound-storage/loop-index-bounds/maybe-uninitialized-index.c
new file mode 100644
index 00000000..9b84f587
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/maybe-uninitialized-index.c
@@ -0,0 +1,25 @@
+// SPDX-License-Identifier: Apache-2.0
+// i is uninitialized when c is 0. The copy starts every slot from an opaque value, so
+// the pilot does not take i for 12 on every run: the existing report stays.
+void maybe_uninitialized_index(int c)
+{
+    char buf[10];
+    int i;
+    if (c)
+        i = 12;
+    buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: on every run
+
+// at line 10, column 12
+// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index variable may go up to 12 (array last valid index: 9)
+// ↳ (this is a write access)
+
+// at line 10, column 9
+// [ !!Warn ] potential read of uninitialized local variable 'i'
+// ↳ this load may execute before any definite initialization on all control-flow paths
diff --git a/test/bound-storage/loop-index-bounds/nested-bad.c b/test/bound-storage/loop-index-bounds/nested-bad.c
new file mode 100644
index 00000000..b0679c83
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/nested-bad.c
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: Apache-2.0
+// Nested loops: i * 4 + j reaches 15 in a 15-byte array on every run.
+void nested_bad(void)
+{
+    char buf[15];
+    for (int i = 0; i < 4; i++)
+        for (int j = 0; j < 4; j++)
+            buf[i * 4 + j] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 8, column 28
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 15)
+// ↳ alias path: buf
+// ↳ index reaches 15 on every run of the function that returns (array last valid index: 14)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/nested-ok.c b/test/bound-storage/loop-index-bounds/nested-ok.c
new file mode 100644
index 00000000..fe59a865
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/nested-ok.c
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: Apache-2.0
+// Nested loops: i * 4 + j covers 0..15 of a 16-byte array.
+void nested_ok(void)
+{
+    char buf[16];
+    for (int i = 0; i < 4; i++)
+        for (int j = 0; j < 4; j++)
+            buf[i * 4 + j] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/param-bad.c b/test/bound-storage/loop-index-bounds/param-bad.c
new file mode 100644
index 00000000..999b9659
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/param-bad.c
@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: Apache-2.0
+// A trip count bounded by an early return: n <= 11, so i may reach 10. Only a
+// caller passing 11 overflows: the report is potential.
+void param_bad(int n)
+{
+    char buf[10];
+    if (n > 11)
+        return;
+    for (int i = 0; i < n; i++)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: on every run
+
+// at line 10, column 16
+// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index variable may go up to 10 (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/param-ok.c b/test/bound-storage/loop-index-bounds/param-ok.c
new file mode 100644
index 00000000..eb7dc789
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/param-ok.c
@@ -0,0 +1,14 @@
+// SPDX-License-Identifier: Apache-2.0
+// A trip count bounded by an early return: n <= 10, so i stays in 0..9.
+void param_ok(int n)
+{
+    char buf[10];
+    if (n > 10)
+        return;
+    for (int i = 0; i < n; i++)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/step2-bad.c b/test/bound-storage/loop-index-bounds/step2-bad.c
new file mode 100644
index 00000000..98fc8a7a
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/step2-bad.c
@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: Apache-2.0
+// Steps of 2 below 11: i + 1 reaches 11 on every run.
+void step2_bad(void)
+{
+    char buf[10];
+    for (int i = 0; i < 11; i += 2)
+        buf[i + 1] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 7, column 20
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 11 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/step2-ok.c b/test/bound-storage/loop-index-bounds/step2-ok.c
new file mode 100644
index 00000000..dd07cb8d
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/step2-ok.c
@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: Apache-2.0
+// Steps of 2 below 10: i + 1 stays in 1..9.
+void step2_ok(void)
+{
+    char buf[10];
+    for (int i = 0; i < 10; i += 2)
+        buf[i + 1] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/stride-bad.c b/test/bound-storage/loop-index-bounds/stride-bad.c
new file mode 100644
index 00000000..cf4b1eda
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/stride-bad.c
@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: Apache-2.0
+// A stride of 2: 2 * i + 2 reaches 10 on every run.
+void stride_bad(void)
+{
+    char buf[10];
+    for (int i = 0; i < 5; i++)
+        buf[2 * i + 2] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 7, column 24
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/stride-ok.c b/test/bound-storage/loop-index-bounds/stride-ok.c
new file mode 100644
index 00000000..8c20c887
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/stride-ok.c
@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: Apache-2.0
+// A stride of 2: 2 * i + 1 stays in 1..9.
+void stride_ok(void)
+{
+    char buf[10];
+    for (int i = 0; i < 5; i++)
+        buf[2 * i + 1] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/two-ivs-bad.c b/test/bound-storage/loop-index-bounds/two-ivs-bad.c
new file mode 100644
index 00000000..853e6436
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/two-ivs-bad.c
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: Apache-2.0
+// Two counters: j follows i over 0..10, and reaches 10 on every run.
+void two_ivs_bad(void)
+{
+    char buf[10];
+    int j = 0;
+    for (int i = 0; i <= 10; i++)
+        buf[j++] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 8, column 18
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
+// ↳ (this is a write access)
diff --git a/test/bound-storage/loop-index-bounds/two-ivs-ok.c b/test/bound-storage/loop-index-bounds/two-ivs-ok.c
new file mode 100644
index 00000000..23b8ea3e
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/two-ivs-ok.c
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: Apache-2.0
+// Two counters: j follows i over 0..9.
+void two_ivs_ok(void)
+{
+    char buf[10];
+    int j = 0;
+    for (int i = 0; i < 10; i++)
+        buf[j++] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/unbounded-trip-count.c b/test/bound-storage/loop-index-bounds/unbounded-trip-count.c
new file mode 100644
index 00000000..9796bafa
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/unbounded-trip-count.c
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: Apache-2.0
+// Nothing bounds n but its type: a range built on it would state the type, so the
+// pilot adds no report.
+void unbounded_trip_count(int n)
+{
+    char buf[10];
+    for (int i = 0; i < n; i++)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: stack buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/wrap-unknown.c b/test/bound-storage/loop-index-bounds/wrap-unknown.c
new file mode 100644
index 00000000..7b9e0104
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/wrap-unknown.c
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: Apache-2.0
+// j wraps at its second step. ScalarEvolution proves no no-wrap for it, so the
+// pilot leaves the index unknown and adds nothing (a known miss: buf[2^63]).
+void wrap_bad(void)
+{
+    char buf[10];
+    unsigned long long j = 0;
+    for (int i = 0; i < 3; ++i)
+    {
+        buf[j] = 'a';
+        j += 9223372036854775808ULL;
+    }
+}
+
+// strict-expectation-details: true
+
+// not contains: stack buffer overflow
diff --git a/test/bound-storage/loop-index-bounds/zero-constant-ok.c b/test/bound-storage/loop-index-bounds/zero-constant-ok.c
new file mode 100644
index 00000000..2462c17a
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/zero-constant-ok.c
@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: Apache-2.0
+// A constant index past the end, in a loop that runs no iteration. The
+// existing report stays, with the unreachable-code note.
+void zero_constant_ok(void)
+{
+    char buf[10];
+    for (int i = 0; i < 0; ++i)
+        buf[10] = 'a';
+}
+
+// strict-expectation-details: true
+
+// at line 8, column 17
+// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ constant index 10 is out of bounds (0..9)
+// ↳ (this is a write access)
+// ↳ [info] this access appears unreachable at runtime (condition is always false for this branch)
diff --git a/test/bound-storage/loop-index-bounds/zero-trip-ok.c b/test/bound-storage/loop-index-bounds/zero-trip-ok.c
new file mode 100644
index 00000000..1d2d6cad
--- /dev/null
+++ b/test/bound-storage/loop-index-bounds/zero-trip-ok.c
@@ -0,0 +1,12 @@
+// SPDX-License-Identifier: Apache-2.0
+// A loop that runs no iteration: its body never runs.
+void zero_trip_ok(void)
+{
+    char buf[10];
+    for (int i = 10; i < 0; ++i)
+        buf[i] = 'a';
+}
+
+// strict-expectation-details: true
+
+// not contains: buffer overflow
diff --git a/test/bound-storage/ne-loop-guard-last-value.c b/test/bound-storage/ne-loop-guard-last-value.c
index 8ff55ec1..9f4e11ef 100644
--- a/test/bound-storage/ne-loop-guard-last-value.c
+++ b/test/bound-storage/ne-loop-guard-last-value.c
@@ -39,9 +39,9 @@ void ne_one_past(void)
 // not contains: at line 26, column 16
 
 // at line 34, column 16
-// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 12)
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 12)
 // ↳ alias path: buf
-// ↳ index variable may go up to 12 (array last valid index: 11)
+// ↳ index reaches 12 on every run of the function that returns (array last valid index: 11)
 // ↳ (this is a write access)
 
 // strict-expectation-details: true
diff --git a/test/bound-storage/ranges_test.c b/test/bound-storage/ranges_test.c
index 0f9b6fc2..25c54ca5 100644
--- a/test/bound-storage/ranges_test.c
+++ b/test/bound-storage/ranges_test.c
@@ -130,9 +130,9 @@ void loop_ub_overflow(void)
     char buf[10];
 
     // at line 137, column 16
-    // [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+    // [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
     // ↳ alias path: buf
-    // ↳ index variable may go up to 10 (array last valid index: 9)
+    // ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
     // ↳ (this is a write access)
     for (int i = 0; i <= 10; ++i)
         buf[i] = 'H';
@@ -271,3 +271,9 @@ int main(void)
 
     return 0;
 }
+
+// at line 147, column 16
+// [!!] negative index on variable 'buf' (size 10)
+// ↳ alias path: buf
+// ↳ index reaches -3 on every run of the function that returns
+// ↳ (this is a write access)
diff --git a/test/bound-storage/smt-path-loop-counter-is-kept.c b/test/bound-storage/smt-path-loop-counter-is-kept.c
index 94cf27b2..d09ca27e 100644
--- a/test/bound-storage/smt-path-loop-counter-is-kept.c
+++ b/test/bound-storage/smt-path-loop-counter-is-kept.c
@@ -20,7 +20,7 @@ void loop_counter(void)
 }
 
 // at line 17, column 16
-// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 16)
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 16)
 // ↳ alias path: buf
-// ↳ index variable may go up to 19 (array last valid index: 15)
+// ↳ index reaches 19 on every run of the function that returns (array last valid index: 15)
 // ↳ (this is a write access)
diff --git a/test/security/buffer-overflow/01_buffer_overflow.c b/test/security/buffer-overflow/01_buffer_overflow.c
index 3b608ad6..5fc36eba 100644
--- a/test/security/buffer-overflow/01_buffer_overflow.c
+++ b/test/security/buffer-overflow/01_buffer_overflow.c
@@ -86,7 +86,7 @@ int main(void)
 // ↳ declared without initializer and no definite write was found in this function
 
 // at line 41, column 16
-// [ !!Warn ] potential stack buffer overflow on variable 'buf' (size 10)
+// [ !!Warn ] stack buffer overflow on variable 'buf' (size 10)
 // ↳ alias path: buf
-// ↳ index variable may go up to 10 (array last valid index: 9)
+// ↳ index reaches 10 on every run of the function that returns (array last valid index: 9)
 // ↳ (this is a write access)
diff --git a/test/unit/analyzer_module_unit_tests.cpp b/test/unit/analyzer_module_unit_tests.cpp
index 003ead88..c0832316 100644
--- a/test/unit/analyzer_module_unit_tests.cpp
+++ b/test/unit/analyzer_module_unit_tests.cpp
@@ -10,6 +10,7 @@
 #include "analysis/InputPipelineRevision.hpp"
 #include "analysis/IntRanges.hpp"
 #include "analysis/IRValueUtils.hpp"
+#include "analysis/PromotedValues.hpp"
 #include "analysis/ParameterDebugBinding.hpp"
 #include "analysis/Reachability.hpp"
 #include "analysis/ResourceLifetimeAnalysis.hpp"
@@ -1692,6 +1693,223 @@ define i32 @entry_value(ptr %q) {
         return report.failures == 0;
     }
 
+    bool testPromotedValues(TestReport& report)
+    {
+        using ctrace::stack::analysis::IndexValues;
+        using ctrace::stack::analysis::PromotedValues;
+        llvm::LLVMContext context;
+        llvm::SMDiagnostic error;
+        // The same -O0 loop, `for (i = 0; i < 11; i++) buf[i] = 'a';`, without and with
+        // lifetime markers.
+        const std::unique_ptr<llvm::Module> module = llvm::parseAssemblyString(R"(
+define void @counted() {
+entry:
+  %buf = alloca [10 x i8]
+  %i = alloca i32
+  store i32 0, ptr %i
+  br label %cond
+cond:
+  %v = load i32, ptr %i
+  %c = icmp slt i32 %v, 11
+  br i1 %c, label %body, label %end
+body:
+  %w = load i32, ptr %i
+  %idx = sext i32 %w to i64
+  %p = getelementptr [10 x i8], ptr %buf, i64 0, i64 %idx
+  store i8 97, ptr %p
+  %n = add nsw i32 %w, 1
+  store i32 %n, ptr %i
+  br label %cond
+end:
+  ret void
+}
+define void @with_lifetime_markers() {
+entry:
+  %buf = alloca [10 x i8]
+  %i = alloca i32
+  call void @llvm.lifetime.start.p0(i64 10, ptr %buf)
+  store i32 0, ptr %i
+  br label %cond
+cond:
+  %v = load i32, ptr %i
+  %c = icmp slt i32 %v, 11
+  br i1 %c, label %body, label %end
+body:
+  %w = load i32, ptr %i
+  %idx = sext i32 %w to i64
+  %p = getelementptr [10 x i8], ptr %buf, i64 0, i64 %idx
+  store i8 97, ptr %p
+  %n = add nsw i32 %w, 1
+  store i32 %n, ptr %i
+  br label %cond
+end:
+  call void @llvm.lifetime.end.p0(i64 10, ptr %buf)
+  ret void
+}
+declare void @llvm.lifetime.start.p0(i64, ptr)
+declare void @llvm.lifetime.end.p0(i64, ptr)
+)",
+                                                                               error, context);
+        if (!module)
+        {
+            report.expect(false, "PromotedValues setup: the IR does not parse");
+            return false;
+        }
+
+        const auto gepOf = [&](const char* name)
+        {
+            for (const llvm::Instruction& inst : llvm::instructions(*module->getFunction(name)))
+            {
+                if (const auto* gep = llvm::dyn_cast<llvm::GetElementPtrInst>(&inst))
+                    return gep;
+            }
+            return static_cast<const llvm::GetElementPtrInst*>(nullptr);
+        };
+        const llvm::Function& counted = *module->getFunction("counted");
+        const std::size_t instructionsBefore = counted.getInstructionCount();
+
+        PromotedValues values(*module, [](const llvm::Function&) { return true; });
+        const llvm::GetElementPtrInst* access = gepOf("counted");
+        const IndexValues range = values.indexValuesAt(*access, *access->getOperand(2));
+        report.expect(range.kind == IndexValues::Kind::Range && range.min == 0 && range.max == 10,
+                      "PromotedValues: the counter of an 11-iteration loop takes 0..10");
+        report.expect(range.minOnEveryRun && range.maxOnEveryRun,
+                      "PromotedValues: an unconditional constant-count loop takes both endpoints");
+        report.expect(values.provesWithin(*access, *access->getOperand(2), 0, 11) &&
+                          !values.provesWithin(*access, *access->getOperand(2), 0, 10),
+                      "PromotedValues: the counter is proven below 11, not below 10");
+
+        const llvm::GetElementPtrInst* marked = gepOf("with_lifetime_markers");
+        report.expect(values.indexValuesAt(*marked, *marked->getOperand(2)).kind ==
+                          IndexValues::Kind::Unknown,
+                      "PromotedValues: a function with lifetime markers is left out");
+
+        const bool keepsFlags = llvm::any_of(llvm::instructions(counted),
+                                             [](const llvm::Instruction& inst)
+                                             {
+                                                 const auto* add =
+                                                     llvm::dyn_cast<llvm::BinaryOperator>(&inst);
+                                                 return add && add->hasNoSignedWrap();
+                                             });
+        report.expect(counted.getInstructionCount() == instructionsBefore &&
+                          llvm::isa<llvm::AllocaInst>(counted.getEntryBlock().front()) &&
+                          keepsFlags,
+                      "PromotedValues: the original function keeps its slots, loads and flags");
+        return report.failures == 0;
+    }
+
+    bool testIndexBoundsPerAccess(TestReport& report)
+    {
+        using ctrace::stack::analysis::StackBufferOverflowIssue;
+        llvm::LLVMContext context;
+        llvm::SMDiagnostic error;
+        // One address &buf[i], i in 0..10, used by accesses that run on different conditions.
+        const std::unique_ptr<llvm::Module> module = llvm::parseAssemblyString(R"(
+define void @shared_address() {
+entry:
+  %buf = alloca [10 x i8]
+  br label %header
+header:
+  %i = phi i64 [0, %entry], [%next, %latch]
+  %more = icmp slt i64 %i, 11
+  br i1 %more, label %body, label %exit
+body:
+  %p = getelementptr [10 x i8], ptr %buf, i64 0, i64 %i
+  %every = load i8, ptr %p
+  %low = icmp slt i64 %i, 10
+  br i1 %low, label %write, label %check
+write:
+  store i8 42, ptr %p
+  br label %check
+check:
+  %high = icmp sgt i64 %i, 4
+  br i1 %high, label %read, label %latch
+read:
+  %late = load i8, ptr %p
+  br label %latch
+latch:
+  %next = add i64 %i, 1
+  br label %header
+exit:
+  ret void
+}
+define void @guarded_write_only() {
+entry:
+  %buf = alloca [10 x i8]
+  br label %header
+header:
+  %i = phi i64 [0, %entry], [%next, %latch]
+  %more = icmp slt i64 %i, 11
+  br i1 %more, label %body, label %exit
+body:
+  %p = getelementptr [10 x i8], ptr %buf, i64 0, i64 %i
+  %low = icmp slt i64 %i, 10
+  br i1 %low, label %write, label %latch
+write:
+  store i8 42, ptr %p
+  br label %latch
+latch:
+  %next = add i64 %i, 1
+  br label %header
+exit:
+  ret void
+}
+define void @stored_address() {
+entry:
+  %buf = alloca [10 x i8]
+  %slot = alloca ptr
+  br label %header
+header:
+  %i = phi i64 [0, %entry], [%next, %header]
+  %p = getelementptr [10 x i8], ptr %buf, i64 0, i64 %i
+  store ptr %p, ptr %slot
+  %next = add i64 %i, 1
+  %more = icmp slt i64 %next, 11
+  br i1 %more, label %header, label %exit
+exit:
+  ret void
+}
+)",
+                                                                               error, context);
+        if (!module)
+        {
+            report.expect(false, "IndexBoundsPerAccess setup: the IR does not parse");
+            return false;
+        }
+
+        const ctrace::stack::AnalysisConfig config;
+        const auto issuesOf = [&](const char* name)
+        {
+            return ctrace::stack::analysis::analyzeStackBufferOverflows(
+                *module, [&](const llvm::Function& F) { return F.getName() == name; }, config);
+        };
+        const auto at = [](const std::vector<StackBufferOverflowIssue>& issues, const char* name)
+        {
+            return std::find_if(issues.begin(), issues.end(),
+                                [&](const StackBufferOverflowIssue& issue)
+                                { return issue.inst && issue.inst->getName() == name; });
+        };
+
+        const std::vector<StackBufferOverflowIssue> shared = issuesOf("shared_address");
+        const auto every = at(shared, "every");
+        const auto late = at(shared, "late");
+        report.expect(shared.size() == 2 && every != shared.end() && late != shared.end(),
+                      "IndexBoundsPerAccess: of three accesses through one address, the two that "
+                      "may run with i == 10 are reported, the one guarded by i < 10 is not");
+        report.expect(every != shared.end() && every->reachedOnEveryRun &&
+                          every->indexOrUpperBound == 10 && !every->isLowerBoundViolation,
+                      "IndexBoundsPerAccess: the unconditional access reaches 10 on every run");
+        report.expect(late != shared.end() && !late->reachedOnEveryRun &&
+                          late->indexOrUpperBound == 10,
+                      "IndexBoundsPerAccess: the access guarded by i > 4 may reach 10");
+        report.expect(issuesOf("guarded_write_only").empty(),
+                      "IndexBoundsPerAccess: an address formed up to &buf[10] and written only "
+                      "below 10 is not reported");
+        report.expect(issuesOf("stored_address").empty(),
+                      "IndexBoundsPerAccess: storing the address &buf[10] does not access buf");
+        return report.failures == 0;
+    }
+
     using ctrace::stack::analysis::smt::ConstraintIR;
     using ctrace::stack::analysis::smt::ExprId;
     using ctrace::stack::analysis::smt::ExprKind;
@@ -3027,6 +3245,8 @@ int main(int argc, char** argv)
     (void)testSmtEvaluatorEncodesLazily(report);
     (void)testFunctionFactsClobberingAccess(repoRoot, report);
     (void)testTryGetConstFromValue(report);
+    (void)testPromotedValues(report);
+    (void)testIndexBoundsPerAccess(report);
     (void)testSmtEncoderMemoryModel(repoRoot, report);
     (void)testSmtEncoderPathCondition(repoRoot, report);
 #ifdef CTRACE_STACK_ENABLE_Z3_BACKEND