From 087e51e27790c6680991cd8711e61c816cae6467 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 14 Oct 2026 10:02:29 +0530 Subject: [PATCH 1/3] verify: Report a function template only when it has contracts, not when nothing verified calls it. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 3387ec0793..a555d6d522 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -1864,9 +1864,12 @@ std::vector> ASTConverter::convertTranslationUnit() { ": member function verification is unsupported"); continue; } + // Only a template with contracts is reported here: one without matters + // where verified code calls it, which reports the call. if (FD->isTemplated()) { if (!FD->isInStdNamespace() && - Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation())) + Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation()) && + (functionContract(FD) || hasContractStatements(FD, Ctx))) Errors.push_back(FD->getNameAsString() + ": function template verification is unsupported"); continue; From 01411614bf0ee61a53b5abdc112e72d8b50e1418 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 14 Oct 2026 10:02:29 +0530 Subject: [PATCH 2/3] test: Check that an uncontracted template stops nothing unless verified code calls it. --- clang/test/Verify/suite/unused_template.cpp | 37 +++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 clang/test/Verify/suite/unused_template.cpp diff --git a/clang/test/Verify/suite/unused_template.cpp b/clang/test/Verify/suite/unused_template.cpp new file mode 100644 index 0000000000..820aa7100e --- /dev/null +++ b/clang/test/Verify/suite/unused_template.cpp @@ -0,0 +1,37 @@ +// RUN: %cpp-verify %s -- 2>&1 | FileCheck %s --implicit-check-not=error: +// RUN: not %cpp-verify %s -- -DCALL 2>&1 | FileCheck %s --check-prefix=CALL +// RUN: not %cpp-verify %s -- -DSTATEMENT 2>&1 | FileCheck %s --check-prefix=STATEMENT +// +// A function template without contracts is not verified, and stops nothing +// unless verified code calls it: that call is reported. One with contract +// statements is reported, as one with contracts is. + +template T twice(T v) { return v + v; } + +int inc(int x) + cppverify::pre(x < 1000) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} +// CHECK: Verified: inc [backend=z3] + +#ifdef CALL +int uses_twice(int x) + cppverify::pre(0 <= x && x <= 1000) + cppverify::post(cppverify::result == 2 * x) +{ + return twice(x); +} +#endif +// CALL: error: uses_twice: call to function without a verification contract: twice +// CALL-NOT: function template verification + +#ifdef STATEMENT +template T checked(T v) +{ + cppverify::check(true); + return v; +} +#endif +// STATEMENT: error: checked: function template verification is unsupported From 977a47535e235fde30d033448e7cd61f2ad4e4c6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 14 Oct 2026 10:02:30 +0530 Subject: [PATCH 3/3] docs: State when an uncontracted template stops verification. --- website/source/language/limitations.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 5e4f3508c2..d463751d9b 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -129,7 +129,8 @@ C++ feature boundaries reference parameters and through automatic objects, with mutual recursion among functions of one kind (spec, proof, or executable). - Member functions (their contracts are ignored with a warning), - templates, variadics, indirect calls, recursion through a function + templates (one without contracts stops nothing unless verified code + calls it), variadics, indirect calls, recursion through a function that allocates or frees storage, and general link-time summaries. * - Storage - Supported locals, constrained scalar dynamic storage, and inferred