fix(report): keep Proved for exact bounded models only

Problem: docs/research/soundness.md defines `proved` as an exact bounded
model establishing the property, but several detectors assigned Proved
without one: double-free from a heap-model flag, static-ptr-asymmetry from
a cross-function pattern, unused-function and dead-statement from AST
facts, the stdlib copy-overflow check, and the heap use-after-free / OOB
checks from SAT results whose encoding precision was never consulted. A
SAT result over an over-approximated path (an opaque call, an unsupported
node) can be spurious.

Fix: double-free and static-ptr-asymmetry report Heuristic; unused-function
and dead-statement report Syntactic; the stdlib copy check reports
Heuristic. Heap OOB and use-after-free keep Proved only when the path's
SymbolicEnv carries no imprecision tag. So that `malloc(sizeof(T))` paths
stay exact, sizeof/alignof on complete non-VLA types are now encoded as
exact constants (symbolic::typeTraitConstant) instead of an unsupported
node.

Test: tests/unit/test_proved_requires_exact_model.cpp covers each
downgraded detector, a heap UAF on an exact path (stays Proved, control)
and under an opaque call (Heuristic), and typeTraitConstant including the
VLA negative case. Full suite: 138/138.

include/fold/symbolic/encoder_type_queries.hpp

@@ -3,10 +3,12 @@
 #include <z3++.h>
 
 #include <cstdint>
+#include <optional>
 
 namespace clang {
 class ASTContext;
 class QualType;
+class UnaryExprOrTypeTraitExpr;
 } // namespace clang
 
 namespace fold {
@@ -45,4 +47,11 @@ namespace fold::symbolic {
 [[nodiscard]] z3::expr byteWidthExpr(SymbolicEnv& env, const clang::ASTContext& ctx,
                                      const clang::QualType& qt);
 
+// The exact value of `sizeof` / `alignof` (and the other type traits) when
+// the compiler folds it to a constant: complete, non-dependent, non-VLA
+// operands. nullopt otherwise; the encoder then treats the node as
+// unsupported rather than guess a size.
+[[nodiscard]] std::optional<std::uint64_t>
+typeTraitConstant(const clang::ASTContext& ctx, const clang::UnaryExprOrTypeTraitExpr* expr);
+
 } // namespace fold::symbolic

src/detect/dead_statement.cpp

@@ -204,7 +204,8 @@ class DeadStatementVisitor : public clang::RecursiveASTVisitor<DeadStatementVisi
 
             Finding f;
             f.kind = FindingKind::DeadStatement;
-            f.confidence = Confidence::Proved;
+            // A CFG fact read off the AST, not a solver result.
+            f.confidence = Confidence::Syntactic;
             f.locations.push_back(locOf(anchor, ctx_, fname));
             const auto statement_anchor = stableStatementAnchor(anchor, ctx_);
             f.id = stableQualityFindingId("dead-statement", stableFunctionId(fd), statement_anchor);

src/detect/double_free.cpp

@@ -76,7 +76,10 @@ class DoubleFreeObserver : public SafetyObserver {
         Finding f;
         f.id = "double-free:" + current_function_ + ":" + dedup_key;
         f.kind = FindingKind::DoubleFree;
-        f.confidence = Confidence::Proved;
+        // No solver query backs this: it is the heap model's freed flag on the
+        // walked path, and the path itself is never checked. Proved needs an
+        // exact bounded model (docs/research/soundness.md).
+        f.confidence = Confidence::Heuristic;
         f.message = "Double-free: heap allocation freed at " + current_function_ + ":" + dedup_key +
                     " was already freed on this path";
         Location l;

src/detect/oob_access.cpp

@@ -210,7 +210,7 @@ class OOBObserver : public SafetyObserver {
                           const clang::VarDecl* base_var = nullptr) override {
         SolverStats::ScopedHookTimer _t(stats_);
         if (heap_access) {
-            checkUseAfterFree(*heap_access, path, loc);
+            checkUseAfterFree(*heap_access, path, loc, env);
         }
         if (known_len < 0) {
             // T160: interprocedural buffer-bound threading (ParmVarDecl sizes).
@@ -240,7 +240,7 @@ class OOBObserver : public SafetyObserver {
             }
             if (known_len < 0) {
                 if (heap_access)
-                    checkHeapBounds(*heap_access, path, loc);
+                    checkHeapBounds(*heap_access, path, loc, env);
                 return;
             }
         }
@@ -381,19 +381,22 @@ class OOBObserver : public SafetyObserver {
                         const clang::VarDecl* /*var*/, const ir::SourceLoc& loc,
                         const ::fold::symbolic::HeapAccessInfo* heap_access,
                         const ::fold::DefUseContext* /*def_use*/,
-                        const ::fold::SymbolicEnv* /*env*/) override {
+                        const ::fold::SymbolicEnv* env) override {
         if (!heap_access)
             return;
-        checkUseAfterFree(*heap_access, path, loc);
+        checkUseAfterFree(*heap_access, path, loc, env);
         // Member writes bounds-check the region (placement_new_*: intTwo @8>4).
         if (heap_access->alloc_id != 0)
-            checkHeapBounds(*heap_access, path, loc);
+            checkHeapBounds(*heap_access, path, loc, env);
     }
 
     void onFree(const z3::expr& /*ptr*/, const ir::Expr& /*ptrExpr*/, const z3::expr& /*path*/,
                 const ir::SourceLoc& loc, bool known_region, bool was_already_freed) override {
+        // No query backs this: it is the heap model's freed flag, so it cannot
+        // be Proved (docs/research/soundness.md).
         if (known_region && was_already_freed) {
-            emitUseAfterFree(loc, nullptr, "Double free on tracked heap region");
+            emitUseAfterFree(loc, nullptr, "Double free on tracked heap region",
+                             /*exact_model=*/false);
         }
     }
 
@@ -436,22 +439,29 @@ class OOBObserver : public SafetyObserver {
     }
 
   private:
+    // Proved needs an exact bounded model (docs/research/soundness.md): a SAT
+    // result from an over-approximated encoding may be spurious.
+    static bool exactEncoding(const SymbolicEnv* env) {
+        return env != nullptr && !env->tag().isImprecise();
+    }
+
     void checkHeapBounds(const symbolic::HeapAccessInfo& heap_access, const z3::expr& path,
-                         const ir::SourceLoc& loc) {
+                         const ir::SourceLoc& loc, const SymbolicEnv* env) {
         z3::expr end = heap_access.offset + heap_access.width;
         z3::expr hazard = (heap_access.ptr != heap_access.ptr.ctx().bv_val(0, 64)) &&
                           !heap_access.is_use_after_free && z3::ugt(end, heap_access.region_size);
         if (checkHazard(path, hazard, loc, "oob-access-heap") == z3::sat) {
-            emitHeap(heap_access, loc);
+            emitHeap(heap_access, loc, exactEncoding(env));
         }
     }
 
     void checkUseAfterFree(const symbolic::HeapAccessInfo& heap_access, const z3::expr& path,
-                           const ir::SourceLoc& loc) {
+                           const ir::SourceLoc& loc, const SymbolicEnv* env) {
         if (checkHazard(path, heap_access.is_use_after_free, loc, "uaf-access") == z3::sat) {
             emitUseAfterFree(loc, &heap_access,
                              "Use-after-free on heap buffer from " +
-                                 describeAllocationSite(heap_access.site));
+                                 describeAllocationSite(heap_access.site),
+                             exactEncoding(env));
         }
     }
 
@@ -652,8 +662,10 @@ class OOBObserver : public SafetyObserver {
         Finding f;
         f.kind = FindingKind::OOBAccess;
         const auto size_value = numeralU64(size_expr);
+        // The copy hook carries no encoding precision, so even a constant size
+        // over a constant capacity is not an exact bounded model of the path.
+        f.confidence = Confidence::Heuristic;
         const bool is_const = size_value.has_value();
-        f.confidence = is_const ? Confidence::Proved : Confidence::Heuristic;
         Location l = locationFromSloc(loc);
         f.locations.push_back(std::move(l));
         f.id = std::string("oob-access:") + f.locations.front().file + ":" +
@@ -835,11 +847,12 @@ class OOBObserver : public SafetyObserver {
         out_.push_back(std::move(f));
     }
 
-    void emitHeap(const symbolic::HeapAccessInfo& heap_access, const ir::SourceLoc& loc) {
+    void emitHeap(const symbolic::HeapAccessInfo& heap_access, const ir::SourceLoc& loc,
+                  bool exact_model) {
         Finding f;
         f.kind = FindingKind::OOBAccess;
-        f.confidence =
-            heap_access.region_size.is_numeral() ? Confidence::Proved : Confidence::Heuristic;
+        f.confidence = heap_access.region_size.is_numeral() && exact_model ? Confidence::Proved
+                                                                           : Confidence::Heuristic;
         Location l = locationFromSloc(loc);
         f.locations.push_back(std::move(l));
         if (!heap_access.site.file.empty()) {
@@ -864,10 +877,10 @@ class OOBObserver : public SafetyObserver {
     }
 
     void emitUseAfterFree(const ir::SourceLoc& loc, const symbolic::HeapAccessInfo* heap_access,
-                          const std::string& message) {
+                          const std::string& message, bool exact_model) {
         Finding f;
         f.kind = FindingKind::OOBAccess;
-        f.confidence = Confidence::Proved;
+        f.confidence = exact_model ? Confidence::Proved : Confidence::Heuristic;
         Location l = locationFromSloc(loc);
         f.locations.push_back(std::move(l));
         if (heap_access && !heap_access->site.file.empty()) {

src/detect/static_ptr_asymmetry.cpp

@@ -319,7 +319,9 @@ std::vector<Finding> detectStaticPtrAsymmetryInContext(clang::ASTContext& ctx) {
 
             Finding f;
             f.kind = FindingKind::NullDeref;
-            f.confidence = Confidence::Proved;
+            // A cross-function discipline pattern, not a solver result: the
+            // unchecked function may be unreachable while the pointer is null.
+            f.confidence = Confidence::Heuristic;
             f.locations.push_back(locOf(ctx, loc, fd->getQualifiedNameAsString()));
             f.id = std::string("static-ptr-asymmetry:") + f.locations.front().file + ":" +
                    std::to_string(f.locations.front().line) + ":" +

src/detect/unused_function.cpp

@@ -219,7 +219,8 @@ std::vector<Finding> detectUnusedFunctionsInContext(clang::ASTContext& ctx) {
 
         Finding f;
         f.kind = FindingKind::UnusedFunction;
-        f.confidence = Confidence::Proved;
+        // A call-graph fact read off the AST, not a solver result.
+        f.confidence = Confidence::Syntactic;
         f.locations.push_back(locOf(fd, ctx));
         f.id = stableQualityFindingId("unused-function", stableFunctionId(fd));
         f.message = "Static function `" + fd->getNameAsString() +

src/detect/use_after_free.cpp

@@ -23,6 +23,7 @@
 
 #include "fold/detect/security_walker.hpp"
 #include "fold/symbolic/budget.hpp"
+#include "fold/symbolic/encoder.hpp"
 #include "fold/symbolic/encoder_callee_names.hpp"
 #include "fold/symbolic/heap_model.hpp"
 #include "fold/symbolic/safety_observer.hpp"
@@ -415,33 +416,35 @@ class UseAfterFreeObserver : public SafetyObserver {
                         const clang::VarDecl* /*var*/, const ir::SourceLoc& loc,
                         const ::fold::symbolic::HeapAccessInfo* heap_access,
                         const ::fold::DefUseContext* /*def_use*/,
-                        const ::fold::SymbolicEnv* /*env*/) override {
+                        const ::fold::SymbolicEnv* env) override {
         if (!heap_access)
             return;
-        checkUseAfterFree(*heap_access, path, loc);
+        checkUseAfterFree(*heap_access, path, loc, env);
     }
 
     void onArraySubscript(const z3::expr& /*idx*/, int /*known_len*/, const z3::expr& path,
                           const ir::SourceLoc& loc,
                           const ::fold::symbolic::HeapAccessInfo* heap_access,
-                          const ::fold::DefUseContext* /*def_use*/,
-                          const ::fold::SymbolicEnv* /*env*/, const clang::Expr* /*idx_expr*/,
+                          const ::fold::DefUseContext* /*def_use*/, const ::fold::SymbolicEnv* env,
+                          const clang::Expr* /*idx_expr*/,
                           const clang::VarDecl* /*base_var*/) override {
         if (!heap_access)
             return;
-        checkUseAfterFree(*heap_access, path, loc);
+        checkUseAfterFree(*heap_access, path, loc, env);
     }
 
     void onFree(const z3::expr& /*ptr*/, const ir::Expr& /*ptrExpr*/, const z3::expr& /*path*/,
                 const ir::SourceLoc& loc, bool known_region, bool was_already_freed) override {
+        // The heap model's freed flag, with no query behind it: not Proved.
         if (known_region && was_already_freed) {
-            emitUseAfterFree(loc, nullptr, "Double free on tracked heap region");
+            emitUseAfterFree(loc, nullptr, "Double free on tracked heap region",
+                             /*exact_model=*/false);
         }
     }
 
   private:
     void checkUseAfterFree(const symbolic::HeapAccessInfo& heap_access, const z3::expr& path,
-                           const ir::SourceLoc& loc) {
+                           const ir::SourceLoc& loc, const SymbolicEnv* env) {
         z3::context& c = const_cast<z3::context&>(heap_access.is_use_after_free.ctx());
         z3::expr hazard = heap_access.is_use_after_free;
 
@@ -451,7 +454,11 @@ class UseAfterFreeObserver : public SafetyObserver {
         z3::check_result result = checkHazard(path, hazard, loc, "use-after-free");
         if (result == z3::sat) {
             std::string alloc_desc = describeAllocationSite(heap_access.site);
-            emitUseAfterFree(loc, &heap_access, "Use-after-free on heap buffer from " + alloc_desc);
+            // Proved needs an exact bounded model: a SAT result from an
+            // over-approximated encoding may be spurious (soundness.md).
+            const bool exact = env != nullptr && !env->tag().isImprecise();
+            emitUseAfterFree(loc, &heap_access, "Use-after-free on heap buffer from " + alloc_desc,
+                             exact);
         }
     }
 
@@ -512,10 +519,10 @@ class UseAfterFreeObserver : public SafetyObserver {
     }
 
     void emitUseAfterFree(const ir::SourceLoc& loc, const symbolic::HeapAccessInfo* heap_access,
-                          const std::string& message) {
+                          const std::string& message, bool exact_model) {
         Finding f;
         f.kind = FindingKind::UseAfterFree;
-        f.confidence = Confidence::Proved;
+        f.confidence = exact_model ? Confidence::Proved : Confidence::Heuristic;
         f.locations.push_back(locationFromSloc(loc));
         if (heap_access && !heap_access->site.file.empty()) {
             Location alloc_loc;

src/symbolic/encoder_expr.cpp

@@ -611,6 +611,12 @@ z3::expr encodeExpr(ir::Expr expr_ir, const clang::ASTContext& ctx, SymbolicEnv&
     // is now empty — any unmigrated AST kind falls through to the
     // unsupported-node bail at the function end.
 
+    if (const auto* trait = dyn_cast<UnaryExprOrTypeTraitExpr>(e)) {
+        if (auto value = symbolic::typeTraitConstant(ctx, trait))
+            return markEncoded("UnaryExprOrTypeTraitExpr",
+                               env.ctx().bv_val(static_cast<std::uint64_t>(*value), kBitvecWidth));
+    }
+
     recordBailedNode(expr->getStmtClassName(),
                      std::string("expr kind ") + expr->getStmtClassName());
     recordPrecision(env, EncodingPrecision::UnsupportedNode,

src/symbolic/encoder_type_queries.cpp

@@ -1,6 +1,7 @@
 #include "fold/symbolic/encoder_type_queries.hpp"
 
 #include <clang/AST/ASTContext.h>
+#include <clang/AST/Expr.h>
 #include <clang/AST/Type.h>
 
 #include "fold/symbolic/encoder.hpp"
@@ -46,4 +47,19 @@ z3::expr byteWidthExpr(SymbolicEnv& env, const clang::ASTContext& ctx, const cla
     return env.ctx().bv_val(typeSizeBytes(ctx, qt), kBitvecWidth);
 }
 
+std::optional<std::uint64_t> typeTraitConstant(const clang::ASTContext& ctx,
+                                               const clang::UnaryExprOrTypeTraitExpr* expr) {
+    if (expr == nullptr || expr->isValueDependent() || expr->isTypeDependent())
+        return std::nullopt;
+    clang::Expr::EvalResult result;
+    if (!expr->EvaluateAsInt(result, ctx) || !result.Val.isInt())
+        return std::nullopt;
+    const llvm::APSInt& value = result.Val.getInt();
+    if (value.isSigned() && value.isNegative())
+        return std::nullopt;
+    if (value.getActiveBits() > 64)
+        return std::nullopt;
+    return value.getZExtValue();
+}
+
 } // namespace fold::symbolic

tests/unit/meson.build

@@ -204,6 +204,15 @@ test_library_callee_identity = executable(
 )
 test('library_callee_identity', test_library_callee_identity)
 
+test_proved_requires_exact_model = executable(
+  'test_proved_requires_exact_model',
+  'test_proved_requires_exact_model.cpp',
+  dependencies: [fold_core_dep, catch2_dep],
+  install: false,
+  build_by_default: false,
+)
+test('proved_requires_exact_model', test_proved_requires_exact_model)
+
 test_batch_safety_observer = executable(
   'test_batch_safety_observer',
   'test_batch_safety_observer.cpp',

tests/unit/test_proved_requires_exact_model.cpp

@@ -0,0 +1,163 @@
+#include <clang/AST/RecursiveASTVisitor.h>
+#include <clang/Frontend/ASTUnit.h>
+#include <clang/Tooling/Tooling.h>
+
+#include <catch2/catch_test_macros.hpp>
+#include <memory>
+#include <optional>
+#include <string>
+#include <vector>
+
+#include "fold/detect/dead_statement.hpp"
+#include "fold/detect/double_free.hpp"
+#include "fold/detect/oob_access.hpp"
+#include "fold/detect/static_ptr_asymmetry.hpp"
+#include "fold/detect/unused_function.hpp"
+#include "fold/detect/use_after_free.hpp"
+#include "fold/report/finding.hpp"
+#include "fold/symbolic/budget.hpp"
+#include "fold/symbolic/encoder_type_queries.hpp"
+
+// docs/research/soundness.md: `proved` means an exact bounded model
+// established the property. These detectors assigned Proved without one:
+// from a heap-model flag (double-free), a cross-function pattern
+// (static-ptr-asymmetry), an AST fact (unused-function, dead-statement), or a
+// SAT result whose encoding precision was never checked (stdlib OOB copy,
+// use-after-free under an unknown call).
+
+namespace {
+
+std::unique_ptr<clang::ASTUnit> parse(const std::string& code) {
+    return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
+}
+
+std::optional<fold::Confidence> confidenceOf(const std::vector<fold::Finding>& findings,
+                                             fold::FindingKind kind) {
+    for (const auto& f : findings)
+        if (f.kind == kind)
+            return f.confidence;
+    return std::nullopt;
+}
+
+const std::string kLibc = "extern \"C\" void* malloc(unsigned long);\n"
+                          "extern \"C\" void free(void*);\n"
+                          "extern \"C\" void* memcpy(void*, const void*, unsigned long);\n";
+
+} // namespace
+
+TEST_CASE("double-free without a solver query is Heuristic", "[proved-contract][double-free]") {
+    auto unit =
+        parse(kLibc + "void f() { void* p = malloc(8); if (!p) return; free(p); free(p); }");
+    REQUIRE(unit);
+    fold::SolverBudget b;
+    fold::SolverStats s;
+    const auto c = confidenceOf(fold::detectDoubleFreeInContext(unit->getASTContext(), b, s),
+                                fold::FindingKind::DoubleFree);
+    REQUIRE(c.has_value());
+    CHECK(*c == fold::Confidence::Heuristic);
+}
+
+TEST_CASE("static-ptr-asymmetry is a pattern, not a proof", "[proved-contract][static-ptr]") {
+    auto unit = parse("struct S { int v; };\n"
+                      "static S* g_state = nullptr;\n"
+                      "int checked() { if (!g_state) return 0; return g_state->v; }\n"
+                      "int unchecked() { return g_state->v; }\n");
+    REQUIRE(unit);
+    const auto c = confidenceOf(fold::detectStaticPtrAsymmetryInContext(unit->getASTContext()),
+                                fold::FindingKind::NullDeref);
+    REQUIRE(c.has_value());
+    CHECK(*c == fold::Confidence::Heuristic);
+}
+
+TEST_CASE("unused static function is an AST fact: Syntactic", "[proved-contract][unused]") {
+    auto unit = parse("static int helper(int x) { return x + 1; }\nint api(int x) { return x; }\n");
+    REQUIRE(unit);
+    const auto c = confidenceOf(fold::detectUnusedFunctionsInContext(unit->getASTContext()),
+                                fold::FindingKind::UnusedFunction);
+    REQUIRE(c.has_value());
+    CHECK(*c == fold::Confidence::Syntactic);
+}
+
+TEST_CASE("statement after return is an AST fact: Syntactic", "[proved-contract][dead-stmt]") {
+    auto unit = parse("int f(int x) { return x; x += 1; }\n");
+    REQUIRE(unit);
+    const auto c = confidenceOf(fold::detectDeadStatementsInContext(unit->getASTContext()),
+                                fold::FindingKind::DeadStatement);
+    REQUIRE(c.has_value());
+    CHECK(*c == fold::Confidence::Syntactic);
+}
+
+TEST_CASE("stdlib copy overflow without encoding precision is Heuristic",
+          "[proved-contract][oob]") {
+    auto unit = parse(kLibc + "void f(const char* src) { char buf[8]; memcpy(buf, src, 16); }");
+    REQUIRE(unit);
+    fold::SolverBudget b;
+    fold::SolverStats s;
+    const auto c = confidenceOf(fold::detectOOBAccessInContext(unit->getASTContext(), b, s),
+                                fold::FindingKind::OOBAccess);
+    REQUIRE(c.has_value());
+    CHECK(*c == fold::Confidence::Heuristic);
+}
+
+TEST_CASE("heap use-after-free keeps Proved only on an exact encoding", "[proved-contract][uaf]") {
+    // The SAT-backed heap use-after-free surfaces through the OOB detector
+    // (`uaf-access`).
+    auto uafConfidence = [](const std::string& code) -> std::optional<fold::Confidence> {
+        auto unit = parse(code);
+        REQUIRE(unit);
+        fold::SolverBudget b;
+        fold::SolverStats s;
+        for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s))
+            if (f.id.rfind("uaf-access:", 0) == 0)
+                return f.confidence;
+        return std::nullopt;
+    };
+    SECTION("exact: stays Proved (control)") {
+        const auto c = uafConfidence(
+            kLibc + "int f() { int* p = (int*)malloc(sizeof(int)); free(p); return p[0]; }");
+        REQUIRE(c.has_value());
+        CHECK(*c == fold::Confidence::Proved);
+    }
+    SECTION("an over-approximated operation on the path: Heuristic") {
+        const auto c = uafConfidence(kLibc + "extern int opaque(int);\n"
+                                             "int f(int k) { int* p = (int*)malloc(sizeof(int));"
+                                             " int n = opaque(k); free(p); return p[n - n]; }");
+        REQUIRE(c.has_value());
+        CHECK(*c == fold::Confidence::Heuristic);
+    }
+}
+
+namespace {
+
+// Value of the first sizeof/alignof in `code`, as the encoder would see it.
+std::optional<std::uint64_t> firstTypeTrait(const std::string& code, bool c_mode = false) {
+    auto unit = c_mode ? clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c11"}, "input.c")
+                       : parse(code);
+    REQUIRE(unit);
+    struct Finder : clang::RecursiveASTVisitor<Finder> {
+        const clang::UnaryExprOrTypeTraitExpr* found = nullptr;
+        bool VisitUnaryExprOrTypeTraitExpr(clang::UnaryExprOrTypeTraitExpr* e) {
+            if (!found)
+                found = e;
+            return true;
+        }
+    } finder;
+    finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl());
+    REQUIRE(finder.found);
+    return fold::symbolic::typeTraitConstant(unit->getASTContext(), finder.found);
+}
+
+} // namespace
+
+TEST_CASE("type-trait constants are exact for complete types only", "[proved-contract][sizeof]") {
+    // sizeof was an unsupported node, which marked every `malloc(sizeof(T))`
+    // path imprecise and so could never back a Proved finding.
+    CHECK(firstTypeTrait("unsigned long f() { return sizeof(int); }") == 4u);
+    CHECK(firstTypeTrait(
+              "struct S { char c; double d; }; unsigned long f() { return sizeof(S); }") == 16u);
+    CHECK(firstTypeTrait("unsigned long f() { return alignof(double); }") == 8u);
+    // A VLA's size is a runtime value: not a constant.
+    CHECK_FALSE(firstTypeTrait("unsigned long f(int n) { char buf[n]; return sizeof(buf); }",
+                               /*c_mode=*/true)
+                    .has_value());
+}