#include <clang/Tooling/Tooling.h>

#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>

#include "fold/detect/oob_access.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"

namespace {

struct TestResult {
    std::vector<fold::Finding> findings;
    fold::SolverStats stats;
};

TestResult run(const std::string& code) {
    auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    auto findings = fold::detectOOBAccessInContext(unit->getASTContext(), b, s);
    return {std::move(findings), s};
}

} // namespace

TEST_CASE("oob-access: constant index 10 in `int a[4]` flagged Proved", "[oob][const]") {
    auto [findings, stats] = run("int f(){ int a[4] = {0}; return a[10]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE(findings[0].confidence == fold::Confidence::Proved);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("oob-access: negative constant index is formatted safely", "[oob][const]") {
    auto [findings, stats] = run("int f(){ int a[4] = {0}; return a[-1]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE(findings[0].message.find("buffer 'a'") != std::string::npos);
    REQUIRE(findings[0].message.find("-1") != std::string::npos);
    REQUIRE(findings[0].message.find("capacity 4") != std::string::npos);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("oob-access: constant index 2 in `int a[4]` is in-bounds", "[oob][safe]") {
    auto [findings, stats] = run("int f(){ int a[4] = {0}; return a[2]; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.unsat == 1);
}

TEST_CASE("oob-access: size()+1 buffer with size() index is in-bounds", "[oob][string-length]") {
    // `dup_cstr` idiom: malloc(b.size()+1) then p[b.size()]='\0'. The two
    // size() calls must resolve to the SAME length symbol (the intervening
    // assignment to `p` clears member_cache_ but not the string-length cache),
    // so the final write lands exactly at the end, not out of bounds. Uses a
    // self-contained struct because the test harness does not resolve
    // <string>; stringLengthObjectKey is class-agnostic (zero-arg const
    // size/length).
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "struct Buf { unsigned long n; unsigned long size() const; };\n"
                                 "char* dup(Buf b) {\n"
                                 "  char* p = (char*)malloc(b.size() + 1);\n"
                                 "  if (!p) return nullptr;\n"
                                 "  p[b.size()] = '\\0';\n"
                                 "  return p;\n"
                                 "}\n");
    REQUIRE(findings.empty());
}

TEST_CASE("oob-access: size()+1 buffer with size()+1 index still flagged", "[oob][string-length]") {
    // Clean negative: p[b.size()+1] is one byte past the end of the
    // b.size()+1 allocation, so the genuine OOB must still fire.
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "struct Buf { unsigned long n; unsigned long size() const; };\n"
                                 "char* dup(Buf b) {\n"
                                 "  char* p = (char*)malloc(b.size() + 1);\n"
                                 "  if (!p) return nullptr;\n"
                                 "  p[b.size() + 1] = '\\0';\n"
                                 "  return p;\n"
                                 "}\n");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
}

TEST_CASE("oob-access: symbolic index produces a Heuristic finding", "[oob][symbolic]") {
    auto [findings, stats] = run("int f(int i){ int a[4] = {0}; return a[i]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("oob-access: symbolic index expression produces a Heuristic finding", "[oob][symbolic]") {
    auto [findings, stats] = run("int f(int i){ int a[4] = {0}; return a[i + 1]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("oob-access: guarded symbolic index suppresses the finding", "[oob][guarded]") {
    // Path predicate inside the then-arm constrains i to [0, 4); OOB
    // predicate is UNSAT under that constraint.
    auto [findings, stats] = run("int f(int i){"
                                 "  int a[4] = {0};"
                                 "  if (i >= 0 && i < 4) return a[i];"
                                 "  return 0;"
                                 "}");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.unsat == 1);
}

TEST_CASE("oob-access: min-bounded index suppresses the finding", "[oob][min]") {
    // `lvl = min(p, 3)` is provably in [0, 3], so `a[lvl]` into a 4-element
    // array is in-bounds. A user-defined `min` keeps the test independent of
    // `<algorithm>` resolution in the synthetic AST. The bound is proven either
    // by the syntactic min-bound pre-check (abstract_unsat) or by the solver
    // (unsat) if the encoder inlines the call.
    auto [findings, stats] =
        run("static int min(int a, int b){ return a < b ? a : b; }\n"
            "int f(int p){ int a[4] = {0}; int lvl = min(p, 3); return a[lvl]; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
}

TEST_CASE("oob-access: modulo-bounded index suppresses the finding", "[oob][mod]") {
    // `i % 4` is provably in [0, 3]; indexing a 4-element array is in-bounds.
    // (The encoder proves the modulo bound natively; the syntactic check is a
    // redundant safety net for opaque-divisor cases.)
    auto [findings, stats] = run("int f(int i){ int a[4] = {0}; return a[i % 4]; }");
    REQUIRE(findings.empty());
}

TEST_CASE("oob-access: clamp-bounded index suppresses the finding", "[oob][clamp]") {
    // `clamp(i, 0, 3)` is provably in [0, 3] (bounded by the hi argument).
    auto [findings, stats] =
        run("static int clamp(int v, int lo, int hi){ return v < lo ? lo : (v > hi ? hi : v); }\n"
            "int f(int i){ int a[4] = {0}; int c = clamp(i, 0, 3); return a[c]; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
}

TEST_CASE("oob-access: single-trip loop guard suppresses second unrolled iteration",
          "[oob][loop][guard]") {
    auto [findings, stats] = run("int f(){"
                                 "  int amaxv[8] = {0};"
                                 "  int sum = 0;"
                                 "  for (int j = 0; j < 1; ++j) {"
                                 "    sum += amaxv[8 * j];"
                                 "    sum += amaxv[8 * j + 4];"
                                 "  }"
                                 "  return sum;"
                                 "}");
    REQUIRE(findings.empty());
    REQUIRE(stats.sat == 0);
}

TEST_CASE("oob-access: Curl_str max+1 terminator index is safe", "[oob][curl][safe]") {
    auto [findings, stats] =
        run("struct Curl_str { const char* str; unsigned long len; };\n"
            "extern int curlx_str_quotedword(const char**, Curl_str*, unsigned long);\n"
            "#define curlx_strlen(x) ((x)->len)\n"
            "int f(const char* in){ const char* line = in; Curl_str date{};\n"
            "  if(curlx_str_quotedword(&line, &date, 17)) return 0;\n"
            "  char dbuf[18]; dbuf[curlx_strlen(&date)] = 0; return dbuf[0]; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.sat == 0);
}

TEST_CASE("oob-access: Curl_str bound does not hide undersized buffers", "[oob][curl][tp]") {
    auto [findings, stats] =
        run("struct Curl_str { const char* str; unsigned long len; };\n"
            "extern int curlx_str_quotedword(const char**, Curl_str*, unsigned long);\n"
            "#define curlx_strlen(x) ((x)->len)\n"
            "int f(const char* in){ const char* line = in; Curl_str date{};\n"
            "  if(curlx_str_quotedword(&line, &date, 17)) return 0;\n"
            "  char dbuf[17]; dbuf[curlx_strlen(&date)] = 0; return dbuf[0]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: heap allocation with symbolic index is checked", "[oob][heap]") {
    auto [findings, stats] =
        run("extern \"C\" void* malloc(unsigned long);\n"
            "int f(int i){ int* p = (int*)malloc(4 * sizeof(int)); return p[i]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE_FALSE(findings[0].message.empty());
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: heap byte offset 63 in 64-byte buffer is in-bounds", "[oob][heap][offset]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "int f(){ char* buf = (char*)malloc(64); return buf[63]; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.unsat >= 1);
}

TEST_CASE("oob-access: heap byte offset 64 in 64-byte buffer is flagged", "[oob][heap][offset]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "int f(){ char* buf = (char*)malloc(64); return buf[64]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE_FALSE(findings[0].message.empty());
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: heap byte offset 100 in 64-byte buffer is flagged", "[oob][heap][offset]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "int f(){ char* buf = (char*)malloc(64); return buf[100]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE_FALSE(findings[0].message.empty());
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: heap finding attributes the correct allocation site", "[oob][heap][site]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "int f(){\n"
                                 "  char* a = (char*)malloc(64);\n"
                                 "  char* b = (char*)malloc(64);\n"
                                 "  return b[100];\n"
                                 "}");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE(findings[0].message.find("malloc at input.cpp:4") != std::string::npos);
    REQUIRE(findings[0].locations.size() >= 2);
    REQUIRE(findings[0].locations[1].line == 4);
    REQUIRE(findings[0].locations[1].function == "f");
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: derived heap pointer preserves byte offset", "[oob][heap][offset]") {
    auto [findings, stats] =
        run("extern \"C\" void* malloc(unsigned long);\n"
            "int f(){ char* buf = (char*)malloc(64); int* p = (int*)(buf + 10); return p[14]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE_FALSE(findings[0].message.empty());
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: C++ new array is tracked as heap allocation", "[oob][heap][new]") {
    auto [findings, stats] = run("int f(){ char* buf = new char[64]; return buf[64]; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: C++ delete array marks tracked allocation freed", "[oob][uaf][new]") {
    auto [findings, stats] =
        run("int f(){ char* buf = new char[4]; delete[] buf; return buf[0]; }");
    bool saw_uaf = false;
    for (const auto& finding : findings) {
        saw_uaf = saw_uaf || finding.message.find("Use-after-free") != std::string::npos;
    }
    REQUIRE(saw_uaf);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: use-after-free on tracked heap pointer is flagged", "[oob][uaf]") {
    auto [findings, stats] =
        run("extern \"C\" void* malloc(unsigned long);\n"
            "extern \"C\" void free(void*);\n"
            "int f(){ int* p = (int*)malloc(sizeof(int)); free(p); return p[0]; }");
    REQUIRE_FALSE(findings.empty());
    bool saw_uaf = false;
    for (const auto& finding : findings) {
        saw_uaf = saw_uaf || finding.message.find("Use-after-free") != std::string::npos;
    }
    REQUIRE(saw_uaf);
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: loop-allocated regions are not reported as cross-iteration uaf",
          "[oob][uaf][loop]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "extern \"C\" void free(void*);\n"
                                 "int f(){\n"
                                 "  int* p = nullptr;\n"
                                 "  for (int i = 0; i < 2; ++i) {\n"
                                 "    p = (int*)malloc(sizeof(int));\n"
                                 "    free(p);\n"
                                 "  }\n"
                                 "  return p[0];\n"
                                 "}");
    bool saw_uaf = false;
    for (const auto& finding : findings) {
        saw_uaf = saw_uaf || finding.message.find("Use-after-free") != std::string::npos;
    }
    REQUIRE_FALSE(saw_uaf);
}

TEST_CASE("oob-access: memcpy into undersized stack buffer is flagged", "[oob][stdlib][stack]") {
    auto [findings, stats] =
        run("extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"
            "int f(){ char src[128] = {0}; char dst[64] = {0}; memcpy(dst, src, 100); return 0; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("memcpy") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: oversized memcpy length does not drive byte modeling loop",
          "[oob][stdlib][wide-constant]") {
    auto [findings, stats] =
        run("extern \"C\" void* memcpy(void*, const void*, unsigned long long);\n"
            "int f(){ char src[1] = {0}; char dst[1] = {0}; "
            "memcpy(dst, src, 18446744073709551615ULL); return 0; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("18446744073709551615") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: memcpy within stack buffer capacity is safe", "[oob][stdlib][stack]") {
    auto [findings, stats] =
        run("extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"
            "int f(){ char src[128] = {0}; char dst[64] = {0}; memcpy(dst, src, 32); return 0; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.unsat >= 1);
}

TEST_CASE("oob-access: memcpy into undersized heap buffer is flagged", "[oob][stdlib][heap]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"
                                 "int f(){ char src[128] = {0}; char* dst = (char*)malloc(64); "
                                 "memcpy(dst, src, 100); return 0; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("memcpy") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: memcpy through stack pointer alias is flagged", "[oob][stdlib][stack]") {
    auto [findings, stats] =
        run("extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"
            "int f(){ char src[128] = {0}; char buf[64] = {0}; char* dst; dst = buf; "
            "memcpy(dst, src, 100); return 0; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("memcpy") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: memcpy through heap pointer alias is flagged", "[oob][stdlib][heap]") {
    auto [findings, stats] = run("extern \"C\" void* malloc(unsigned long);\n"
                                 "extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"
                                 "int f(){ char src[128] = {0}; char* buf = (char*)malloc(64); "
                                 "char* dst; dst = buf; memcpy(dst, src, 100); return 0; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("memcpy") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: snprintf bound beyond destination size is flagged", "[oob][stdlib][heap]") {
    auto [findings, stats] =
        run("extern \"C\" void* malloc(unsigned long);\n"
            "extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "int f(){ char* dst = (char*)malloc(64); return snprintf(dst, 100, \"%s\", \"x\"); }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("snprintf") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: strlen uses tracked char-array initializer length",
          "[oob][stdlib][strlen]") {
    auto [findings, stats] =
        run("extern \"C\" unsigned long strlen(const char*);\n"
            "extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "int f(){ char src[16] = \"abcdefghij\"; char dst[4] = {0}; "
            "return snprintf(dst, strlen(src) + 1, \"%s\", src); }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("snprintf") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: memcpy propagates copied string length to strlen", "[oob][stdlib][strlen]") {
    auto [findings, stats] =
        run("extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"
            "extern \"C\" unsigned long strlen(const char*);\n"
            "extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "int f(){ char src[8] = \"abcdef\"; char tmp[8] = {0}; char dst[4] = {0}; "
            "memcpy(tmp, src, 7); return snprintf(dst, strlen(tmp) + 1, \"%s\", tmp); }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("snprintf") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: strncpy propagates terminated string length to strlen",
          "[oob][stdlib][strlen]") {
    auto [findings, stats] =
        run("extern \"C\" char* strncpy(char*, const char*, unsigned long);\n"
            "extern \"C\" unsigned long strlen(const char*);\n"
            "extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "int f(){ char src[8] = \"abcdef\"; char tmp[8] = {0}; char dst[4] = {0}; "
            "strncpy(tmp, src, 7); return snprintf(dst, strlen(tmp) + 1, \"%s\", tmp); }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("snprintf") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: strcpy into undersized stack buffer is flagged", "[oob][stdlib][stack]") {
    auto [findings, stats] = run(
        "extern \"C\" char* strcpy(char*, const char*);\n"
        "int f(){ char buf[10] = {0}; strcpy(buf, \"this string is way too long\"); return 0; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("strcpy") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob-access: strcpy with fitting literal is safe", "[oob][stdlib][stack]") {
    auto [findings, stats] =
        run("extern \"C\" char* strcpy(char*, const char*);\n"
            "int f(){ char buf[100] = {0}; strcpy(buf, \"short\"); return 0; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.unsat >= 1);
}

TEST_CASE("oob-access: sprintf percent-s literal into undersized stack buffer is flagged",
          "[oob][stdlib][stack]") {
    auto [findings, stats] = run("extern \"C\" int sprintf(char*, const char*, ...);\n"
                                 "int f(){ char buf[10] = {0}; return sprintf(buf, \"%s\", \"this "
                                 "string is way too long\"); }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].message.find("sprintf") != std::string::npos);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("oob: snprintf fixed-width hex fits exact stack buffer", "[oob][snprintf][format]") {
    auto [findings, stats] =
        run("extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "void f(unsigned char b){ char buf[3]; snprintf(buf, sizeof(buf), \"%02x\", b); }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("oob: destination-bounded snprintf truncation is not an overflow",
          "[oob][snprintf][format]") {
    auto [findings, stats] =
        run("extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "void f(unsigned char b){ char buf[2]; snprintf(buf, sizeof(buf), \"%02x\", b); }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("oob: snprintf fixed-width decimal fits full int stack buffer",
          "[oob][snprintf][format]") {
    auto [findings, stats] =
        run("extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "void f(int n){ char buf[12]; snprintf(buf, sizeof(buf), \"%03d\", n); }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("oob: destination bound prevents minimum-width decimal overflow",
          "[oob][snprintf][format]") {
    auto [findings, stats] =
        run("extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "void f(int n){ char buf[8]; snprintf(buf, sizeof(buf), \"%03d\", n); }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("oob: snprintf bounded clamp decimal fits small stack buffer",
          "[oob][snprintf][format]") {
    auto [findings, stats] =
        run("namespace std { double lround(double); template<class T> T clamp(T, T, T); }\n"
            "extern \"C\" int snprintf(char*, unsigned long, const char*, ...);\n"
            "struct C { double alpha; };\n"
            "void f(C c){ int a100 = static_cast<int>(std::lround(std::clamp(c.alpha, 0.0, 1.0) * "
            "100.0)); "
            "char buf[8]; snprintf(buf, sizeof(buf), \"%03d\", a100); }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("oob: uniform int distribution index within array length", "[oob][array][random]") {
    auto [findings, stats] =
        run("namespace std { template<class T=int> struct uniform_int_distribution { "
            "uniform_int_distribution(int, int); int operator()(int&); }; } "
            "char f(int& gen){ const char hex_chars[] = \"0123456789abcdef\"; "
            "std::uniform_int_distribution<> dis(0, 15); "
            "return hex_chars[dis(gen)]; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
}

TEST_CASE("oob: readlink count bounded by destination minus nul", "[oob][array][readlink]") {
    auto [findings, stats] = run(
        "extern \"C\" long readlink(const char*, char*, unsigned long); "
        "void f(const char* path){ char buf[4096]; long n = readlink(path, buf, sizeof(buf) - 1); "
        "if(n > 0) buf[n] = '\\0'; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
}

TEST_CASE("oob: snprintf destination-sized bound suppresses long float format",
          "[oob][snprintf][format]") {
    auto [findings, stats] =
        run("extern \"C\" int snprintf(char*, unsigned long, const char*, ...); "
            "void f(double value){ char buf[16]; snprintf(buf, sizeof(buf), \"%.3f\", value); }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
}

TEST_CASE("oob: interprocedural buffer-bound from decayed stack array", "[oob][interproc]") {
    // T160: decode_base64(basic_auth, decoded) where decoded[256] decays
    // to char* output.  The callee writes output[output_index++] in an
    // unbounded loop.  Fold must thread the 256-element buffer size from
    // the call site and flag the OOB.
    auto [findings, stats] =
        run("void decode_base64(const char* input, char* output);\n" // fwd decl
            "int f(const char* basic_auth) {\n"
            "  char decoded[256];\n"
            "  decode_base64(basic_auth, decoded);\n"
            "  return decoded[0];\n"
            "}\n"
            "void decode_base64(const char* input, char* output) {\n"
            "  int output_index = 0;\n"
            "  for (int i = 0; input[i] != 0; ++i) {\n"
            "    output[output_index++] = input[i];\n"
            "  }\n"
            "  output[output_index] = 0;\n"
            "}");
    REQUIRE_FALSE(findings.empty());
    bool saw_oob_on_output = false;
    for (const auto& f : findings) {
        if (f.kind == fold::FindingKind::OOBAccess && f.evidence.variable_name == "output") {
            saw_oob_on_output = true;
        }
    }
    REQUIRE(saw_oob_on_output);
}

TEST_CASE("oob: pre-pass seeds callee buffer from caller ConstantArrayType arg",
          "[oob][interproc]") {
    // T163: Callee defined BEFORE caller (declaration order). Caller
    // passes a stack array (ConstantArrayType) to the callee. The callee
    // has an ArraySubscriptExpr that writes past the buffer bounds.
    // The pre-pass seedInterproceduralContext() must populate
    // param_buffer_sizes_ before any function walk so the callee's
    // OOB is flagged even though it appears first in the TU.
    auto [findings, stats] = run("void fill_buf(char* buf) {\n" // callee FIRST, no fwd decl
                                 "  int i = 0;\n"
                                 "  while (i < 20) {\n"
                                 "    buf[i] = (char)('a' + i);\n"
                                 "    i++;\n"
                                 "  }\n"
                                 "  buf[i] = 0;\n"
                                 "}\n"
                                 "int caller() {\n"   // caller SECOND
                                 "  char small[8];\n" // ConstantArrayType char[8]
                                 "  fill_buf(small);\n"
                                 "  return small[0];\n"
                                 "}");
    REQUIRE_FALSE(findings.empty());
    bool saw_oob_on_buf = false;
    for (const auto& f : findings) {
        if (f.kind == fold::FindingKind::OOBAccess && f.evidence.variable_name == "buf") {
            saw_oob_on_buf = true;
        }
    }
    REQUIRE(saw_oob_on_buf);
}