Skip to content

use C++20 - #9156

Draft
kroening wants to merge 3 commits into
developfrom
c++20
Draft

use C++20#9156
kroening wants to merge 3 commits into
developfrom
c++20

Conversation

@kroening

Copy link
Copy Markdown
Collaborator

This bumps the build from C++17 to C++20.

  • 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.

@kroening kroening added the Build label Aug 11, 2026
@kroening
kroening force-pushed the c++20 branch 4 times, most recently from cbab6a2 to 2a7200a Compare August 11, 2026 10:31
This bumps the build from C++17 to C++20.
@codecov

codecov Bot commented Aug 11, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 71.42857% with 16 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.83%. Comparing base (0ebdc4c) to head (9e3c664).
⚠️ Report is 3 commits behind head on develop.

Files with missing lines Patch % Lines
src/util/format_expr.cpp 54.54% 5 Missing ⚠️
src/util/std_expr.cpp 33.33% 4 Missing ⚠️
src/util/bv_arithmetic.cpp 0.00% 3 Missing ⚠️
src/util/format_type.cpp 0.00% 2 Missing ⚠️
src/goto-programs/goto_trace.cpp 50.00% 1 Missing ⚠️
src/util/cmdline.cpp 50.00% 1 Missing ⚠️
Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #9156   +/-   ##
========================================
  Coverage    80.83%   80.83%           
========================================
  Files         1717     1716    -1     
  Lines       190069   190110   +41     
  Branches        73       74    +1     
========================================
+ Hits        153647   153684   +37     
- Misses       36422    36426    +4     

☔ 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.

MSVC defaults to the local codepage (cp1252) for the execution character
set. The plain string literals with \uXXXX escapes that replace the
formerly used u8 literals (which are no longer streamable in C++20) were
therefore encoded as '?', mangling all Unicode output and failing unit
and regression tests on both Windows jobs. Passing /utf-8 makes the
source and execution character sets UTF-8, restoring the previous
behaviour byte-for-byte.

CaDiCaL 3.0.0's vivify.hpp uses std::tuple without including <tuple>,
which libstdc++ 12 no longer provides transitively in C++20 mode,
breaking check-ubuntu-22_04-make-clang. Extend the CaDiCaL patch to add
the missing include.
C++20 considers reversed operands as overload candidates for == and !=.
For a non-const member operator== the reversed candidate takes a const
object and is therefore a different, ambiguous overload; clang 14
rejects such uses with -Wambiguous-reversed-operator, which broke
check-ubuntu-22_04-make-clang. Making the operators const removes the
ambiguity and is correct const-wise anyway.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant