Repository navigation
C++ front end tests: C++11 - #9411
Open
tautschnig wants to merge 3 commits into
Open
tautschnig wants to merge 3 commits into
tautschnig wants to merge 3 commits into
Conversation
Tests of the C++ front end depend on the standard library headers cbmc preprocesses with (the host gcc's libstdc++, libc++, or the MSVC STL) and on GNU extensions or the Itanium ABI. regression/cbmc-cpp's CMake and Makefile now exclude, according to the host: - libcxx (run, as CORE only, in a profile of its own where clang and the libc++ headers are installed), msvc-stl (only with MSVC); - libstdcxx, libstdcxx12, libstdcxx13, libstdcxx16 (when the host gcc is not GNU gcc, or older than the version), broken-libstdcxx16 (with GCC 16 or later); - gnu-extensions and itanium-abi with MSVC; gcc-only also when the build compiler is not GNU (in regression/cpp, too). CORE runs in four shards with a per-test timeout of 900 s, and without --validate-goto-model with GCC < 13. regression/README.md documents the tags. No test uses them yet: they are for the C++ tests to follow. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
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.
2 of 3 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Nov 10, 2026
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>
tautschnig
force-pushed
the
pr/cpp-tests-cpp11
branch
from
November 10, 2026 11:54
87f08e9 to
62fea6f
Compare
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Nov 10, 2026
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>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9411 +/- ##
===========================================
+ Coverage 81.02% 81.05% +0.02%
===========================================
Files 1723 1723
Lines 191314 191314
Branches 73 73
===========================================
+ Hits 155020 155060 +40
+ Misses 36294 36254 -40 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
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
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>
tautschnig
force-pushed
the
pr/cpp-tests-cpp11
branch
from
November 10, 2026 15:34
62fea6f to
9de1fea
Compare
kroening
pushed a commit
that referenced
this pull request
Nov 10, 2026
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. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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: #9407