Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3353 commits
Select commit Hold shift + click to select a range
9784795
C++: expand a compound-type pack pattern in a substituted template ar…
tautschnig Oct 18, 2026
9bf3076
C++ library models: libc++'s std::to_string for integers
tautschnig Oct 18, 2026
4117de1
C++ constexpr: a const integral variable is usable in constant expres…
tautschnig Oct 18, 2026
8986223
C++: initializing an empty base subobject stores nothing
tautschnig Oct 18, 2026
5a9b7b6
cbmc-cpp: cpp11_std_bind_invocable_traits_first needs libstdc++
tautschnig Oct 18, 2026
4253366
C++ parser: a non-type template parameter pack of pointer or referenc…
tautschnig Oct 18, 2026
d067ca8
C++: a class with a constructor template is not an aggregate
tautschnig Oct 18, 2026
5131b68
C++: [over.best.ics]/4.5 for return {{...}}
tautschnig Oct 18, 2026
c555d65
C++ library models: libc++'s std::stoi to std::stoull
tautschnig Oct 18, 2026
1157656
cbmc-cpp: tag ten more tests gnu-extensions
tautschnig Oct 18, 2026
7fb2ea8
cbmc-cpp: run cpp98_dynamic_cast_reference_throws_bad_cast as C++11
tautschnig Oct 18, 2026
07b365b
C++ parser: a type-constraint qualified from the global namespace
tautschnig Oct 18, 2026
5510d5c
C++: match a member template's out-of-line definition by signature first
tautschnig Oct 18, 2026
72ab8e5
Notes: round 190
tautschnig Oct 18, 2026
58a3aff
C++: name the parameters of a this-adjusting virtual thunk
tautschnig Oct 18, 2026
9fddf28
C++: the injected-class-name in an out-of-class member definition
tautschnig Oct 18, 2026
a50c435
C++: a member template's definition is not a same-arity member's
tautschnig Oct 18, 2026
13893b0
C++: assignment operator templates of a POD class
tautschnig Oct 18, 2026
49a2566
C++: a trailing non-type pack not otherwise deduced is empty
tautschnig Oct 18, 2026
40b7267
C++: a redeclared deduced return type under a reference declarator
tautschnig Oct 18, 2026
623e1bd
C++: no built-in comparison of class-type operands
tautschnig Oct 19, 2026
74d2154
Notes: round 191
tautschnig Oct 19, 2026
d58a9f8
C++: a hidden friend template is found only by argument-dependent lookup
tautschnig Oct 19, 2026
e55ad9e
C++: prefer a member template definition only among its own class's
tautschnig Oct 19, 2026
7fd9344
Value sets: find a field-sensitive member read through a member expre…
tautschnig Oct 19, 2026
b479c34
cbmc-cpp: KNOWNBUG for a template lambda with a reference parameter
tautschnig Oct 19, 2026
d45112f
Notes: round 192
tautschnig Oct 19, 2026
a85007d
cbmc-cpp: spell the size type portably in two tests
tautschnig Oct 19, 2026
e238295
Visual Studio layout: align a base subobject, not its members
tautschnig Oct 19, 2026
28de194
cbmc-cpp: do not assume a 4-byte wchar_t
tautschnig Oct 19, 2026
1824591
cbmc-cpp: do not assume a 32-bit wchar_t in a concepts test
tautschnig Oct 19, 2026
eaa5e67
C++: list-initialization of an enumeration with a fixed underlying type
tautschnig Oct 19, 2026
c40ab5b
C++: explicit specializations of array variable templates
tautschnig Oct 19, 2026
3625626
C++: an explicit specialization of a variable template is not a parti…
tautschnig Oct 19, 2026
edbfda6
C++ overload resolution: compare reference bindings before preferring…
tautschnig Oct 19, 2026
5abd30e
C++: a hidden friend template's parameter types may name the enclosin…
tautschnig Oct 19, 2026
de0394f
C++ deduction: a compound pack pattern deduces the pack's elements fr…
tautschnig Oct 19, 2026
771c9f1
C++ deduction: expand the enclosing class's packs in a member templat…
tautschnig Oct 19, 2026
b25fafa
C++ deduction: a function template's own packs hide same-named contex…
tautschnig Oct 19, 2026
39b4db1
C++: expand call-argument packs in a decltype nested-name-specifier
tautschnig Oct 19, 2026
53547b8
C++: complete a class template's static member array bound from its i…
tautschnig Oct 19, 2026
d2b8f8e
C++: no scalar binding for a multi-element pack of a partial speciali…
tautschnig Oct 19, 2026
af480a6
C++ ADL: the base classes of an argument's class are associated
tautschnig Oct 19, 2026
8de0202
Notes for round 193
tautschnig Oct 19, 2026
4fa5151
C++: sizeof of a subscript of a class object
tautschnig Oct 19, 2026
70277cd
C++: dereference a cast to a reference to a pointer
tautschnig Oct 19, 2026
8ff91f0
cbmc-cpp: KNOWNBUG for a discarded return in placeholder deduction; b…
tautschnig Oct 19, 2026
1b9d072
C++: a constexpr static data member of class type is const
tautschnig Oct 19, 2026
69671d7
cbmc-cpp: run the std::span tests with the MSVC STL
tautschnig Oct 19, 2026
4c1c5a6
C++: fold reads of constexpr objects in a requires-clause
tautschnig Oct 19, 2026
e2ef278
C++ deduction: an explicit template template argument in P
tautschnig Oct 19, 2026
8cf9873
C++: check a member template's trailing requires-clause with its own …
tautschnig Oct 19, 2026
7c36600
C++ parser: requires-expression parameters are parameter declarations
tautschnig Oct 19, 2026
ea8c6ae
C++: keep the cv-qualifiers of a named parameter pack's pattern
tautschnig Oct 19, 2026
ddffc01
C++: type-constraints of a conversion function template's parameters
tautschnig Oct 20, 2026
6ac4266
C++: an explicit conversion function template is not used in copy-ini…
tautschnig Oct 20, 2026
b9f0583
C++: a parenthesized aggregate initialization copy-initializes its el…
tautschnig Oct 20, 2026
6e00594
C++: a function template's empty pack binding ends with its declaration
tautschnig Oct 20, 2026
986ffa9
C++: a trailing requires-clause reuses the parameters already in scope
tautschnig Oct 20, 2026
5469a8f
cbmc-cpp: run cpp20_ranges_basic with the MSVC STL; drop broken-msvc-stl
tautschnig Oct 20, 2026
7af67a8
C++ deduction: the parameters of a pointer to member function type
tautschnig Oct 20, 2026
7ff1b9d
Visual Studio preprocessing: use the MSVC STL's non-vectorized algori…
tautschnig Oct 20, 2026
903416a
C++ parser: a non-type parameter pack of a qualified type
tautschnig Oct 20, 2026
2d996ed
C++ parser: declare a non-type parameter of a qualified type to the s…
tautschnig Oct 20, 2026
734aa5b
C++: static_cast to a class may use an explicit constructor
tautschnig Oct 20, 2026
740508b
C++ Visual Studio mode: declare the MSVC STL's character intrinsics
tautschnig Oct 20, 2026
0c43f80
C++ deduction: a template template parameter deduces the template
tautschnig Oct 20, 2026
a14783f
C++: a call with dependent qualified arguments as a template argument
tautschnig Oct 20, 2026
72244c7
C++: __is_assignable of a class checks the operator= call
tautschnig Oct 20, 2026
d556e96
Visual Studio mode: __is_assignable_no_precondition_check
tautschnig Oct 20, 2026
cc2a46a
Notes for round 194
tautschnig Oct 20, 2026
f22b37d
C++ deduction: factor out matching a template template parameter
tautschnig Oct 20, 2026
f1888b1
cbmc-cpp: std::format test is CORE again
tautschnig Oct 20, 2026
4f0e270
C++: cite [temp.arg.general]/3 for the type-id/expression ambiguity
tautschnig Oct 20, 2026
03888b4
C++ partial ordering: a non-dependent part of P must equal A
tautschnig Oct 20, 2026
febf552
C++: a stale parameter symbol does not hide a function parameter pack
tautschnig Oct 20, 2026
b2368bf
C++: an rvalue reference binds to a temporary of a braced scalar prvalue
tautschnig Oct 20, 2026
98dab5c
C++: a top-level const parameter does not change a function template'…
tautschnig Oct 20, 2026
918c783
C++: pointer arithmetic instantiates the pointee class template
tautschnig Oct 20, 2026
b923949
C++20: a lambda's template-parameter-list is its operator()'s
tautschnig Oct 20, 2026
f033bb0
C++: a lambda's lowered call operator is evaluated in constant expres…
tautschnig Oct 20, 2026
48f2777
C++20: select the destructor among constrained prospective destructors
tautschnig Oct 20, 2026
f47e4a5
C++17: class template argument deduction for `C{}' without arguments
tautschnig Oct 20, 2026
0244449
C++: find the closure type of a lambda in a template specialization
tautschnig Oct 20, 2026
18f336c
C++: a member's trailing return type names its parameters
tautschnig Oct 20, 2026
c2788ae
C++: a friend function defined outside its class is not in its scope
tautschnig Oct 20, 2026
9dca097
C++: compare the referred objects of reference-typed operands
tautschnig Oct 20, 2026
6b44404
C++: KNOWNBUG for an alias template parameter shadowed by a later name
tautschnig Oct 20, 2026
6404354
Notes for round 195
tautschnig Oct 21, 2026
c79b5a8
C++: a template parameter is found before the template's using scope
tautschnig Oct 21, 2026
f574f1a
C++: a function type's trailing return type names its parameters
tautschnig Oct 21, 2026
aded05e
C++: a data member of reference-to-function type
tautschnig Oct 21, 2026
22e5773
C++: a friend declaration does not bind the function's name
tautschnig Oct 21, 2026
44d7a27
C++: check the access of members of classes in a namespace
tautschnig Oct 21, 2026
5b0a0ec
C++ library models: the classic ctype<char> facet of libc++ and MSVC
tautschnig Oct 21, 2026
ff8b131
Simplifier: merge all constant operands of a bitwise operator
tautschnig Oct 21, 2026
e05d9e8
C++: typeid's integer name of libc++'s non-unique ARM RTTI is unique
tautschnig Oct 21, 2026
3e006f4
C++: member function templates that differ only in the return type
tautschnig Oct 21, 2026
9677e37
cbmc-cpp: two vector tests need more than 256 objects with libc++ 17
tautschnig Oct 21, 2026
db65d33
C++17: `auto x{e}' deduces the type of e
tautschnig Oct 22, 2026
3824b3e
Notes for round 196
tautschnig Oct 22, 2026
fcb8550
Byte-operator lowering: a negative constant offset
tautschnig Oct 22, 2026
bf5edd3
C++ constant evaluation: assign to elements of member arrays
tautschnig Oct 22, 2026
e9c0c00
C++ library models: the MSVC runtime's filesystem string conversions
tautschnig Oct 22, 2026
eed579a
C++: expand a deduced pack outside constant expressions
tautschnig Oct 22, 2026
2e99fc4
C library: link the model of _InterlockedIncrement
tautschnig Oct 22, 2026
7b31ae3
goto conversion: deleting a null pointer calls no destructor
tautschnig Oct 22, 2026
47b0f76
C++ library models: the MSVC runtime's global locale implementation
tautschnig Oct 22, 2026
5db01db
Notes for round 197
tautschnig Oct 22, 2026
8913064
C++ library models: the MSVC runtime's file stream support
tautschnig Oct 22, 2026
65fd098
C++ constexpr evaluation: a local of class type with an array member
tautschnig Oct 22, 2026
b085419
C++: construct initializer_list elements in place in the backing array
tautschnig Oct 22, 2026
5a28bef
C++ front end: rename a local variable that Visual Studio reserves
tautschnig Oct 22, 2026
fae9929
systemc/EqualOp1: comparing class objects without operator== is an error
tautschnig Oct 22, 2026
b467086
Regression tests: exclude x86 preprocessing on other hosts
tautschnig Oct 22, 2026
747c3b4
Regression tests: bounds that let the end of main be reached
tautschnig Oct 22, 2026
aca6544
C++ lambdas: keep a copy of the lambda's source location
tautschnig Oct 22, 2026
bc4a2c8
Byte-operator lowering: the bound of a negative offset with 32-bit si…
tautschnig Oct 22, 2026
130aae7
union_pointer_array_member_field_sensitive_value_set: no-new-smt
tautschnig Oct 22, 2026
7146425
Notes for round 198
tautschnig Oct 22, 2026
f00b40b
KNOWNBUG: std::ofstream from a string with the MSVC STL
tautschnig Oct 22, 2026
4c9bb8a
C preprocessing: data-model options only for gcc of the same family
tautschnig Oct 22, 2026
59c4e07
goto conversion: destroy a conditional's temporaries only if created
tautschnig Oct 22, 2026
c3eaae5
C++ library models: MSVC exception data, code page, libc++ ctype<char>
tautschnig Oct 22, 2026
9f5514f
C++ constexpr evaluation: writes through references to subobjects
tautschnig Oct 22, 2026
dc8ffa7
C++: instantiate a deferred constexpr member a constant expression calls
tautschnig Oct 22, 2026
7fe04a0
CI: check that C++ tests expecting success are not vacuous
tautschnig Oct 22, 2026
229ac7c
C++ constant expressions: a comma's constant left operand is discarded
tautschnig Oct 23, 2026
b2fc11e
unit-proofs/string2optional: THOROUGH, it was vacuous
tautschnig Oct 23, 2026
bbfdecf
Regression tests: bounds that let the end of main be reached, part 2
tautschnig Oct 23, 2026
4e0960f
check_vacuity.py: also check tests that require success by exit status
tautschnig Oct 23, 2026
d15af55
Notes for round 199
tautschnig Oct 23, 2026
becbcc3
Notes for round 199: the cvise result and the commit count
tautschnig Oct 23, 2026
5212b95
byte_extract_negative_constant_offset: declare malloc, include no header
tautschnig Oct 23, 2026
eee43e6
C++: discard a constant comma operand only in a finished initializer
tautschnig Oct 23, 2026
fad1773
cpp11_libstdcxx_header_drops: std::format is broken with libstdc++ 16
tautschnig Oct 23, 2026
0f71871
unit-proofs/string2optional: a KNOWNBUG for its scaling limit
tautschnig Oct 23, 2026
315c780
goto conversion: a branch flag only for temporaries with a destructor
tautschnig Oct 23, 2026
8d13972
C++ parser: the reserved type-trait builtins with cl as the preprocessor
tautschnig Oct 24, 2026
206978d
C preprocessing with cl: __cplusplus is the selected standard's value
tautschnig Oct 24, 2026
97dd7e4
cbmc-cpp: data model and preprocessor assumptions explicit in five tests
tautschnig Oct 24, 2026
1647625
TEMPORARY: instrumentation to debug the Windows-only cbmc-cpp failures
tautschnig Oct 24, 2026
455da85
TEMPORARY: CI runs only the VS 2026 cbmc-cpp tests and the debugging …
tautschnig Oct 24, 2026
98c047f
C library: memcpy and memmove of zero bytes from null with Microsoft'…
tautschnig Oct 24, 2026
17fe68e
C preprocessing with cl: no /Zc:__cplusplus for C++98/03
tautschnig Oct 24, 2026
9d5d9c4
C++ parser: a sequence of alignment-specifiers
tautschnig Oct 24, 2026
cca3cfd
TEMPORARY: print both types of a goto program symbol type inconsistency
tautschnig Oct 24, 2026
2767eec
Linking: one inline function defined in a header shared by C++ and C
tautschnig Oct 25, 2026
269efdf
cbmc-cpp: three std::ofstream tests are broken with the MSVC STL
tautschnig Oct 25, 2026
c9db057
Revert "TEMPORARY: print both types of a goto program symbol type inc…
tautschnig Oct 25, 2026
5230bab
Revert "TEMPORARY: CI runs only the VS 2026 cbmc-cpp tests and the de…
tautschnig Oct 25, 2026
52ab318
Revert "TEMPORARY: instrumentation to debug the Windows-only cbmc-cpp…
tautschnig Oct 25, 2026
24dae4d
C library: the memcpy and memmove models formatted as clang-format wants
tautschnig Oct 25, 2026
69d4fe4
Notes for round 200
tautschnig Oct 25, 2026
9c726cd
cbmc-library/memcpy/test_msvc: declare memcpy and memmove, no <string.h>
tautschnig Oct 25, 2026
c030f3f
doc: reproducing Windows-only C++ failures on Linux
tautschnig Oct 26, 2026
3f09856
C++: a delegating constructor's target constructs the virtual bases
tautschnig Oct 26, 2026
3348a0b
C++: the MSVC runtime's locale and ios_base counters start defined
tautschnig Oct 26, 2026
70df445
cbmc-cpp: the std::ofstream tests run with the MSVC STL again
tautschnig Oct 26, 2026
15ea29c
cbmc-cpp: istringstream's delegating constructors construct basic_ios
tautschnig Oct 26, 2026
1895262
C++: is_constant_evaluated() forwarded by a constexpr function is con…
tautschnig Oct 26, 2026
28aae9a
regression: four C tests whose main does not end by design: no-vacuit…
tautschnig Oct 26, 2026
2cc5422
String_Abstraction16: allocate the buffer size that the test assumes
tautschnig Oct 26, 2026
343ce5e
KNOWNBUG: hidden friend operator<=> template with dependent alias ret…
tautschnig Oct 26, 2026
6ae327a
KNOWNBUG: discarded-value call statement in a constexpr evaluation
tautschnig Oct 26, 2026
46f6bbc
KNOWNBUG: virtual call in the constructor of an indirect base with vi…
tautschnig Oct 26, 2026
ab2bf33
cbmc-cpp: current GCC 16 causes in two broken-libstdcxx16 descs
tautschnig Oct 26, 2026
1cacaca
KNOWNBUG: the standard stream objects are not initialized
tautschnig Oct 26, 2026
43b728b
cpp11_standard_stream_objects_initialized: also the cause of the slow…
tautschnig Oct 26, 2026
5337392
KNOWNBUG: array delete after an intervening malloc
tautschnig Oct 26, 2026
4a42ef2
KNOWNBUG: range adaptor closure called through __invoke_impl
tautschnig Oct 27, 2026
aa22407
Notes for round 201
tautschnig Oct 27, 2026
80c3d27
cbmc-cpp: the MSVC runtime lock model with two threads
tautschnig Oct 27, 2026
cf8a92b
C library: malloc records its object for the new[]/delete[] checks
tautschnig Oct 27, 2026
e044bb0
C++: classes declared by elaborated-type-specifiers, target scope and…
tautschnig Oct 27, 2026
fac4dd4
C++: covariant overriders get thunks of the overridden function's type
tautschnig Oct 27, 2026
5511a06
C++: member access through an accessible intermediate base
tautschnig Oct 27, 2026
900e947
C++: elements of T{...} keep the access judged where they appear
tautschnig Oct 27, 2026
4be246a
C++: cite [class.access.general]/6 where access is judged at the name
tautschnig Oct 27, 2026
9fdd437
C++: a call converted on demand gets the callee's deduced return type
tautschnig Oct 27, 2026
25906cf
C++: library specializations without a definition use the primary tem…
tautschnig Oct 27, 2026
4fd5709
C++: constant evaluation of a call statement whose value is discarded
tautschnig Oct 27, 2026
fb0d12d
C++: a hidden friend template's declared types see the class's parame…
tautschnig Oct 27, 2026
f6ddd93
cpp20_range_adaptor_closure_invoked_through_invoke_impl: what is know…
tautschnig Oct 27, 2026
086671e
Notes for round 202
tautschnig Oct 27, 2026
b245486
C++: class template argument deduction for alias templates
tautschnig Oct 27, 2026
4e34423
goto-conversion: destroy an initializer_list variable's backing array
tautschnig Oct 27, 2026
49efd32
cpp20_range_adaptor_closure_invoked_through_invoke_impl: a faithful r…
tautschnig Oct 27, 2026
5fb2689
C++: libstdc++'s std::_Destroy keeps its header body
tautschnig Oct 28, 2026
c04a188
goto-conversion: an initializer_list backing array is a temporary
tautschnig Oct 28, 2026
7154edf
C++: model std::uncaught_exception and std::uncaught_exceptions
tautschnig Oct 28, 2026
6e1e09a
C++: define and construct the standard stream objects
tautschnig Oct 28, 2026
a7cc06b
goto-conversion: copy a throw's operand before stack unwinding
tautschnig Oct 28, 2026
4e86157
KNOWNBUG: a manipulator template inserted into two stream specializat…
tautschnig Oct 28, 2026
587b840
remove_cpp_exceptions: a destructor run by stack unwinding runs fully
tautschnig Oct 28, 2026
6b80c8f
Notes for round 203
tautschnig Oct 28, 2026
ef4e2ef
KNOWNBUG: the exception object is not copy-constructed
tautschnig Oct 28, 2026
df2c405
KNOWNBUG: integer extraction from std::cin
tautschnig Oct 28, 2026
14664de
KNOWNBUG: a destructor exiting via an exception during unwinding
tautschnig Oct 28, 2026
c48271f
KNOWNBUG: a write to std::cout cannot fail
tautschnig Oct 28, 2026
dc48b32
KNOWNBUG: standard stream objects with the MSVC STL
tautschnig Oct 28, 2026
a2439be
C++: call std::terminate when exception handling is abandoned
tautschnig Oct 28, 2026
5ca42bb
KNOWNBUG: implicit and computed exception specifications
tautschnig Oct 28, 2026
b7ae958
C++: a write to a standard stream may fail
tautschnig Oct 28, 2026
90b61ba
C++: initialize the exception object through its constructor
tautschnig Oct 28, 2026
096b184
KNOWNBUG: the exception object is never destroyed
tautschnig Oct 28, 2026
a1e6bf6
Notes for round 204
tautschnig Oct 28, 2026
a692d9a
remove_cpp_exceptions: clear the exception before a catch(...) body
tautschnig Oct 28, 2026
8039b5c
C++: implicit exception specifications of destructors and deallocation
tautschnig Oct 28, 2026
ce6cf4a
C++: partial ordering of function templates with parameter packs
tautschnig Oct 28, 2026
37762b4
C++: a variable template specialization is an lvalue
tautschnig Oct 28, 2026
9906f44
C++: the address of a constexpr variable
tautschnig Oct 28, 2026
07c1503
KNOWNBUG: auto variable template with a parenthesized initializer
tautschnig Oct 28, 2026
cb2f25b
C++: evaluate noexcept(expression)
tautschnig Oct 28, 2026
c48a447
KNOWNBUG: is_nothrow_constructible with constructor arguments
tautschnig Oct 28, 2026
a979d2e
KNOWNBUG: implicit constructors' exception specification
tautschnig Oct 28, 2026
4774f16
C++: a member's noexcept-specifier is a complete-class context
tautschnig Oct 28, 2026
eddb9f4
Notes for round 205
tautschnig Oct 28, 2026
c95de4a
KNOWNBUG: prvalue aggregate with a base class
tautschnig Oct 29, 2026
ae4f7da
C++: the lifetime of the exception object
tautschnig Oct 29, 2026
3941885
KNOWNBUG: call result through a pack in a static member template
tautschnig Oct 29, 2026
fb6c161
Notes for round 206
tautschnig Oct 29, 2026
9c78d94
C++: a function template name as an operand of an overloaded operator
tautschnig Oct 29, 2026
b6a4edb
C++: a braced prvalue of an aggregate with a base with data members
tautschnig Oct 29, 2026
25d89f3
C++: the "C" locale's num_get facet (libstdc++)
tautschnig Oct 29, 2026
985ecf3
cpp20_call_result_through_pack_in_static_member_template: narrowed di…
tautschnig Oct 29, 2026
3039201
Notes for round 207
tautschnig Oct 29, 2026
b73cf5b
C++ front-end: keep pack expansions of other packs in a template body
tautschnig Oct 29, 2026
51e5bec
C++ front-end: exception specifications of implicit constructors
tautschnig Oct 29, 2026
8703c23
KNOWNBUG: implicit move constructor declared only for move-only members
tautschnig Oct 29, 2026
7a45dcc
C++ front-end: construction vtables for nested base subobjects
tautschnig Oct 29, 2026
16bc1ae
KNOWNBUGs: classes with a repeated polymorphic base
tautschnig Oct 29, 2026
626a3b1
C++ front-end: a variable template specialization instantiated again
tautschnig Oct 29, 2026
f92ccff
C++ front-end: dynamic initialization of instantiated variables
tautschnig Oct 29, 2026
1c1db65
C++ front-end: member noexcept-specifiers that name later members
tautschnig Oct 29, 2026
250331d
KNOWNBUG: member noexcept-specifier naming a later member, class temp…
tautschnig Oct 29, 2026
9298d4d
Notes for round 208
tautschnig Oct 29, 2026
366e0e9
C++ front-end: thunks are not overload candidates
tautschnig Oct 30, 2026
8af0767
C++ front-end: the table of a repeated base subobject
tautschnig Oct 30, 2026
5611d22
C++ front-end: noexcept-specifiers of class template members when needed
tautschnig Oct 30, 2026
b018b10
C++ front-end: implicit move constructors for classes with movable me…
tautschnig Oct 30, 2026
8add331
C++ front-end: dynamic_cast to a pointer to void
tautschnig Oct 30, 2026
603028b
C++: delete through a pointer to a polymorphic base deallocates the o…
tautschnig Oct 30, 2026
f7e8678
KNOWNBUG: overrider reached through a virtual base's table in a deriv…
tautschnig Oct 30, 2026
4cbacd7
Notes for round 209
tautschnig Oct 30, 2026
e569332
C++ front-end: no implicit move constructor for a deleted member move
tautschnig Oct 30, 2026
75fb189
KNOWNBUGs: gaps found auditing the known limitations
tautschnig Oct 30, 2026
61a69a0
KNOWNBUGs: <chrono> and <format> body drops with libstdc++ 16.2.0
tautschnig Oct 30, 2026
4f2d45e
KNOWNBUG: integer insertion into a stream with the MSVC STL
tautschnig Oct 30, 2026
d5afeb7
Notes for round 209: audit of known gaps
tautschnig Oct 30, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
The diff you're trying to view is too large. We only load the first 3000 changed files.
1 change: 1 addition & 0 deletions .clang-format-ignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,4 @@ jbmc/src/miniz/miniz.cpp
jbmc/src/miniz/miniz.h
src/cprover/wcwidth.c
unit/catch/catch.hpp
.kiro
212 changes: 198 additions & 14 deletions .github/workflows/pull-request-checks.yaml

Large diffs are not rendered by default.

15,735 changes: 15,735 additions & 0 deletions .kiro/decltype_tuple_apply_findings.md

Large diffs are not rendered by default.

23 changes: 23 additions & 0 deletions .kiro/reductions/da1_and_helper_23line.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
extern "C" void __CPROVER_assert(bool, const char *);
template <bool> using __enable_if_t = int;
template <int __v> struct integral_constant {
static const int value = __v;
};
template <class...> using __expand_to_true = integral_constant<true>;
template <class... _Pred>
__expand_to_true<__enable_if_t<_Pred::value>...> __and_helper(int);
template <class> integral_constant<false> __and_helper(...);
template <class... _Pred> using _And = decltype(__and_helper<_Pred...>(0));
template <class, class = void>
struct _HasToAddress : integral_constant<false> {};
template <class _Pointer>
struct _HasToAddress<_Pointer, decltype(to_address(_Pointer()))>;
template <class> struct _IsFancyPointer {
static const bool value = _HasToAddress<int>::value;
};
template <class _Pointer> void __to_address(_Pointer);
template <class _Pointer>
auto to_address(_Pointer __p) -> decltype(__to_address(__p));
int main() {
__CPROVER_assert(_And<_IsFancyPointer<int>>::value, "conjunction holds");
}
108 changes: 108 additions & 0 deletions .kiro/reductions/fh1_layer5_108lines.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,108 @@
template <int __v> struct integral_constant {
static const int value = __v;
};
struct __apply_cv_impl {
template <class _Up> using __apply = _Up;
};
template <class, class _Up> using __apply_cv_t = __apply_cv_impl::__apply<_Up>;
template <class _Fp, class...> decltype(_Fp()()) __invoke(_Fp, ...);
template <unsigned long...> struct __tuple_indices {};
template <class _IdxType, _IdxType... _Values> struct __integer_sequence {
template <long> using __to_tuple_indices = __tuple_indices<_Values...>;
};
template <long _Ep, long _Sp>
using __make_indices_imp =
__make_integer_seq<__integer_sequence, long,
_Ep - _Sp>::template __to_tuple_indices<_Sp>;
template <class _Tp, _Tp...> struct integer_sequence;
template <long... _Ip>
using index_sequence = integer_sequence<unsigned long, _Ip...>;
template <class _Tp, _Tp _Ep>
using __make_integer_sequence = __make_integer_seq<integer_sequence, _Tp, _Ep>;
template <class _Tp, _Tp _Np>
using make_integer_sequence = __make_integer_sequence<_Tp, _Np>;
template <long _Np>
using make_index_sequence = make_integer_sequence<unsigned long, _Np>;
template <class... _Tp>
using index_sequence_for = make_index_sequence<sizeof...(_Tp)>;
template <class...> class tuple;
template <int _Ep, long _Sp = 0> struct __make_tuple_indices {
typedef __make_indices_imp<_Ep, _Sp> type;
};
template <class...> struct __tuple_types {};
template <class> struct tuple_size;
template <class... _Tp>
struct tuple_size<tuple<_Tp...>> : integral_constant<sizeof...(_Tp)> {};
template <class, class> struct __make_tuple_types_flat;
template <template <class...> class _Tuple, class... _Types, long... _Idx>
struct __make_tuple_types_flat<_Tuple<_Types...>, __tuple_indices<_Idx...>> {
template <class _Tp>
using __apply_quals =
__tuple_types<__apply_cv_t<_Tp, __type_pack_element<_Idx, _Types...>>...>;
};
template <class _Tp, long _Ep = tuple_size<_Tp>::value, long _Sp = 0>
struct __make_tuple_types {
using type =
__make_tuple_types_flat<_Tp, typename __make_tuple_indices<_Ep, _Sp>::
type>::template __apply_quals<_Tp>;
};
template <class _Hp> struct __tuple_leaf {
_Hp __value_;
};
template <class...> struct __tuple_impl;
template <long... _Indx, class... _Tp>
struct __tuple_impl<__tuple_indices<_Indx...>, _Tp...> : __tuple_leaf<_Tp>... {
template <unsigned long... _Uf, class... _Tf, class... _Up>
__tuple_impl(__tuple_indices<_Uf...>, __tuple_types<_Tf...>,
__tuple_indices<>, __tuple_types<>, _Up... __u)
: __tuple_leaf<_Tf>(__u)... {}
};
template <class... _Tp> struct tuple {
__tuple_impl<typename __make_tuple_indices<sizeof...(_Tp)>::type, _Tp...>
__base_;
template <class... _Up>
tuple(_Up... __u)
: __base_(typename __make_tuple_indices<sizeof...(_Up)>::type(),
typename __make_tuple_types<tuple>::type(),
typename __make_tuple_indices<sizeof...(_Tp),
sizeof...(_Up)>::type(),
typename __make_tuple_types<tuple, sizeof...(_Tp),
sizeof...(_Up)>::type(),
__u...) {}
};
template <class _Tp> constexpr long tuple_size_v = tuple_size<_Tp>::value;
template <class...> struct __perfect_forward_impl;
template <class _Op, long... _Idx, class... _BoundArgs>
struct __perfect_forward_impl<_Op, index_sequence<_Idx...>, _BoundArgs...> {
tuple<_BoundArgs...> __bound_args_;
template <class... _Args>
__perfect_forward_impl(_Args... __bound_args)
: __bound_args_(__bound_args...) {}
template <class...> auto operator()() -> decltype(_Op());
};
template <class _Op, class... _Args>
using __perfect_forward =
__perfect_forward_impl<_Op, index_sequence_for<>, _Args...>;
template <long _NBound, class = make_index_sequence<_NBound>>
struct __bind_back_op;
template <long _NBound, long... _Ip>
struct __bind_back_op<_NBound, index_sequence<_Ip...>> {};
template <class _Fn, class _BoundArgs>
struct __bind_back_t
: __perfect_forward<__bind_back_op<tuple_size_v<_BoundArgs>>, _Fn,
_BoundArgs> {
using __perfect_forward<__bind_back_op<tuple_size_v<_BoundArgs>>, _Fn,
_BoundArgs>::__perfect_forward;
};
template <class _Fn, class... _Args> auto __bind_back(_Fn __f, _Args...) {
return __bind_back_t<_Fn, tuple<_Args...>>(__f, 0);
}
struct {
auto operator()(int __n) { return __bind_back(this, __n); }
} take;
int main_arr;
int main() {
auto c = take(3);
auto r = __invoke(c, main_arr);
(void)r;
}
113 changes: 113 additions & 0 deletions .kiro/reductions/fk1_layer8_113lines.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,113 @@
template <int __v> struct integral_constant {
static const int value = __v;
};
struct __apply_cv_impl {
template <class _Up> using __apply = _Up;
};
template <class, class _Up> using __apply_cv_t = __apply_cv_impl::__apply<_Up>;
template <class _Fp> decltype(_Fp()()) __invoke(_Fp);
template <class> using invoke_result_t = int;
invoke_result_t<void> invoke(void());
template <unsigned long...> struct __tuple_indices {};
template <class _IdxType, _IdxType... _Values> struct __integer_sequence {
template <long> using __to_tuple_indices = __tuple_indices<_Values...>;
};
template <long _Ep, long _Sp>
using __make_indices_imp =
__make_integer_seq<__integer_sequence, long,
_Ep - _Sp>::template __to_tuple_indices<_Sp>;
template <class _Tp, _Tp...> struct integer_sequence;
template <long... _Ip>
using index_sequence = integer_sequence<unsigned long, _Ip...>;
template <class _Tp, _Tp _Ep>
using __make_integer_sequence = __make_integer_seq<integer_sequence, _Tp, _Ep>;
template <class _Tp, _Tp _Np>
using make_integer_sequence = __make_integer_sequence<_Tp, _Np>;
template <long _Np>
using make_index_sequence = make_integer_sequence<unsigned long, _Np>;
template <class... _Tp>
using index_sequence_for = make_index_sequence<sizeof...(_Tp)>;
template <class...> class tuple;
template <int _Ep, long _Sp = 0> struct __make_tuple_indices {
typedef __make_indices_imp<_Ep, _Sp> type;
};
template <class...> struct __tuple_types {};
template <class> struct tuple_size;
template <class... _Tp>
struct tuple_size<tuple<_Tp...>> : integral_constant<sizeof...(_Tp)> {};
template <class, class> struct __make_tuple_types_flat;
template <template <class...> class _Tuple, class... _Types, long... _Idx>
struct __make_tuple_types_flat<_Tuple<_Types...>, __tuple_indices<_Idx...>> {
template <class _Tp>
using __apply_quals =
__tuple_types<__apply_cv_t<_Tp, __type_pack_element<_Idx, _Types...>>...>;
};
template <class _Tp, long _Ep = tuple_size<_Tp>::value, long _Sp = 0>
struct __make_tuple_types {
using type =
__make_tuple_types_flat<_Tp, typename __make_tuple_indices<_Ep, _Sp>::
type>::template __apply_quals<_Tp>;
};
template <class _Hp> struct __tuple_leaf {
_Hp __value_;
};
template <class...> struct __tuple_impl;
template <long... _Indx, class... _Tp>
struct __tuple_impl<__tuple_indices<_Indx...>, _Tp...> : __tuple_leaf<_Tp>... {
template <unsigned long... _Uf, class... _Tf, class... _Up>
__tuple_impl(__tuple_indices<_Uf...>, __tuple_types<_Tf...>,
__tuple_indices<>, __tuple_types<>, _Up... __u)
: __tuple_leaf<_Tf>(__u)... {}
};
template <class... _Tp> struct tuple {
__tuple_impl<typename __make_tuple_indices<sizeof...(_Tp)>::type, _Tp...>
__base_;
template <class... _Up>
tuple(_Up... __u)
: __base_(typename __make_tuple_indices<sizeof...(_Up)>::type(),
typename __make_tuple_types<tuple>::type(),
typename __make_tuple_indices<sizeof...(_Tp),
sizeof...(_Up)>::type(),
typename __make_tuple_types<tuple, sizeof...(_Tp),
sizeof...(_Up)>::type(),
__u...) {}
};
template <int> void get();
template <class _Tp> constexpr long tuple_size_v = tuple_size<_Tp>::value;
template <class...> struct __perfect_forward_impl;
template <class _Op, long... _Idx, class... _BoundArgs>
struct __perfect_forward_impl<_Op, index_sequence<_Idx...>, _BoundArgs...> {
tuple<_BoundArgs...> __bound_args_;
template <class... _Args>
__perfect_forward_impl(_Args... __bound_args)
: __bound_args_(__bound_args...) {}
template <class...> auto operator()() -> decltype(_Op()(get<_Idx>...));
};
template <class _Op, class... _Args>
using __perfect_forward =
__perfect_forward_impl<_Op, index_sequence_for<_Args...>, _Args...>;
template <long _NBound, class = make_index_sequence<_NBound>>
struct __bind_back_op;
template <long _NBound, long... _Ip>
struct __bind_back_op<_NBound, index_sequence<_Ip...>> {
template <class _Fn, class _BoundArgs>
auto operator()(_Fn __f, _BoundArgs) -> decltype(invoke(__f));
};
template <class _Fn, class _BoundArgs>
struct __bind_back_t
: __perfect_forward<__bind_back_op<tuple_size_v<_BoundArgs>>, _Fn,
_BoundArgs> {
using __perfect_forward<__bind_back_op<tuple_size_v<_BoundArgs>>, _Fn,
_BoundArgs>::__perfect_forward;
};
template <class _Fn, class... _Args> auto __bind_back(_Fn __f, _Args...) {
return __bind_back_t<_Fn, tuple<_Args...>>(__f, 0);
}
struct {
auto operator()(int __n) { return __bind_back(this, __n); }
} take;
int main() {
auto c = take(3);
auto r = __invoke(c);
(void)r;
}
14 changes: 14 additions & 0 deletions .kiro/reductions/lambda_decltype_cvs1_531b.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
template <int __v> struct integral_constant {
static const int value = __v;
};
template <bool, class> using __enable_if_t = int;
using ::wprintf __attribute__((__using_if_exists__));
template <class> struct basic_string {
int __r_;
basic_string(basic_string &&)
: __r_([](basic_string __s) -> decltype(__s) {}) {}
template <__enable_if_t<integral_constant<false>::value, int> = 0>
basic_string(char *);
};
basic_string Trans_NS_literals___throw_invalid_type_format_error___trans_tmp_2 =
basic_string<char>("");
33 changes: 33 additions & 0 deletions .kiro/reductions/ranges_pipe_itc_cvr1_1382b.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
template <int __v> struct integral_constant {
static const int value = __v;
};
namespace std {
template <class _Tp, _Tp...> struct integer_sequence;
template <long... _Ip> using index_sequence = integer_sequence<long, _Ip...>;
template <class _Tp, _Tp _Ep>
using __make_integer_sequence = __make_integer_seq<integer_sequence, _Tp, _Ep>;
template <class _Tp, _Tp _Np>
using make_integer_sequence = __make_integer_sequence<_Tp, _Np>;
template <long _Np>
using make_index_sequence = make_integer_sequence<long, _Np>;
template <class...> struct tuple {};
template <class> struct tuple_size;
template <class... _Tp>
struct tuple_size<tuple<_Tp...>> : integral_constant<sizeof...(_Tp)> {};
template <class _Tp> long tuple_size_v = tuple_size<_Tp>::value;
template <class> struct __perfect_forward_impl;
template <class... _Args>
using __perfect_forward = __perfect_forward_impl<_Args...>;
template <long _NBound, class = make_index_sequence<_NBound>>
struct __bind_back_op;
template <long _NBound, long... _Ip>
struct __bind_back_op<_NBound, index_sequence<_Ip...>>;
template <class, class _BoundArgs>
struct __bind_back_t
: __perfect_forward<__bind_back_op<tuple_size_v<_BoundArgs>>> {};
template <class _Fn> void __bind_back(_Fn, int) { __bind_back_t<_Fn, tuple<>>; }
int operator0___n;
struct {
auto operator0() { __bind_back(this, operator0___n); }
} take;
} // namespace std
Loading
Loading