[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements by tautschnig · Pull Request #8878 · diffblue/cbmc

tautschnig · 2026-03-17T19:05:10Z

This branch contains comprehensive improvements to CBMC's C++ front-end, covering parser, type-checker, template instantiation, GOTO conversion, and standard library model support for C++11 through C++26.

Summary of changes:

Parser: Lambdas, range-for, variadic templates, braced-init-lists, decltype, noexcept, constexpr/consteval, structured bindings, if constexpr, fold expressions, concepts, requires clauses, three-way comparison, designated initializers, coroutines, deducing this, pack indexing, contracts (pre/post)
Type-checker: Template partial specialization, SFINAE, forwarding references, implicit conversions, constexpr evaluation, access control, virtual dispatch, defaulted/deleted functions, GCC type traits builtins
Template instantiation: Variadic packs, template aliases, member templates, CTAD, concept subsumption
Library models: operator new/delete, allocator_traits, iterator, math classification functions, coroutine builtins
Infrastructure: --cpp14/--cpp17/--cpp20/--cpp23/--cpp26 flags, --stdlib option for libc++ support, <:: digraph fix, system header error suppression
Tests: 536 CORE regression tests, 1 KNOWNBUG (C++20 modules)

This branch will be split into smaller PRs for review. See CPP_SUPPORT_STATUS.md for a detailed feature matrix.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.

codecov · 2026-03-19T23:17:55Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 81.30%. Comparing base (0170409) to head (293e0bb).
⚠️ Report is 12 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8878      +/-   ##
===========================================
+ Coverage    80.41%   81.30%   +0.89%     
===========================================
  Files         1703     1705       +2     
  Lines       188398   197647    +9249     
  Branches        73       79       +6     
===========================================
+ Hits        151496   160706    +9210     
- Misses       36902    36941      +39

☔ View full report in Codecov by Sentry.
📢 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.

Add parsing support for C++11 constexpr specifier, template parameter packs (variadic templates), braced-init-list expressions, and direct parsing of C++ cast expressions (static_cast, dynamic_cast, etc.). Includes type-checker changes to handle constexpr in declarations and template pack storage. Adds regression tests for each feature. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… type traits Extend the C++ parser to handle decltype in names, noexcept/throw specifications, enum attributes, anonymous classes with base specifiers, braced-init-list after template-id, >> in empty template arguments, using declarations in statements, angle bracket disambiguation, and GCC built-in type trait keywords (__is_class, __is_enum, etc.). Also aligns parser grammar comments with the C++11 standard. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… aliases, ref-qualifiers Add parsing for noexcept specifications, ref-qualifiers on member functions, alignas in member declarations, trailing return types with abstract declarators, braced-init-list in member initializers, and template alias declarations. Includes irep_ids for new constructs and type-checker support for template alias resolution. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…xpansion, range-for, lambdas Parse defaulted/deleted member functions, final/override/alignas specifiers, _Float32/64/32x/64x types, pack expansion in braced-init- lists, decltype in base specifiers, range-based for statements, and lambda expressions. Includes type-checker support for defaulted functions and lambda closure types. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ecialization, type traits, rvalue refs Support inline namespaces in name resolution, explicit conversion operators, partial specialization matching for non-type parameters, GCC built-in type traits in expressions, rvalue references in member access and static_cast, template alias instantiation with enum args, base class member initializers for POD types, and const qualifier preservation on struct/union tag pointer subtypes. Each fix includes a regression test in regression/cpp/. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…riadic packs, GCC type transforms Fix template parameter scope resolution, void-typed typedef members in structs, pointer-to-bool and struct-to-bool implicit conversions, template specialization filtering in class member lookup, variadic template parameter packs with multiple arguments, and partial specialization matching in elaborate_class_template. Implement GCC built-in type transformations: __remove_cv, __remove_reference, __remove_cvref. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… ctors, template deduction Fix inline friend function scope, safe symbol lookup for constexpr evaluation, member typedef scope resolution, class scope visibility for friend function bodies, braced-init-list as constructor arguments, static_assert constant expression evaluation, duplicate function templates with SFINAE constraints, inline namespace using-scopes, partial explicit template arguments, delegating constructors, and template argument deduction from template type parameters. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ualified template tags, SFINAE Fix rvalue reference binding and type representation, nested template member function definitions, template argument deduction through function pointer types, default template args with empty variadic packs, empty variadic template parameter packs in function templates, qualified names as class template tags, and SFINAE error suppression during default template argument evaluation. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…, functional cast disambiguation Fix template constructor overload resolution crash, empty braced-init- list as value initialization for class types, template converting constructors in implicit conversions, rvalue vs lvalue reference distinction in overload resolution, forwarding references and reference collapsing, and functional cast ambiguity with static_cast for rvalue references. Also relaxes array type invariant in declaration type checking. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… _Float128 builtins Implement partial ordering for class template specializations. Fix template const deduction, double typechecking of member initializer operands, typedef and using alias scope resolution, template constructor resolution, extern template declarations, base class name resolution in constructor initializers, and template argument deduction across unrelated templates. Add GCC _Float128 math builtins (__builtin_*f128). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…eted ctors, linking fixes Fix constexpr handling for skip statements and initialized declarations, aggregate initialization in return statements, nested class access to enclosing class members, deleted constructor member initialization, while-loop declaration conditions, most vexing parse disambiguation, constexpr static members as array sizes, and brace-enclosed array member initialization. Also fixes linking for missing symbols in remove_internal_symbols and adds cycle detection to size_of_expr/pointer_offset_bits. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…late friends Fix most vexing parse for non-type names and overload candidate parameter count filtering. Improve GOTO conversion robustness: create missing parameter symbols, handle missing function symbols gracefully, skip functions with non-code values, handle unresolved function names and non-boolean conditions, and handle incomplete template instantiation artifacts. Also fix template friend class declarations, trailing return types in class scope, and auto type deduction for non-primitive types. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

macOS 14 CI runner is slower and needs more time for 542 tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

MSVC's <exception> header uses void* ptr = {} which requires converting an empty brace-init-list to a null pointer. Produce null_pointer_exprt instead of throwing a conversion error. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The make build on macOS uses Clang, not GCC. Detect the compiler from goto-cc --version and exclude gcc-only tests accordingly. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

- cbmc-cpp Makefile: exclude gcc-only and skip --validate-goto-model on non-GCC platforms (matching CMakeLists.txt behavior) - cpp Makefile: already fixed in previous commit - libcxx_namespace_attr: re-tag gcc-only (__attribute__ on namespace is GCC/Clang-specific syntax, not supported by MSVC) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

MSVC's <ratio> header uses a constexpr _Gcd function with a while loop. CBMC's constexpr evaluator previously gave up on any control flow. Now handles: - if/else: evaluate condition, execute the taken branch - while: bounded iteration (max 1000), evaluate condition and body Both fall back to non-constexpr on unsupported constructs. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Handle [&args...] and [args...] syntax where the ellipsis follows the identifier. Previously only [...args] (C++20 pack init-capture) was supported. Required by MSVC's <mutex> header. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Instead of relaxing access control for system headers, properly handle the case where overload resolution selects a private member: mark it as inaccessible and let the caller try other overloads. Fixes MSVC's bad_alloc(const char*) which is private but was being selected over the public default constructor. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Detect GCC by checking for 'Free Software Foundation' in gcc --version. On macOS (Apple Clang) and other non-GCC platforms, exclude gcc-only tests. Re-tag libcxx_namespace_attr as gcc-only (__attribute__ on namespace is GCC/Clang syntax). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

With fixes for <ratio> (constexpr while), <mutex> (lambda pack capture), <exception> (brace-init), char16_t, and bad_alloc, <thread> may now work on MSVC. On macOS libc++ it may still fail due to a SFINAE scope issue in iterator_traits.h. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Switch from double quotes to single quotes for the mangled function name with parentheses, matching the pattern used by jbmc tests. Remove gcc-only tag since the quoting now works cross-platform. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The test uses void* pointer arithmetic (__p++) which is a GCC extension not supported by MSVC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The parser produces empty name components before the decltype node in a qualified name. The resolver failed with 'scope not found' because it tried to look up an empty scope name. Fix: - Check ID_expr_arg (used by rVarNameCore) in addition to ID_type_arg (used by type specifier path) - Skip empty scope lookups that occur with decltype components This fixes the libc++ SFINAE pattern used in Xcode 15.4's iterator_traits.h: decltype(__test<_Tp>(nullptr))::value Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Xcode 16.4's libc++ uses __is_trivially_relocatable(_Tp) in is_trivially_relocatable.h. Add as Clang-only unary type predicate. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

When a private member is accessed from code in system headers (paths containing 'include' or 'Include'), mark as inaccessible but don't throw. This handles MSVC's bad_array_new_length calling bad_alloc(const char*) which is private. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

For multiple inheritance, virtual dispatch thunks must adjust the 'this' pointer from the base subobject to the derived class. The thunk previously used a simple typecast which doesn't adjust the pointer offset. Now computes the base class offset from the vtable pointer position and subtracts it for non-primary bases. Only non-primary bases (not the first base in the hierarchy) need adjustment. Primary bases share the same starting address as the derived class. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Handle {expr1, expr2, ...} to aggregate struct conversion by assigning initializer list elements to struct members in order. Excludes std::initializer_list types which have their own handler. Required by MSVC's <ratio> _Big_multiply: return {hi, lo}; Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

<thread> on Xcode 15.4 libc++ triggers a logic_error constructor resolution failure. This is specific to the older libc++ version and doesn't affect Xcode 16.4 (macOS 15). Increase cbmc-cpp suite timeout from 2400s to 4800s for the slow macOS 14 CI runner. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The previous detection used head -1 which missed 'Free Software Foundation' on line 2 of gcc --version output. Use grep without head to search the full output. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Each VS 2025 test suite is a separate GitHub Actions step with if: always() so we can identify which suite kills the runner. 10 steps: cpp, cbmc-cpp, cbmc, goto-instrument, goto-analyzer, contracts, unit tests, jbmc, jbmc-strings, remaining. macOS 15: only cpp and systemc regression tests. All other CI jobs disabled. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

On MSVC, valarray's complex template instantiation can cause CBMC to run indefinitely without a depth bound, killing the CI runner. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Use goto-cc --version | grep 'gcc:' instead of gcc --version to detect GCC. goto-cc outputs 'gcc: <version>' on GCC systems and 'clang: <version>' on Clang/macOS systems. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

On MSVC, __GNUC__ is not defined, so guards like '#if !defined(__GNUC__) || __GNUC__ >= 11' include the code. But MSVC doesn't support the C++23/26 features or have the same headers. Add '&& !defined(_MSC_VER)' to exclude on MSVC. Also add '!defined(_MSC_VER) &&' to __has_include guards for C++20 headers that CBMC can't fully handle on MSVC yet. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

These tests fail on MSVC due to: - _Mybase using declaration not resolved (vector iterator) - shared_ptr::operator* not resolved (template instantiation) - optional/string_view/variant not found (template chain failure) Root cause: MSVC STL uses _Mybase typedef + inheriting constructors pattern that CBMC's type-checker can't resolve yet. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

For 'using _Mybase::_Mybase' where _Mybase is a typedef for Base: 1. resolve_scope: follow typedef to class type and navigate to that class's scope 2. using handler: replace the typedef name with the actual class name so constructor lookup succeeds This is the pattern used by MSVC's STL (typedef Base _Mybase; using _Mybase::_Mybase for inheriting constructors). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The typedef-to-class scope resolution fix may resolve the _Mybase issue that caused these tests to fail on MSVC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig self-assigned this Mar 17, 2026

tautschnig force-pushed the cpp11-parser-rework-squashed branch 10 times, most recently from ab675bb to 4f0b085 Compare March 18, 2026 22:35

tautschnig force-pushed the cpp11-parser-rework-squashed branch 6 times, most recently from c5a365a to 5ae57d8 Compare March 29, 2026 20:28

tautschnig and others added 12 commits March 29, 2026 21:45

tautschnig and others added 2 commits March 29, 2026 21:45

Increase cbmc-cpp test suite timeout from 1800s to 2400s

bcaeb80

macOS 14 CI runner is slower and needs more time for 542 tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the cpp11-parser-rework-squashed branch from 5ae57d8 to e8683a9 Compare March 29, 2026 21:47

tautschnig and others added 2 commits March 30, 2026 06:13

Exclude gcc-only tests on non-GCC compilers in cpp Makefile

0076dfe

The make build on macOS uses Clang, not GCC. Detect the compiler from goto-cc --version and exclude gcc-only tests accordingly. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the cpp11-parser-rework-squashed branch from e8683a9 to 2dee770 Compare March 30, 2026 08:15

tautschnig and others added 8 commits March 30, 2026 12:14

Tag Function_Arguments1 as gcc-only (void* pointer arithmetic)

d1e4456

The test uses void* pointer arithmetic (__p++) which is a GCC extension not supported by MSVC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the cpp11-parser-rework-squashed branch from fa3e897 to 499e75a Compare March 30, 2026 16:36

tautschnig and others added 6 commits March 30, 2026 18:26

Add __is_trivially_relocatable Clang builtin

2f0236a

Xcode 16.4's libc++ uses __is_trivially_relocatable(_Tp) in is_trivially_relocatable.h. Add as Clang-only unary type predicate. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Fix Makefile gcc-only detection: search full gcc --version output

e897e48

The previous detection used head -1 which missed 'Free Software Foundation' on line 2 of gcc --version output. Use grep without head to search the full output. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the cpp11-parser-rework-squashed branch from 8f4e2d7 to f3d208e Compare March 31, 2026 08:28

tautschnig and others added 2 commits March 31, 2026 11:13

Add --depth 100 to cpp17_valarray_basic to prevent unbounded analysis

dfee254

On MSVC, valarray's complex template instantiation can cause CBMC to run indefinitely without a depth bound, killing the CI runner. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig force-pushed the cpp11-parser-rework-squashed branch from f3d208e to dfee254 Compare March 31, 2026 11:42

tautschnig and others added 5 commits March 31, 2026 14:32

Remove gcc-only from 23 MSVC tests to re-test with typedef fix

293e0bb

The typedef-to-class scope resolution fix may resolve the _Mybase issue that caused these tests to fail on MSVC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements#8878

[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements#8878
tautschnig wants to merge 131 commits intodiffblue:developfrom
tautschnig:cpp11-parser-rework-squashed

tautschnig commented Mar 17, 2026

Uh oh!

codecov bot commented Mar 19, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

tautschnig commented Mar 17, 2026

Uh oh!

codecov bot commented Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

codecov bot commented Mar 19, 2026 •

edited

Loading