Skip to content

verify: Report a function template only when it has contracts - #21

Merged
SwayamInSync merged 3 commits into
mainfrom
fix/unused-templates
Oct 14, 2026
Merged

SwayamInSync merged 3 commits into
mainfrom
fix/unused-templates

Conversation

@SwayamInSync

Copy link
Copy Markdown
Owner

Any function template written in the main file stopped verification of the whole file with error: twice: function template verification is unsupported, even one without contracts that no verified function calls:

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;
}

On main inc gets no verdict. A template is now reported only when it has contracts or contract statements, as member functions already are. One without them matters only where verified code calls it, and that call is already reported (call to function without a verification contract: twice).

Testing: suite/unused_template.cpp fails on main; it also checks the call from verified code and a template with a cppverify::check, which stays an error and which dropping the contract-statement test misses. Verify suite: 398 passed, 1 unsupported. A verdict differential against main over the 405 Verify sources changes only backward_compat_exhaustive.cpp, plain C++ whose uncontracted templated stopped the file on main; decode_uleb128_length_10 timed out on main under load in that run.

@SwayamInSync
SwayamInSync merged commit 165b0c6 into main Oct 14, 2026
13 of 14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant