Skip to content

clang-format: Standard c++20 - #9414

Merged
kroening merged 1 commit into
diffblue:developfrom
tautschnig:pr/clang-format-cpp20
Nov 10, 2026
Merged

kroening merged 1 commit into
diffblue:developfrom
tautschnig:pr/clang-format-cpp20

Conversation

@tautschnig

Copy link
Copy Markdown
Collaborator

In C++17 mode clang-format splits <=>' into <= >' (which does not compile) and does not know requires-clauses and compound requirements. The C++ front end tests (#9411, #9412) are formatted as clang-format 18.1.8 does in C++20 mode. CI checks only the lines a pull request changes (git-clang-format), so existing code is not reformatted.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

In C++17 mode clang-format splits `<=>' into `<= >' (which does not
compile) and does not know requires-clauses and compound requirements.
The C++ front end tests (diffblue#9411, diffblue#9412) are formatted as clang-format
18.1.8 does in C++20 mode.  CI checks only the lines a pull request
changes (git-clang-format), so existing code is not reformatted.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Copilot AI balanced review requested due to automatic review settings November 10, 2026 11:52

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota. Try requesting a review at a lower effort level.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.

tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (312 test directories in
regression/cbmc-cpp), as written for the reworked front end.  Each ends
with an assertion that must fail and requires `** 1 of N failed', so
that a test that does not type-check fails.  None of the 340 test
descriptions passes with the current front end, so all are KNOWNBUG;
they become CORE as the changes they test are merged.  Tests that need
particular headers or compilers carry the tags of regression/README.md.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (81 test directories in regression/cbmc-cpp),
as written for the reworked front end.  Each ends with an assertion that
must fail and requires `** 1 of N failed', so that a test that does not
type-check fails.  None of the 83 test descriptions passes with the
current front end, so all are KNOWNBUG; they become CORE as the changes
they test are merged.  Tests that need particular headers or compilers
carry the tags of regression/README.md.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (961 test directories in
regression/cbmc-cpp), as written for the reworked front end.  Each ends
with an assertion that must fail and requires `** 1 of N failed', so
that a test that does not type-check fails.  Of the 1044 test
descriptions, the 46 that pass with the current front end are CORE and
the other 998 are KNOWNBUG; they become CORE as the changes they test
are merged.  Tests that need particular headers or compilers carry the
tags of regression/README.md.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (322 test directories in
regression/cbmc-cpp), as written for the reworked front end.  Each ends
with an assertion that must fail and requires `** 1 of N failed', so
that a test that does not type-check fails.  None of the 353 test
descriptions passes with the current front end, so all are KNOWNBUG;
they become CORE as the changes they test are merged.  Tests that need
particular headers or compilers carry the tags of regression/README.md.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (297 test directories in regression/cbmc-cpp
and regression/cpp), as written for the reworked front end.  Each ends
with an assertion that must fail and requires `** 1 of N failed', so
that a test that does not type-check fails.  Of the 319 test
descriptions, the 38 that pass with the current front end are CORE and
the other 281 are KNOWNBUG; they become CORE as the changes they test
are merged.  Tests that need particular headers or compilers carry the
tags of regression/README.md.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (78 test directories in regression/cbmc-cpp),
as written for the reworked front end.  Each ends with an assertion that
must fail and requires `** 1 of N failed', so that a test that does not
type-check fails.  None of the 80 test descriptions passes with the
current front end, so all are KNOWNBUG; they become CORE as the changes
they test are merged.  Tests that need particular headers or compilers
carry the tags of regression/README.md.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
@codecov

codecov Bot commented Nov 10, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 81.02%. Comparing base (826c1c7) to head (1121c54).

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #9414      +/-   ##
===========================================
- Coverage    81.02%   81.02%   -0.01%     
===========================================
  Files         1723     1723              
  Lines       191314   191314              
  Branches        73       73              
===========================================
- Hits        155020   155017       -3     
- Misses       36294    36297       +3     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (955 test directories in
regression/cbmc-cpp), as written for the reworked front end.  Each ends
with an assertion that must fail and requires `** 1 of N failed', so
that a test that does not type-check fails.  Of the 1037 test
descriptions, the 39 that pass with the current front end are CORE and
the other 998 are KNOWNBUG; they become CORE as the changes they test
are merged.  Tests that need particular headers or compilers carry the
tags of regression/README.md.  Not included, although written for the
reworked front end too: cpp11_cstring_verify, cpp11_limits_verify,
cpp11_cv_qualified_member_overload_through_base,
cpp11_derived_to_base_class_parameter_is_conversion_rank,
cpp11_integral_promotion_target_of_same_width,
cpp11_reinterpret_cast_ref, as they pass with the current front end on
Linux with GCC 13 but fail on macOS, Windows, 32-bit or with GCC 14;
each comes with the change that makes it pass on every platform.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Nov 10, 2026
Tests of the C++ front end (296 test directories in regression/cbmc-cpp
and regression/cpp), as written for the reworked front end.  Each ends
with an assertion that must fail and requires `** 1 of N failed', so
that a test that does not type-check fails.  Of the 318 test
descriptions, the 37 that pass with the current front end are CORE and
the other 281 are KNOWNBUG; they become CORE as the changes they test
are merged.  Tests that need particular headers or compilers carry the
tags of regression/README.md.  Not included, although written for the
reworked front end too: braced_mem_init1, as it fails with Visual Studio
(goto-cc in cl mode rejects the braced mem-initializer); each comes with
the change that makes it pass on every platform.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Depends-on: diffblue#9407
Depends-on: diffblue#9414
@kroening
kroening merged commit 107a1e5 into diffblue:develop Nov 10, 2026
38 of 43 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.

3 participants