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

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>

…dressof, libc++ compat Implement __is_convertible and __is_assignable builtin type traits. Enable argument-dependent lookup (ADL) and fix template deduction for mismatched types. Add __builtin_addressof as template function. Implement basic template template parameter support and process using declarations in class bodies. Initial libc++ compatibility: fix cv-qualifier matching, add type predicates, parse C++14 variable template usage in expressions. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ble templates, UDLs Add C++14 decltype(auto) support, auto return type deduction, relaxed constexpr functions (multiple statements), variable template parsing and instantiation, and user-defined literal operator parsing. Fix sizeof... for non-type parameter packs, deferred method body template map, named rvalue reference value category in overload resolution, and <valarray> template recursion. Includes C++11 standard library regression tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…pes, structured bindings Add --cpp14 and --cpp17 command-line flags. Parse C++17 nested namespace definitions, noexcept in function types, structured bindings (syntax), and GCC __attribute__ after noexcept. Fix out-of-class template destructors, forward-declared enums with underlying type, break/continue flags clobbered by recursive convert_function, and missing GCC type traits (__is_final, __is_aggregate, __has_unique_object_representations). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…tandard library tests Synthesize bodies for std::list support functions. Fix C++17 header parsing for deduction guides, enum redefinition, and noexcept. Store noexcept as annotation on function types for template naming. Support direct-list-initialization for non-POD types. Handle C++ structs with methods in initializer code and prevent PSTL header includes causing infinite recursion. Fix --validate-goto-model for C++ programs. Add C++11, C++14, and C++17 standard library regression tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… dispatch, assert built-in Fix forward-declared enum class definition, catch clause with reference parameter and unknown type, overload resolution fallback, char vs wchar_t template disambiguation, and qualified friend function scope entries. Provide stdlib models for iostream and fix numeric_traits init order. Fix virtual function thunk duplicate this argument, virtual dispatch crash with override and virtual destructor. Declare assert as C++ built-in and upgrade 37 KNOWNBUG tests to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…s and upgrades Lower temporary_object side effects during goto conversion. Fix inverted CHECK_RETURN for array size in default_assignop_value and conversion operator name resolution for out-of-class definitions. Replace assert built-in with #include <cassert> in regression tests. Move Templates34/36 to cpp suite. Add --cpp11 to STL tests and upgrade valarray1, iterator_basic, and 4 STL tests to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ions, copy semantics Fix overload disambiguation with derived-to-base conversions, protected member access check for derived classes, overloaded operator-> for data member access and chained calls, top-level const stripping from parameters in function identity. Fix virtual function thunk return value, virtual function dispatch for inherited vtable pointers, static template member function body typechecking, dynamic initialization order for PODs with side effects, virtual destructor dispatch for delete expressions, and base class copy constructor marking in member initializers. Resolve __builtin_FILE, __builtin_LINE, __builtin_FUNCTION at type-check time. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…lates, const resolution Restrict derived class access to protected members only. Fix multiple inheritance pointer offset adjustment, ternary type mismatch with bitfields, anonymous union member access, POD base class copy order, char vs signed char in template specialization, and operator restrictions for non-member functions. Fix pointer-to-member type mismatch in notequal conversion, allow bounded recursive template elaboration, reconcile pointer-to-member type in symex assignment, and simplify non-constant values in const symbol resolution. Move extractbits1 to systemc test suite. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…on, STL/SystemC upgrades Continue processing declarations after type-checking errors. Fix copy constructor calls for non-POD pass-by-value arguments and return values, byte_update for base-class subobject writes through cast pointers, and variadic template parameter pack expansion in function template deduction. Fix struct_tag type mismatches in function call validation, non-code initializer in cpp_new goto conversion, and missing template crash in disambiguate. Upgrade Vector1, STL1, STL2, extractbits1, and several container tests to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…das, defaulted operator== Fix template specialization lookup in instantiate_template and support SFINAE with enable_if as default template argument. Support C++20 lambda init-capture with pack expansion and expand template aliases during function template argument deduction. Support generic lambdas with non-int argument types and generate body for defaulted operator== and operator!=. Fix if constexpr with auto return type deduction and support namespace alias in block scope. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…riend constexpr, <compare> header Support C++17 binary fold expressions and fold expressions with all binary operators. Support C++17 using-declaration pack expansion and variadic lambda params. Parse complex requires clause expressions and fix C++20 parsing for STL headers. Fix friend constexpr function access to private members, handle defaulted friend operator== in class definitions, defer friend function body type-checking, and fix <compare> header support (constexpr eval, friend operator==, operator!=). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…hip with structs Fix ternary expressions in template defaults and register enum tags. Fix bitfield default member initializers and constrained partial specializations with duplicate bodies. Fix spaceship comparison with struct types. Add __builtin_strlen, __builtin_is_constant_evaluated, and brace pack init support. Add regression tests for C++20 compare header. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… if consteval runtime branch Add __builtin_memcpy, __builtin_memmove, and __builtin_strcmp library models. Support union templates and skip member template aliases during instantiation. Fix merge_type crash on empty type, skip type alias components during struct zero-initialization, return template symbol for unresolved template arguments, and fix operator() on temporary objects. Skip precondition instrumentation for functions without preconditions. Fix if consteval to take runtime (else) branch. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…old in members, GCC predicates Fix partial specialization matching with empty variadic packs and lambda in unevaluated context (decltype). Fix template method symbol collision with different return types. Expand fold expressions in class template member initializers and fix decltype to preserve reference types from function calls. Skip void-typed members during template instantiation. Add missing GCC built-in type predicates and fix template constructor default args referencing class template params. Add CORE tests for C++20/C++26 features. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ymex c_bool/bool fix Fix aggregate init bounds check for structs with type-alias components. Fix SFINAE alternative template constructor scope visibility. Strip unresolved C++ names from user function bodies instead of clearing them entirely. Fix three invariant violations: constructor, constexpr eval, and designator. Fix c_bool vs bool type mismatch in symex_assign for C++ bool semantics. Force auto return type deduction for template methods at call site. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…leak, parser fixes Implement C++20 concept subsumption ordering for function templates. Add C++23 if !consteval support. Fix template parameter scope leak in parser and parsing of decltype(expr)::member qualified names. Fix constructor_name invariant crash. Fix using enum in default member initializers and qualified non-type template parameters in C++20 mode. Add 9 CORE tests for C++20/23 features. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…t_cast, sort, accumulate Add CORE regression tests for standard library features: std::any and std::string_view (C++17), std::apply (C++17), std::to_underlying (C++23), constrained auto (C++20), std::numbers and std::bit_cast (C++20), std::chrono (C++14), std::optional/variant/tuple (C++17), std::sort (C++20 <algorithm>), and std::accumulate (C++20 <numeric>). Fix forward-referenced member variable template parsing and support standard library UDL suffixes with auto constexpr order. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ional, unreachable, erase_if Add CORE regression tests for C++17 iostream, thread, and mutex headers. Add CORE tests for C++20 std::vector, std::map, std::optional, and std::erase_if. Add C++23 optional::transform and std::unreachable tests. Add C++17 <string> header test. Fix operator""if parsing for complex UDL operators, downgrade malformed-type implicit conversion to warning, downgrade designator out-of-bounds to warning, skip unresolved out-of-class template member definitions, and fix constexpr decl_block evaluation. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…bodies Fix member function templates defined out-of-class: partially instantiate during class template member processing, fix deferred method bodies, and fix overload body swap in typecheck_class_template_ member. Strip unresolved statements from system header bodies instead of clearing them. Provide goto-level bodies for operator new/delete via __new/__delete built-ins. Add KNOWNBUG tests for initializer_list and shared_ptr gaps. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… suppression, coroutine stubs Support auto deduction for braced-init-lists (C++11 initializer_list syntax). Fix scope resolution fallback for namespaces in template scopes. Provide model for __normal_iterator::base() and promote vector test to CORE. Add try-catch for namespace items from system headers. Suppress class template not found error for system headers and fix <regex>. Fix constructor calls used as values by adding this pointer. Handle missing functions in symex gracefully (make_shared fix). Add coroutine builtin stubs and promote coroutine_types to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…r null handler Support braced-init-list in template arguments for C++20 class NTTP. Suppress system header errors with null message handler. Add comprehensive C++ standard support status document (CPP_SUPPORT_STATUS.md). Add KNOWNBUG tests for identified C++ support gaps. Simplify filesystem test and update descriptions. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… timeout Fix concept overload resolution and pack indexing in expressions. Parse qualified concept names in shorthand template syntax and fix shorthand concept constraint syntax for qualified names. Fix C++20 coroutine support: suspend_never, suspend_always, co_return built-in types and parsing. Add per-test timeout support (-t flag) to test.pl. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…ening, --stdlib option Fix namespace item source location fallback and regex_match. Fix vector push_back invariant violation and add linkage spec error recovery. Widen c_bool/bool reconciliation in symex_assign. Fix bit_cast template parameter substitution and resolve cpp_name types in typecast expressions. Add --stdlib option for selecting C++ standard library (-stdlib=libc++ support) with gcc_cmdline forwarding and preprocessor handling. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

… vector::size() bodies Fix nil type invariant in typecheck_template_args and promote 26 tests to CORE. Fix nil type in template args, use safe id_map lookups, and promote 27 more tests to CORE. Fix parser for libc++: brace-init pack expansion and post-type friend declarations. Fix __attribute__ before typedef in class body. Disable _Float keywords in C++ mode with clang preprocessor. Fix vector::size() verification by providing bodies for _S_relocate and allocator_traits::construct. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

- Brace-init in parenthesized template args (maybeTemplateArgs) - .template operator()<Args>() syntax (rVarNameCore) - __attribute__ before typedef in class body (rClassMember) - Post-type specifiers: void constexpr, bool friend (rDeclaration, rOtherDeclaration) - Bit-field brace-init defaults: int x : 1 {0} (rDeclarator) - Designated initializer brace-init: .member{expr} (rInitializeExpr) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

When using clang as preprocessor (--stdlib libc++), _Float32 etc. come as typedefs from system headers, not as built-in types. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Change catch(int) to catch(...) in all null_message_handlert swap patterns. A non-int exception could destroy the local handler while message_handler still pointed to it. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Accept TEMPLATE_SCOPE entries in id_map search and do reverse key lookup for template scopes with empty identifiers. Fixes C++20 std::sort which uses __numeric_traits_integer. Also: safe id_map lookups via find() instead of operator[]. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Produce ID_bit_cast instead of ID_typecast for __builtin_bit_cast. Handle ID_bit_cast in C++ type-checker by resolving cpp_name types. Also: handle __builtin_isfinite/isinf/isnan/isnormal as CPROVER built-in expressions. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

- _S_nothrow_relocate: return true (no exception modeling) - _S_relocate: return result + (last - first) - allocator_traits::construct: *ptr = val - _Destroy_aux::__destroy: no-op - std::isfinite/isinf/isnan/isnormal: CPROVER built-in expressions - std::dynamic_extent: (size_t)-1 built-in constant Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Handle type mismatches from brace-init designated initializers (.member{expr}) gracefully with conditional_cast instead of hard invariant. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add cpp_contract_basic test using __CPROVER_requires (C syntax). Add cpp_pre_post test for C++26 pre/post syntax. Fix chain.sh to handle both .c and .cpp file extensions. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

- Relax test patterns for GCC version compatibility - Update CPP_SUPPORT_STATUS.md with comprehensive gap documentation - Update man pages, irep_ids, unit tests - Remove duplicate test directories Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Tests that include complex STL headers require GCC 13+ libstdc++. Tag them with 'gcc-13' so they can be excluded on older platforms. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

- CMakeLists.txt: exclude gcc-13 tag when GCC < 13 or Clang - CMakeLists.txt: exclude libcxx tag on MSVC - Promote gcc_builtin_f128_math from KNOWNBUG to CORE Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Add clang, libc++-dev, libc++abi-dev to apt-get install on all Ubuntu CI runners so that libc++ regression tests can run. Remove -X libcxx exclusion from CMakeLists.txt (keep only for MSVC). Keep -X libcxx in Makefile removed since Make builds are Ubuntu-only. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

- Restore cast_expression in irep_ids.def to preserve ID numbering (fixes var_overlap2 JSON test on all platforms) - Move C_ref_qualifier to end of irep_ids.def - Tag cpp11_thread_header, cpp23_elifdef, cpp23_expected_basic, cpp23_unreachable with gcc-13 (fail on GCC 11/12) - Tag libc++ tests with gcc-13 (libc++ 14 on Ubuntu 22.04 differs) - Add gcc-13 exclusion to regression/cpp/ CMakeLists.txt - Revert gcc_builtin_f128_math to KNOWNBUG (__float128 unavailable on ARM) 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 8 times, most recently from 209fa9c to 5da59cb Compare March 18, 2026 17:23

tautschnig and others added 21 commits March 18, 2026 17:59

tautschnig and others added 15 commits March 18, 2026 18:00

tautschnig force-pushed the cpp11-parser-rework-squashed branch from 5da59cb to ab675bb Compare March 18, 2026 18:38

tautschnig and others added 12 commits March 18, 2026 22:09

Disable _Float keywords in C++ mode with clang preprocessor

448b2b9

When using clang as preprocessor (--stdlib libc++), _Float32 etc. come as typedefs from system headers, not as built-in types. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Fix use-after-free in system header error suppression

9fb5814

Change catch(int) to catch(...) in all null_message_handlert swap patterns. A non-int exception could destroy the local handler while message_handler still pointed to it. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Relax type invariant in designated initializer for brace-init

060aaf1

Handle type mismatches from brace-init designated initializers (.member{expr}) gracefully with conditional_cast instead of hard invariant. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Tag GCC-13-dependent regression tests

d3d2014

Tests that include complex STL headers require GCC 13+ libstdc++. Tag them with 'gcc-13' so they can be excluded on older platforms. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Exclude gcc-13 tests on older GCC and promote f128 math test

b84adb5

- CMakeLists.txt: exclude gcc-13 tag when GCC < 13 or Clang - CMakeLists.txt: exclude libcxx tag on MSVC - Promote gcc_builtin_f128_math from KNOWNBUG to CORE Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

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

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 55 commits intodiffblue:developfrom
tautschnig:cpp11-parser-rework-squashed

tautschnig commented Mar 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

tautschnig commented Mar 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant