verify: Report a function template only when it has contracts

clang/lib/Verify/Frontend/ASTConverter.cpp

@@ -1864,9 +1864,12 @@ std::vector<std::unique_ptr<VFunction>> 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;

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 <class T> 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 <class T> T checked(T v)
+{
+  cppverify::check(true);
+  return v;
+}
+#endif
+// STATEMENT: error: checked: function template verification is unsupported

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