Repository navigation

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

Draft

tautschnig wants to merge 3531 commits into

diffblue:developfrom

tautschnig:cpp11-parser-rework-squashed

Draft

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

This pull request is big! We're only showing the most recent 250 commits

Commits on Nov 6, 2026
- C++: cite [class.access.general]/6 where access is judged at the name
  
  tautschnig
  and
  kiro-agent
  committed
  0f07c02
- C++: a call converted on demand gets the callee's deduced return type
  
  tautschnig
  and
  kiro-agent
  committed
  7bfec24
- C++: library specializations without a definition use the primary template
  
  tautschnig
  and
  kiro-agent
  committed
  1abcedd
- C++: constant evaluation of a call statement whose value is discarded
  
  tautschnig
  and
  kiro-agent
  committed
  bce4094
- C++: a hidden friend template's declared types see the class's parameters
  
  tautschnig
  and
  kiro-agent
  committed
  a500ce2
- cpp20_range_adaptor_closure_invoked_through_invoke_impl: what is known of the cause
  
  tautschnig
  and
  kiro-agent
  committed
  ce9ab73
- Notes for round 202
  
  tautschnig
  and
  kiro-agent
  committed
  5171f21
- C++: class template argument deduction for alias templates
  
  tautschnig
  and
  kiro-agent
  committed
  0e1007b
- goto-conversion: destroy an initializer_list variable's backing array
  
  tautschnig
  and
  kiro-agent
  committed
  eaaea15
- cpp20_range_adaptor_closure_invoked_through_invoke_impl: a faithful reduction
  
  tautschnig
  and
  kiro-agent
  committed
  044fbe0
- C++: libstdc++'s std::_Destroy keeps its header body
  
  tautschnig
  and
  kiro-agent
  committed
  9bcdd85
- goto-conversion: an initializer_list backing array is a temporary
  
  tautschnig
  and
  kiro-agent
  committed
  cee87a2
- C++: model std::uncaught_exception and std::uncaught_exceptions
  
  tautschnig
  and
  kiro-agent
  committed
  fb3c2d9
- C++: define and construct the standard stream objects
  
  tautschnig
  and
  kiro-agent
  committed
  a2a1778
- goto-conversion: copy a throw's operand before stack unwinding
  
  tautschnig
  and
  kiro-agent
  committed
  d7b4ba0
- KNOWNBUG: a manipulator template inserted into two stream specializations
  
  tautschnig
  and
  kiro-agent
  committed
  b40fbf9
- remove_cpp_exceptions: a destructor run by stack unwinding runs fully
  
  tautschnig
  and
  kiro-agent
  committed
  e07faa2
- Notes for round 203
  
  tautschnig
  and
  kiro-agent
  committed
  3dc5942
- KNOWNBUG: the exception object is not copy-constructed
  
  tautschnig
  and
  kiro-agent
  committed
  27479ca
- KNOWNBUG: integer extraction from std::cin
  
  tautschnig
  and
  kiro-agent
  committed
  ba9f2a4
- KNOWNBUG: a destructor exiting via an exception during unwinding
  
  tautschnig
  and
  kiro-agent
  committed
  eaccb12
- KNOWNBUG: a write to std::cout cannot fail
  
  tautschnig
  and
  kiro-agent
  committed
  0c3e184
- KNOWNBUG: standard stream objects with the MSVC STL
  
  tautschnig
  and
  kiro-agent
  committed
  bd1caf4
- C++: call std::terminate when exception handling is abandoned
  
  tautschnig
  and
  kiro-agent
  committed
  4d092f6
- KNOWNBUG: implicit and computed exception specifications
  
  tautschnig
  and
  kiro-agent
  committed
  4351189
- C++: a write to a standard stream may fail
  
  tautschnig
  and
  kiro-agent
  committed
  4f8afa4
- C++: initialize the exception object through its constructor
  
  tautschnig
  and
  kiro-agent
  committed
  0926da8
- KNOWNBUG: the exception object is never destroyed
  
  tautschnig
  and
  kiro-agent
  committed
  b60ccc8
- Notes for round 204
  
  tautschnig
  and
  kiro-agent
  committed
  abadd51
- remove_cpp_exceptions: clear the exception before a catch(...) body
  
  tautschnig
  and
  kiro-agent
  committed
  d18e2be
- C++: implicit exception specifications of destructors and deallocation
  
  tautschnig
  and
  kiro-agent
  committed
  8456367
- C++: partial ordering of function templates with parameter packs
  
  tautschnig
  and
  kiro-agent
  committed
  3f3e518
- C++: a variable template specialization is an lvalue
  
  tautschnig
  and
  kiro-agent
  committed
  97245c0
- C++: the address of a constexpr variable
  
  tautschnig
  and
  kiro-agent
  committed
  98c2c61
- KNOWNBUG: auto variable template with a parenthesized initializer
  
  tautschnig
  and
  kiro-agent
  committed
  cacec69
- C++: evaluate noexcept(expression)
  
  tautschnig
  and
  kiro-agent
  committed
  ce92de9
- KNOWNBUG: is_nothrow_constructible with constructor arguments
  
  tautschnig
  and
  kiro-agent
  committed
  388525f
- KNOWNBUG: implicit constructors' exception specification
  
  tautschnig
  and
  kiro-agent
  committed
  2d3b42b
- C++: a member's noexcept-specifier is a complete-class context
  
  tautschnig
  and
  kiro-agent
  committed
  1b142b4
- Notes for round 205
  
  tautschnig
  and
  kiro-agent
  committed
  6848d06
- KNOWNBUG: prvalue aggregate with a base class
  
  tautschnig
  and
  kiro-agent
  committed
  bc7b686
- C++: the lifetime of the exception object
  
  tautschnig
  and
  kiro-agent
  committed
  9d6f07c
- KNOWNBUG: call result through a pack in a static member template
  
  tautschnig
  and
  kiro-agent
  committed
  913844c
- Notes for round 206
  
  tautschnig
  and
  kiro-agent
  committed
  60ddb33
- C++: a function template name as an operand of an overloaded operator
  
  tautschnig
  and
  kiro-agent
  committed
  fe3ff67
- C++: a braced prvalue of an aggregate with a base with data members
  
  tautschnig
  and
  kiro-agent
  committed
  afdaeb7
- C++: the "C" locale's num_get facet (libstdc++)
  
  tautschnig
  and
  kiro-agent
  committed
  8e21259
- cpp20_call_result_through_pack_in_static_member_template: narrowed diagnosis
  
  tautschnig
  and
  kiro-agent
  committed
  ec66793
- Notes for round 207
  
  tautschnig
  and
  kiro-agent
  committed
  c596601
- C++ front-end: keep pack expansions of other packs in a template body
  
  tautschnig
  and
  kiro-agent
  committed
  aa334cf
- C++ front-end: exception specifications of implicit constructors
  
  tautschnig
  and
  kiro-agent
  committed
  61a7128
- KNOWNBUG: implicit move constructor declared only for move-only members
  
  tautschnig
  and
  kiro-agent
  committed
  da47c28
- C++ front-end: construction vtables for nested base subobjects
  
  tautschnig
  and
  kiro-agent
  committed
  99f140a
- KNOWNBUGs: classes with a repeated polymorphic base
  
  tautschnig
  and
  kiro-agent
  committed
  395c9ce
- C++ front-end: a variable template specialization instantiated again
  
  tautschnig
  and
  kiro-agent
  committed
  906d823
- C++ front-end: dynamic initialization of instantiated variables
  
  tautschnig
  and
  kiro-agent
  committed
  7a1acd1
- C++ front-end: member noexcept-specifiers that name later members
  
  tautschnig
  and
  kiro-agent
  committed
  af53a4a
- KNOWNBUG: member noexcept-specifier naming a later member, class template
  
  tautschnig
  and
  kiro-agent
  committed
  08f679b
- Notes for round 208
  
  tautschnig
  and
  kiro-agent
  committed
  f1e8e9e
- C++ front-end: thunks are not overload candidates
  
  tautschnig
  and
  kiro-agent
  committed
  aaec495
- C++ front-end: the table of a repeated base subobject
  
  tautschnig
  and
  kiro-agent
  committed
  d2f81b4
- C++ front-end: noexcept-specifiers of class template members when needed
  
  tautschnig
  and
  kiro-agent
  committed
  a344d25
- C++ front-end: implicit move constructors for classes with movable members
  
  tautschnig
  and
  kiro-agent
  committed
  2d60338
- C++ front-end: dynamic_cast to a pointer to void
  
  tautschnig
  and
  kiro-agent
  committed
  cc1f3ca
- C++: delete through a pointer to a polymorphic base deallocates the object
  
  tautschnig
  and
  kiro-agent
  committed
  49850b9
- KNOWNBUG: overrider reached through a virtual base's table in a derived object
  
  tautschnig
  and
  kiro-agent
  committed
  cbc5602
- Notes for round 209
  
  tautschnig
  and
  kiro-agent
  committed
  8424920
- C++ front-end: no implicit move constructor for a deleted member move
  
  tautschnig
  and
  kiro-agent
  committed
  3618005
- KNOWNBUGs: gaps found auditing the known limitations
  
  tautschnig
  and
  kiro-agent
  committed
  18c316c
- KNOWNBUGs: <chrono> and <format> body drops with libstdc++ 16.2.0
  
  tautschnig
  and
  kiro-agent
  committed
  4c081e6
- KNOWNBUG: integer insertion into a stream with the MSVC STL
  
  tautschnig
  and
  kiro-agent
  committed
  f5bba99
- Notes for round 209: audit of known gaps
  
  tautschnig
  and
  kiro-agent
  committed
  079ecca
- C++: delete with an operand with side effects deallocates the object
  
  tautschnig
  and
  kiro-agent
  committed
  e6e39a2
- C++ front-end: is_nothrow_constructible of a reference binding
  
  tautschnig
  and
  kiro-agent
  committed
  38ccb88
- C++ front-end: function pointer conversions and noexcept
  
  tautschnig
  and
  kiro-agent
  committed
  983b08a
- C library: keep the contracts library under the string literal limit
  
  tautschnig
  and
  kiro-agent
  committed
  5980a89
- C++ front-end: vcall offsets for thunks entered through a virtual base
  
  tautschnig
  and
  kiro-agent
  committed
  5e46060
- C++ front-end: constant evaluation of calls on local objects
  
  tautschnig
  and
  kiro-agent
  committed
  c462bc1
- C++ front-end: designated initializers for members of class type
  
  tautschnig
  and
  kiro-agent
  committed
  193fa7e
- C++: terminate and set_terminate of the MSVC runtime
  
  tautschnig
  and
  kiro-agent
  committed
  7568c87
- cbmc-cpp: tags for the tests that fail with the MSVC STL
  
  tautschnig
  and
  kiro-agent
  committed
  6022401
- KNOWNBUG: istringstream from a string and an allocator with the MSVC STL
  
  tautschnig
  and
  kiro-agent
  committed
  213859c
- C++ front-end: constant evaluation of __builtin_memcmp
  
  tautschnig
  and
  kiro-agent
  committed
  0ad2b61
- Notes for round 210: CI of d5afeb79ad and round 209's KNOWNBUGs
  
  tautschnig
  and
  kiro-agent
  committed
  0299273
- C++ front end: correct N5008 citations in comments
  
  tautschnig
  and
  kiro-agent
  committed
  ccbf9fe
- Regression tests: correct N5008 citations
  
  tautschnig
  and
  kiro-agent
  committed
  f4c64b1
- Documentation: correct N5008 citations and section numbers
  
  tautschnig
  and
  kiro-agent
  committed
  e3cc6e7
- Notes: correct N5008 citations
  
  tautschnig
  and
  kiro-agent
  committed
  54bebc6
- Notes for round 211: audit of the N5008 citations
  
  tautschnig
  and
  kiro-agent
  committed
  a2f9c55
- C++ front end: drop two includes that include-what-you-use flags
  
  tautschnig
  and
  kiro-agent
  committed
  7c1ed80
- C library: record why malloc sets __CPROVER_new_object, and its cost
  
  tautschnig
  and
  kiro-agent
  committed
  768bcdf
- C++ front end: default arguments of a base constructor before the flag
  
  tautschnig
  and
  kiro-agent
  committed
  ec9190a
- C++ front end: dynamic_cast of an operand with side effects
  
  tautschnig
  and
  kiro-agent
  committed
  e1b750f
- C++: models of std::exception_ptr
  
  tautschnig
  and
  kiro-agent
  committed
  822e898
- Notes for round 212: CI jobs, the MSVC istringstream, exception_ptr
  
  tautschnig
  and
  kiro-agent
  committed
  55b1482
- C++ front end: fold expressions in alias templates
  
  tautschnig
  and
  kiro-agent
  committed
  64b01ba
- C++ front end: a recursion that keeps an argument is not runaway
  
  tautschnig
  and
  kiro-agent
  committed
  f0d4f1a
- C++ front end: Clang's __builtin_invoke
  
  tautschnig
  and
  kiro-agent
  committed
  9642a44
- C++ front end: noexcept of a class template member not evaluated early
  
  tautschnig
  and
  kiro-agent
  committed
  b9192d8
- C++ front end: comma expressions and __builtin_strlen in constexpr calls
  
  tautschnig
  and
  kiro-agent
  committed
  d3c62bc
- C++ front end: constexpr objects whose initializers were converted
  
  tautschnig
  and
  kiro-agent
  committed
  1fa563f
- KNOWNBUG: string_view comparison in a constant expression with libc++
  
  tautschnig
  and
  kiro-agent
  committed
  d9c2b04
- C++ front end: destructor names of classes with function type arguments
  
  tautschnig
  and
  kiro-agent
  committed
  47a9d3a
- Field sensitivity: read a union through its widest member at any offset
  
  tautschnig
  and
  kiro-agent
  committed
  0796c4a
- C++ front end: a one-class pack expanded in a member's function type
  
  tautschnig
  and
  kiro-agent
  committed
  e405d65
- C++ front end: parenthesized aggregate initialization of a union
  
  tautschnig
  and
  kiro-agent
  committed
  ead80fa
- C++ front end: assigning an empty class object stores nothing
  
  tautschnig
  and
  kiro-agent
  committed
  15cdfd4
- C++ front end: zero-sized empty [[no_unique_address]] members
  
  tautschnig
  and
  kiro-agent
  committed
  3ea228e
- C++ front end: [[no_unique_address]] placement, destructors, FUTURE tests
  
  tautschnig
  and
  kiro-agent
  committed
  2145140
- Simplify relations of pointers to distinct objects to false
  
  tautschnig
  and
  kiro-agent
  committed
  50b813c
- C library: models of strtol_l, strtoul_l, strtoll_l and strtoull_l
  
  tautschnig
  and
  kiro-agent
  committed
  71d47ac
- C++ front end: models of libc++'s integer extraction (num_get)
  
  tautschnig
  and
  kiro-agent
  committed
  4f2f6d8
- C library: exact integer conversions in the model of vsnprintf
  
  tautschnig
  and
  kiro-agent
  committed
  d41746f
- C library: localeconv returns the "C" locale's values
  
  tautschnig
  and
  kiro-agent
  committed
  8db3d6b
- C library: model of uselocale
  
  tautschnig
  and
  kiro-agent
  committed
  d8040a0
- C++ front end: models of libc++'s integer insertion (num_put)
  
  tautschnig
  and
  kiro-agent
  committed
  6b98b10
- C++ front end: models of the MSVC runtime's manipulators and locale info
  
  tautschnig
  and
  kiro-agent
  committed
  5cef985
- Documentation: escape `#nua_type' in a doc comment
  
  tautschnig
  and
  kiro-agent
  committed
  b744f52
- Regression test: union_byte_array_holding_function_pointer is no-new-smt
  
  tautschnig
  and
  kiro-agent
  committed
  62d46fc
- C++ front end: classes whose only member is an empty [[no_unique_address]]
  
  tautschnig
  and
  kiro-agent
  committed
  f11d718
- Notes: round 213
  
  tautschnig
  and
  kiro-agent
  committed
  3b837bd
- Simplify an integer cast to a pointer and read back as that integer
  
  tautschnig
  and
  kiro-agent
  committed
  bdf1ed9
- C++ front end: the MSVC STL's locale-name copies succeed; MSVC stream tests
  
  tautschnig
  and
  kiro-agent
  committed
  f39f841
- C++ front end: constexpr class arguments copied by a copy constructor
  
  tautschnig
  and
  kiro-agent
  committed
  51e0515
- C++ front end: model of libc++'s num_get stage 2 for integers
  
  tautschnig
  and
  kiro-agent
  committed
  fba25b5
- Notes: round 214
  
  tautschnig
  and
  kiro-agent
  committed
  d59e4c6
- CI: the GCC 16 cbmc-cpp job excludes msvc-stl tests
  
  tautschnig
  and
  kiro-agent
  committed
  648c2fa
- Regression: the locale_t library tests are unix-only
  
  tautschnig
  and
  kiro-agent
  committed
  74a69a5
- Simplifier: read back an integer cast to a pointer only as its own type
  
  tautschnig
  and
  kiro-agent
  committed
  a09bbb8
- Symex: pass a struct argument to a parameter of a layout-compatible type
  
  tautschnig
  and
  kiro-agent
  committed
  98d4342
- Regression: [[no_unique_address]] layout tests are itanium-abi
  
  tautschnig
  and
  kiro-agent
  committed
  1589a39
- Linking: rename a conflicting typedef with a $link suffix
  
  tautschnig
  and
  kiro-agent
  committed
  8c234e3
- C++ front end: models of the MSVC runtime's _Getctype and _Mbrtowc
  
  tautschnig
  and
  kiro-agent
  committed
  253ce93
- C front end: Darwin's underscore asm label names the function itself
  
  tautschnig
  and
  kiro-agent
  committed
  7bba18f
- Regression: cpp11_stringstream_integer_insertion_msvc needs --object-bits 12
  
  tautschnig
  and
  kiro-agent
  committed
  f67bae6
- Notes: round 215
  
  tautschnig
  and
  kiro-agent
  committed
  9e25d1e
- Regression: MSVC stream tests with the VS 2022 STL
  
  tautschnig
  and
  kiro-agent
  committed
  bfd3401
- Regression: clang-format the two new tests' sources
  
  tautschnig
  and
  kiro-agent
  committed
  9d4bea1
- Regression: _strftime declares the function it calls on macOS too
  
  tautschnig
  and
  kiro-agent
  committed
  e7a15b0
- Notes: round 216
  
  tautschnig
  and
  kiro-agent
  committed
  fad9b3c
- C++ front end: the MSVC runtime's exception copy succeeds
  
  tautschnig
  and
  kiro-agent
  committed
  dfd9c85
- Notes: round 217
  
  tautschnig
  and
  kiro-agent
  committed
  e3112c5
- C++ front end: array and function operands of a conditional expression
  
  tautschnig
  and
  kiro-agent
  committed
  12dee67
- Regression: clang-format cpp11_msvc_exception_copy_of_copy
  
  tautschnig
  and
  kiro-agent
  committed
  9f3be3b
- Notes: round 217, conditional expressions
  
  tautschnig
  and
  kiro-agent
  committed
  9f90aa9
- Regression: a read that symex cannot resolve after a callee's malloc
  
  tautschnig
  and
  kiro-agent
  committed
  c33b153
- Print __CPROVER_fma before its rounding mode is added; dump-c includes math.h
  
  tautschnig
  and
  kiro-agent
  committed
  9f9dcbf
- Calls whose linked definition returns a floating-point value as int
  
  tautschnig
  and
  kiro-agent
  committed
  79b789e
- Regression: descs of ten CORE tests still read as KNOWNBUG
  
  tautschnig
  and
  kiro-agent
  committed
  c81ffda
- Regression: explain the coroutine KNOWNBUG
  
  tautschnig
  and
  kiro-agent
  committed
  35c9d61
- C library models preprocessed on another host: --dump-c-library-models
  
  tautschnig
  and
  kiro-agent
  committed
  009fce6
- Notes: round 218
  
  tautschnig
  and
  kiro-agent
  committed
  861ce91
- Regression: C++11 to C++26 language support census, 66 probes
  
  tautschnig
  and
  kiro-agent
  committed
  c458181
- Regression: tests of C++26's larger features
  
  tautschnig
  and
  kiro-agent
  committed
  30f7c24
- Regression: modules probe of the support census (KNOWNBUG)
  
  tautschnig
  and
  kiro-agent
  committed
  265291b
- Notes: round 219
  
  tautschnig
  and
  kiro-agent
  committed
  5dc43ae
- Regression: an unevaluated static_assert, and GCC 16's saturating_add
  
  tautschnig
  and
  kiro-agent
  committed
  a11cb41
- C++ front end: closure members of class type are constructed
  
  tautschnig
  and
  kiro-agent
  committed
  bed492f
- C++ front end: models of std::thread's start, join and detach
  
  tautschnig
  and
  kiro-agent
  committed
  b31a9cd
- C++ front end: report coroutines as unsupported
  
  tautschnig
  and
  kiro-agent
  committed
  282ff32
- C++ front end: class template argument deduction with std::vector's guides
  
  tautschnig
  and
  kiro-agent
  committed
  0907430
- C++ front end: both branches of if consteval
  
  tautschnig
  and
  kiro-agent
  committed
  b26296c
- C++ front end: a defaulted operator<=> declares operator==
  
  tautschnig
  and
  kiro-agent
  committed
  093f784
- Regression: cpp17_probe_std_variant needs libstdc++ 12
  
  tautschnig
  and
  kiro-agent
  committed
  9423008
- Notes: round 220
  
  tautschnig
  and
  kiro-agent
  committed
  3f4b82d
- Regression: partial specialization with an empty nested pack (KNOWNBUG)
  
  tautschnig
  and
  kiro-agent
  committed
  e55a40b
- C++ front end: partial specializations with an empty nested pack
  
  tautschnig
  and
  kiro-agent
  committed
  e9f204a
- C++ front end: pack expansions in a subscript
  
  tautschnig
  and
  kiro-agent
  committed
  8f106ed
- C++ front end: built-in operators beat a converting non-member
  
  tautschnig
  and
  kiro-agent
  committed
  f544793
- C front end: preprocess C++26 with -std=gnu++2c on GCC 14 and later
  
  tautschnig
  and
  kiro-agent
  committed
  abfef6f
- C++ front end: check C++26 contract assertions
  
  tautschnig
  and
  kiro-agent
  committed
  dfc7a39
- C++ front end: a structured binding declaration as a condition
  
  tautschnig
  and
  kiro-agent
  committed
  0357162
- C++ front end: friend-type-specifier lists and pack expansions
  
  tautschnig
  and
  kiro-agent
  committed
  89c97b2
- C++ front end: models of <debugging>
  
  tautschnig
  and
  kiro-agent
  committed
  56b83e8
- C++ front end: constant evaluation of throw and try
  
  tautschnig
  and
  kiro-agent
  committed
  0c1b1fe
- C++ front end: constant evaluation of placement new
  
  tautschnig
  and
  kiro-agent
  committed
  55da2f3
- C++ front end: models for std::print and system_error
  
  tautschnig
  and
  kiro-agent
  committed
  6533106
- Notes: round 221
  
  tautschnig
  and
  kiro-agent
  committed
  e66478f
- Format with clang-format 18.1.8
  
  tautschnig
  and
  kiro-agent
  committed
  34e83eb
- Doxygen: markup that doxygen 1.15 accepts
  
  tautschnig
  and
  kiro-agent
  committed
  0e63f45
- Notes: round 222
  
  tautschnig
  and
  kiro-agent
  committed
  58f2922
- C library models: file names any file system accepts
  
  tautschnig
  and
  kiro-agent
  committed
  c3fae99
- Regression: cpp11_partial_specialization_trailing_pack_empty without __int128
  
  tautschnig
  and
  kiro-agent
  committed
  7016e44
- Regression: cbmc-library-models leaves no directory behind
  
  tautschnig
  and
  kiro-agent
  committed
  711fa7a
- C++ front end: a cast from a pointer to a const array keeps constness
  
  tautschnig
  and
  kiro-agent
  committed
  ec0fe09
- Regression: cpp26_saturating_arithmetic_gcc16 with either names
  
  tautschnig
  and
  kiro-agent
  committed
  b320456
- C library models: doc comment doxygen 1.15 accepts
  
  tautschnig
  and
  kiro-agent
  committed
  9d8d22d
Commits on Nov 7, 2026
- C++ front end: models of libstdc++'s __throw_X helpers
  
  tautschnig
  and
  kiro-agent
  committed
  6f0b186
- clang-format: Standard c++20
  
  tautschnig
  and
  kiro-agent
  committed
  84a5cd8
- Notes: round 223
  
  tautschnig
  and
  kiro-agent
  committed
  e80580f
- Check C++26 postconditions of class and reference results
  
  tautschnig
  and
  kiro-agent
  committed
  464cdb3
- Notes: round 224
  
  tautschnig
  and
  kiro-agent
  committed
  308dfbc
Commits on Nov 9, 2026
- link_to_library: no linking for a function without library symbols
  
  tautschnig
  and
  kiro-agent
  committed
  485685e
- Notes: round 225
  
  tautschnig
  and
  kiro-agent
  committed
  883a9c0
- C++ front end: reuse alias and variable template instances
  
  tautschnig
  and
  kiro-agent
  committed
  455f4b6
- C++ front end: rescan only changed values for held-back bodies
  
  tautschnig
  and
  kiro-agent
  committed
  1bbb11b
- Notes: round 226
  
  tautschnig
  and
  kiro-agent
  committed
  1f440f8
- C library: memcpy/memmove preconditions without a constant `0 ||'
  
  tautschnig
  and
  kiro-agent
  committed
  762804c
- Notes: round 227
  
  tautschnig
  and
  kiro-agent
  committed
  e073228
- C library: malloc records __CPROVER_new_object only for C++ programs
  
  tautschnig
  and
  kiro-agent
  committed
  38ec620
- goto_check_c: no guards from constant operands of ||, && and ?:
  
  tautschnig
  and
  kiro-agent
  committed
  815179f
Commits on Nov 10, 2026
- C++ front end: rescan only changed bodies for deferred members
  
  tautschnig
  and
  kiro-agent
  committed
  ce86b48
- Notes: round 228
  
  tautschnig
  and
  kiro-agent
  committed
  62803b6
- Notes: round 229, and a script listing what is not upstreamed yet
  
  tautschnig
  and
  kiro-agent
  committed
  0898891
- Unit test: the simplifier folds the difference of a pointer and itself
  
  tautschnig
  and
  kiro-agent
  committed
  8c7b0b7
- Remove the GCC 16 -Warray-bounds pragmas again
  
  tautschnig
  and
  kiro-agent
  committed
  252d9c9
- gcc_builtin_library_functions: test only functions with a model on develop
  
  tautschnig
  and
  kiro-agent
  committed
  b25bf1f
- C library: no models of __builtin_memcmp, __builtin_strcmp, __builtin_strlen, __builtin_memchr
  
  tautschnig
  and
  kiro-agent
  committed
  da1f26f
- Math library models: add missing *BSD variants, cleanup
  
  tautschnig
  and
  kiro-agent
  committed
  806dcb0
- C library: no models of __builtin_isfinite{,f,l}
  
  tautschnig
  and
  kiro-agent
  committed
  d2e5a8d
- C++ front end: constant evaluation of calls with arguments for the ellipsis
  
  tautschnig
  and
  kiro-agent
  committed
  fd276fb
- C++ parser: __builtin_va_arg
  
  tautschnig
  and
  kiro-agent
  committed
  534f197
Commits on Nov 11, 2026
- C++ front end: a class returned by value has its destructor instantiated
  
  tautschnig
  and
  kiro-agent
  committed
  8eeae6f
- C++ front end: out-of-class destructors of nested classes of templates
  
  tautschnig
  and
  kiro-agent
  committed
  3077475
- C++ front end: a conversion to a bit-field type has that type
  
  tautschnig
  and
  kiro-agent
  committed
  079c184
- Keep a class's destructor with the class; no stubs for missing functions
  
  tautschnig
  and
  kiro-agent
  committed
  70d7eb0
- Solvers: no casts for equalities of operands of different types
  
  tautschnig
  and
  kiro-agent
  committed
  a114e1c
- fatal_assertions: a called function is in the goto program
  
  tautschnig
  and
  kiro-agent
  committed
  e8f7005
- goto conversion: a static assertion that reaches it holds again
  
  tautschnig
  and
  kiro-agent
  committed
  85ebe57
- Notes: round 230
  
  tautschnig
  and
  kiro-agent
  committed
  bbf255f
- va_start: the variadic arguments follow the last named parameter
  
  tautschnig
  and
  kiro-agent
  committed
  a97a417
- Goto conversion: the floating-point comparison macros are relations
  
  tautschnig
  and
  kiro-agent
  committed
  36c8cd5
- C++ front end: a constexpr object with a deduced class type is an object
  
  tautschnig
  and
  kiro-agent
  committed
  f2cf0ce
- C++ front end: constexpr functions are recorded as such, not as macros
  
  tautschnig
  and
  kiro-agent
  committed
  a7a2174
- Parameters of a function without a body have no identifiers
  
  tautschnig
  and
  kiro-agent
  committed
  46e1669
- C++ front end: no library model for members of a function's local classes
  
  tautschnig
  and
  kiro-agent
  committed
  8bcd5fe
- Remove fallbacks that no program reaches
  
  tautschnig
  and
  kiro-agent
  committed
  f908aaf
- builtin_functions.cpp: no symbol_table_base.h
  
  tautschnig
  and
  kiro-agent
  committed
  3252448
- Notes: round 231
  
  tautschnig
  and
  kiro-agent
  committed
  957210d
- C++ front end: unnamed template parameters shadow nothing
  
  tautschnig
  and
  kiro-agent
  committed
  a7a9d4b
- C++ front end: no int lowering of three-way comparisons
  
  tautschnig
  and
  kiro-agent
  committed
  52d1061
- C++ front end: libstdc++'s __throw_X throws when X is not declared
  
  tautschnig
  and
  kiro-agent
  committed
  c23ed1f
- C++ front end: probing a callee's parameter types does not odr-use it
  
  tautschnig
  and
  kiro-agent
  committed
  362fe62
- C++ front end: __is_nothrow_invocable checks that the call cannot throw
  
  tautschnig
  and
  kiro-agent
  committed
  052d410
- C++ parser: _Float16 for the macOS target, not the macOS host
  
  tautschnig
  and
  kiro-agent
  committed
  f7de0ca
- C++ front end: remove the system-header suppressions no program reaches
  
  tautschnig
  and
  kiro-agent
  committed
  40f0866
- Notes: round 232
  
  tautschnig
  and
  kiro-agent
  committed
  93a1d59
- C++ front end: the underlying type of an unscoped enum without enum-base
  
  tautschnig
  and
  kiro-agent
  committed
  f669e3f
- C++ front end: a friend declaration does not instantiate the class
  
  tautschnig
  and
  kiro-agent
  committed
  531f0ed
- C++ front end: the constraints of an alias template are checked
  
  tautschnig
  and
  kiro-agent
  committed
  2a1979f
- C++ front end: `m({...})' for an aggregate member is not `m(...)'
  
  tautschnig
  and
  kiro-agent
  committed
  b74a412
- C++ front end: a designated-initializer-list binds a reference
  
  tautschnig
  and
  kiro-agent
  committed
  e6d4510
- C++ front end: default arguments of instantiated member templates
  
  tautschnig
  and
  kiro-agent
  committed
  6fa9a68
Commits on Nov 12, 2026
- expr2cpp: a C++ lambda-expression is not a mathematical lambda
  
  tautschnig
  and
  kiro-agent
  committed
  a3ac16e
- C++ front end: a failed static_assert in an instantiation is an error
  
  tautschnig
  and
  kiro-agent
  committed
  a8a2105
- C++ front end: direct-initialization by a converting constructor template
  
  tautschnig
  and
  kiro-agent
  committed
  783faa2
- C library: models of wcslen, wmem* and wcsto{l,ul,ll,ull}
  
  tautschnig
  and
  kiro-agent
  committed
  a8fd285
- C++ front end: libc++'s sto* of a wstring
  
  tautschnig
  and
  kiro-agent
  committed
  ff83618
- enum_promotion_type: comments that Doxygen reads as intended
  
  tautschnig
  and
  kiro-agent
  committed
  378c371
- Notes: round 233
  
  tautschnig
  and
  kiro-agent
  committed
  721d63e

Commits

Commits on Nov 6, 2026