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 2340 commits into
Draft
tautschnig wants to merge 2340 commits into
tautschnig wants to merge 2340 commits into
Conversation
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
10 times, most recently
from
March 18, 2026 22:35
ab675bb to
4f0b085
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8878 +/- ##
===========================================
+ Coverage 80.83% 81.94% +1.11%
===========================================
Files 1717 1725 +8
Lines 190074 219645 +29571
Branches 73 81 +8
===========================================
+ Hits 153653 179999 +26346
- Misses 36421 39646 +3225 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
10 times, most recently
from
March 31, 2026 08:28
8f4e2d7 to
f3d208e
Compare
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
6 times, most recently
from
April 3, 2026 23:29
5cc8d28 to
980d519
Compare
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
2 times, most recently
from
April 28, 2026 09:27
6347e6c to
b5975fe
Compare
…e; inline static members are definitions
User-reported Issue 12. N5008 [dcl.init.aggr]/4: an array of class type
is initialised element by element from its braced list. The list of an
in-class `static constexpr V vs[N] = {V(1, 2), V(3, 4)};' was handed to
the constructor machinery as ONE operand and became an N-argument
constructor call ("found no match for symbol 'V'"); it now takes the
path a namespace-scope array takes (convert_initializer).
[class.static.data]/3: an `inline' static data member's in-class
declaration is its definition. Left `extern', the initializer of
`static inline const V iv[2] = {...}' never ran (the dynamic
initialization pass skips extern symbols) and the constructor-call code
sat in the symbol's value, which the static initializer then tried to
assign (a type mismatch in symex).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
User-reported Issue 13 (first half). N5008 [temp.deduct.conv]/1 deduces
the conversion function template's parameter from the target type;
[temp.deduct]/5 supplies the parameters that were not deduced from their
default template arguments -- the SFINAE idiom `template <class U, class
= enable_if_t<is_convertible_v<T, U>>> operator U() const'. The
defaulted parameter was left unassigned and the candidate dropped
("invalid implicit conversion from 'struct Wrap' to 'uint64_t'"). The
defaults are now substituted (a failing default is a deduction failure,
[temp.deduct]/8); a default naming the enclosing class template's
parameters gets those bound from the class instance's recorded
arguments, as instantiate_template does for nested templates.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…cks in binary folds and sizeof... User-reported Issue 13 (second half, soundness). A user function whose body the front-end could not fully type-check was kept incomplete with a warning and the error count rolled back: the run reported VERIFICATION SUCCESSFUL with exit 0 over a truncated main() -- every assertion after the failing statement silently gone. The incomplete body is now an error (CONVERSION ERROR, exit 6); library bodies keep the tolerant path. Sixteen tests in cbmc-cpp had been passing this way and are KNOWNBUG now, each with its underlying failure recorded. Two of the truncations were in the new lambda matrix test: * N5008 [expr.prim.fold]/3: a binary fold over an EMPTY pack yields its init operand for either operand order. The side of the pack was decided by the replicated `base$k' names alone, which do not exist for 0 or 1 elements; the operand that names a pack (a replicated name, a recorded pack, a parameter of this method, or a name nothing binds -- the empty pack leaves no parameter) is the pattern. This method's own pack size is found among several live packs by the class prefix of the pack-size key. * [expr.sizeof]/5: `sizeof...(xs)' over a FUNCTION parameter pack: the general handler knows the type pack's name, not `xs'; the member-body pass now folds it from the replicated count or the recorded size. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…cated main() become KNOWNBUG New: cpp17_static_constexpr_class_array_member (in-class static constexpr / inline const arrays of class type, N = 1/2/3, brace elements), cpp17_conversion_template_defaulted_parameter (conversion function templates with a defaulted type / non-type SFINAE parameter, the default naming the enclosing class's parameter), cpp17_incomplete_user_body_is_an_error (an ill-formed program is rejected with CONVERSION ERROR instead of a SUCCESSFUL verdict over a truncated body). Verified with g++ 13 and clang++ 18. KNOWNBUG (16): cpp11_nontype_pack_recursive_two_elem, cpp14_generic_lambda_types, cpp17_function_reference_param, cpp17_libcxx_variant, cpp17_variant_basic (+ libcxx variant), cpp20_class_nttp_brace, cpp20_concept_compound_requirement, cpp20_concept_iterator_chain, cpp20_concepts_named, cpp20_concepts_overload, cpp20_concepts_requires_type, cpp20_nttp_string, cpp20_ranges_basic, cpp20_requires_unparenthesized, cpp26_pack_indexing_expr. Each was reported SUCCESSFUL while main() had been truncated after a type-check failure; the underlying diagnostic is recorded in the test.desc. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…e candidate N5008 [temp.inst]/4 and /11: a function template specialization is implicitly instantiated only when referenced in a context that requires its definition; overload resolution needs the declaration alone, and an implementation shall not instantiate what is not needed. A converting constructor template tried for a user-defined conversion during candidate matching (`Loop(I &&)' for a `const Loop &' parameter while resolving `take(&d)') was instantiated body included; when the candidate lost, the body -- often ill-formed for those arguments -- was still converted and its errors printed: the `no match for symbol 'set'' x115 signature of the dog-food sweep (natural_loops.h), and the "dropped the body" warnings that followed. Such instances are recorded (speculative_instances); their queued bodies are held back while the work list drains and released as soon as a converted body or initializer refers to them (references live in named sub-trees too -- a temporary object's `#initializer' holds its constructor call -- so the whole tree is walked). At the end of type checking the still-unreferenced ones are left as bodyless declarations without a diagnostic. A selected candidate is converted exactly as before. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Findings from the first CI run of the draft PR (diffblue#8878): * clang (-Werror): two lambdas captured `this' without using it (-Wunused-lambda-capture) -- every clang and BSD/macOS build failed on them; the front-end libraries now build with clang++ -Werror. * MSVC: a local variable named `cdecl' (a Windows keyword macro). * check_help: --no-body-assertions was missing from the cbmc and jbmc man pages. * doxygen: `#pragma' / `@inflight_exception' style words in doc comments were link requests; three \param lists documented the wrong function; `<locale>' in a comment was an HTML tag. The C++ front-end development notes under doc/architectural (review logs with nested markdown doxygen cannot parse) are excluded from the doxygen run. * clang-format: the whole-branch diff against develop had ten src files with unformatted hunks (older commits); formatted. Regression test sources and the .kiro notes are excluded from the check for the draft PR (`.clang-format-ignore', cpplint `--exclude'): 314 test files would need reformatting with line-number expectations in their test.desc adjusted -- to be done per individual PR. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…nstantiation, CI status) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The exceptional unwind emitted before a THROW (destructors of the automatic objects constructed since the innermost try, N5008 [except.ctor], [except.throw]/4) also emits the DEAD markers of those scopes. Java has no destructors, and a Java `athrow' throws a local REFERENCE that the exception lowering (remove_exceptions) reads when it replaces the THROW by the in-flight-exception assignment. Marking that local DEAD first made the assignment read a dead variable, so every handler matched a nondeterministic exception: 13 jbmc regression tests (exceptions1/2/4/5/9/22/26/27, catch1, finally3/7, exception-cleanup, nondet_initialize_exception_handler) failed after the C++ unwinding work. Gate the unwind on "mode is not Java" rather than "mode is C++": the C++ front-end gives `main' and `extern "C"' functions C linkage (mode ID_C) and they must keep unwinding (cpp11_throw_dtor_unwinding). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
2bb468a made id_shorthand prefer a symbol's base_name over the `::' split whenever the symbol exists, to keep C++ mangled function names (`ns::f(ref_struct_tag(identifier=std::tag-X<...>))') readable. Java method identifiers `java::A.m:()V' end in their descriptor, so their base_name is not a suffix either, and expr2java started rendering `java::org.cprover.CProver.getCurrentThreadId:()I' as `getCurrentThreadId'. JBMC's concurrency instrumentation matches that rendering against the full descriptor-carrying name (java_bytecode_concurrency_instrumentation.cpp), so `--java-threading' no longer replaced getCurrentThreadId/startThread/ endThread/getMonitorCount: 14 jbmc-concurrency tests failed. Prefer the base name only when the identifier contains `<base_name>(', the C++ function shape the change was made for. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [over.best.ics.general]/4 suppresses user-defined conversion sequences for the parameters of the constructor candidates of ONE copy-initialization (cpp_typecheckt::copy_init_ctor_exploration). A substitution performed while such a candidate is explored -- deducing a constructor template and evaluating its constrained default template argument ([temp.deduct.general]/5, [temp.deduct]/8) -- runs separate overload resolutions, which must see the full set of conversions again. The exemption was keyed on constant_expression_context, which the SFINAE guard itself resets, so it never applied inside a guarded probe. With libstdc++ 11 (Ubuntu 22.04 CI), a `const char*' -> std::string conversion probe reaches the range constructor's `_RequireInputIter<const char*>' default, i.e. is_convertible<random_access_iterator_tag, input_iterator_tag> implemented as `__test_aux<_To1>(declval<_From1>())'; that derived-to-base copy-initialization (a standard conversion, [over.best.ics.general]/6) was refused, the trait's base did not resolve, and the class instance was cached without `value'. Every later `std::vector<int> v(first, last)' then failed with "found no match for symbol 'vector'" (cpp11_conversion_function_template_copy_init, cpp11_locale_ctype_facet on 22.04; libstdc++ 13 uses the __is_convertible builtin and was unaffected). sfinae_contextt now saves and clears copy_init_ctor_exploration like it does constant_expression_context. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The libstdc++ 11 basic_string/_RequireInputIter/is_convertible shape, with a
CTAD-guarded `basic_str(const C*, const A&)' constructor template so that
the `const char*' -> str conversion probe goes through constructor-template
deduction. Fails on the previous binary ("could not fully type-check
'main'"), verified at run time with g++ 13 and clang 18.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ut first
Itanium C++ ABI 2.4 II.1 (as implemented by g++ and clang; N5008 leaves the
layout of a non-standard-layout class to the implementation): a dynamic
class with a primary base -- its first non-virtual dynamic base class in
declaration order -- shares that base's virtual pointer and adds no storage
for its own virtual functions, whose vtable entries follow the primary
base's in the same vtable; and the primary base subobject is placed at
offset 0, before the other bases, whatever its position in the
base-specifier-list.
CBMC gave every class that declares a virtual function its own
`virtual_table::X' struct and `X::@vtable_pointer' component (`struct X : P
{ virtual g(); }' was 24 bytes instead of 16) and flattened the bases in
declaration order (`S : R, P' with P dynamic put R at 0).
Model:
- compound_type: a class with a primary base gets no pointer of its own; its
vtable struct embeds the primary base's vtable struct as first member
`@base' (vtable_chain). Root dynamic classes, and classes whose dynamic
bases are all virtual, keep their own pointer as before.
- do_virtual_table: the vtable object `virtual_table::X@D' of a complete
object D nests the embedded bases' values.
- constructors/destructors: a `B::@vtable_pointer' is set to the address of
the embedded `virtual_table::B' inside the vtable object of the most
derived class sharing that pointer (vtable_pointer_value).
- dispatch: the pointer of the declaring class's primary-base chain
(vtable_pointer_component), cast to `virtual_table::<declaring class>*',
reaches the entry; a class with other dynamic bases still uses their own
pointers for their functions.
- thunks: a base sharing the pointer needs no `this' adjustment; another
dynamic base is at the offset of its own pointer.
- typecheck_compound_bases: resolve all bases first, then lay out the
primary base before the others (bases() keeps declaration order -- the
construction order, [class.base.init]/13).
Virtual bases keep the existing flat model (placed in front, with the
`@most_derived' marker); the ABI places them after the non-virtual part.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Sizes, member offsets measured on objects, base-subobject offsets and virtual dispatch (P* / X* / Q* into three-level and multiple-inheritance hierarchies). 10 assertions failed on the previous binary; verified at run time with g++ 13 and clang 18. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ptr sharing) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [temp.inst]/1: a class template specialization is implicitly
instantiated only when a complete type is required; an alias declaration
does not require one. The typedef branch of convert_non_template_declaration
defers elaboration through skip_typechecking_elaborate, but CLEARED the flag
on exit instead of restoring it. When the aliased type is an alias
template's template-id, resolving it converts the alias template's own
declaration underneath -- also a typedef -- and that inner conversion reset
the flag, so the outer resolver elaborated the specialization.
libstdc++ 11's <string> declares `namespace pmr { template <class T> class
polymorphic_allocator; template <class C, class T = char_traits<C>> using
basic_string = std::basic_string<C, T, polymorphic_allocator<C>>; using
string = basic_string<char>; ... }' with the allocator completed only by
<memory_resource>: std::basic_string<char, ..., polymorphic_allocator<char>>
was instantiated with an incomplete allocator and reported as "dropped 4
system-header declaration(s)" on Ubuntu 22.04. In user code the same shape
laid the class out with an incomplete member that was never constructed
(test cpp11_alias_template_defers_instantiation, 3 assertions failed).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…incomplete argument Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This reverts commit b79b14f. Restoring skip_typechecking_elaborate after the nested alias-template conversion is the [temp.inst]/1-correct behaviour, but cpp20_ranges_pipe_ invoke_drop (libc++ ranges shape) then fails: a `tuple<int>' specialization that is only named through `__apply_cv_t' stays unelaborated, and the later `tuple(_Up... __u)' constructor deduction with an object of that type produces an empty pack. The eager elaboration the cleared flag caused masked that deduction gap. Until the gap is fixed the eager behaviour is kept; the libstdc++ 11 pmr::string alias keeps producing the harmless "dropped 4 system-header declaration(s)" warning on Ubuntu 22.04. The regression test stays as KNOWNBUG. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…b79b14f) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…il padding Two layout defects of multiple inheritance with a non-primary dynamic base. 1. A virtual call through a pointer to a non-primary base enters the overrider through a thunk that adjusts `this' by the base subobject's offset (Itanium C++ ABI 2.5.3). The thunk body was built when the overrider was declared, before add_padding laid the class out, so the offset lacked the alignment padding between base subobjects (`T : P, Q' with P's non-virtual part 12 bytes and Q 8-aligned: 12 instead of 16). The overrider then read its members from the wrong addresses. The body is now built by build_virtual_thunk_body and rebuilt from the final layout in finalize_virtual_thunks, called after add_padding (the thunk records its target and base on its type). Thunks of the primary-base chain keep the zero adjustment. 2. Flattening an already-flattened base (`U : T', `T : P, Q'): the recursion copied P's components from P's own type, so P's tail padding (dropped for the direct base in typecheck_compound_bases) survived in U next to T's own alignment padding, and Q's base-alignment mark -- set on T's copy of Q's first component -- was lost. Q's subobject sat at a misaligned 20 and every later member was 4 bytes off. add_base_components now drops a non-POD indirect base's tail padding as well and propagates the base-alignment mark from `from's copy. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ranch The test sources this branch adds (regression/cbmc-cpp, ansi-c Struct_Padding*/Union_Padding3, unit-proofs harnesses) are now formatted with clang-format-15 and the repository style, and `regression' is no longer excluded in .clang-format-ignore. With the repository's `Standard: c++17' clang-format splits a built-in `<=>' expression into `<= >' in one test (cpp20_spaceship_builtin_strong_ordering); that block is wrapped in clang-format off/on rather than overriding the standard for the directory. test.desc expectations that name a source line were updated (12 tests) and the whole cbmc-cpp suite was re-run. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…on-primary dynamic base 8 assertions; 12 failures on the previous binary; verified at run time with g++ 13 and clang 18. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
… virtual-base design) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [temp.inst]/1: a class template specialization is implicitly
instantiated only when a complete type is required; an alias declaration
does not require one. Two parts:
1. The typedef branch of convert_non_template_declaration defers
elaboration through skip_typechecking_elaborate but CLEARED the flag on
exit instead of restoring it; when the aliased type is an alias
template's template-id, its declaration is converted underneath (also a
typedef) and that reset made the outer resolver elaborate the
specialization. libstdc++ 11's `namespace pmr { using string =
basic_string<char>; }' instantiated std::basic_string<char, ...,
polymorphic_allocator<char>> with the allocator only declared ("dropped 4
system-header declaration(s)" on Ubuntu 22.04); in user code the class
was laid out with an incomplete member that was never constructed.
2. The deferral is about the alias's OWN type only. Once a class body IS
type-checked -- reached from within the alias because a qualified name
looked into it, [temp.inst]/2 -- its bases and members are real uses, so
typecheck_compound_body clears the flag for its duration. Without this
(the first attempt, b79b14f, reverted in 115fdcf) `using
invoke_result_t = __invoke_of<F, A...>::type' left __invoke_of's base
`enable_if<...>' unelaborated, `type' unresolved, and the libc++ ranges
shape cpp20_ranges_pipe_invoke_drop failed with "type has no size".
cpp11_alias_template_defers_instantiation is CORE again.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ep zero-init
Two goto-model validation failures (`--validate-goto-model', which the CI
harness passes to every cbmc-cpp test) in libstdc++ shapes:
1. `__atomic_load_n' etc.: the C front end gives a polymorphic built-in one
symbol per instantiated type, with an implementation; the C++ front end
only took the typed symbol expression, so a single `__atomic_load_n'
symbol served calls on `long long*' and `int*' (_Sp_counted_base::
_M_release) with the return type of whichever came first ("function
returns expression of wrong type") and had no body. The C logic is
factored into c_typecheck_baset::materialize_gcc_polymorphic_builtin and
used by both front ends.
2. A block-scope object with static storage duration and a constructor
(`static const pair<...> __classnames[] = {...}' in regex_traits::
lookup_classname) had the constructor CODE left as its symbol value after
the call was emitted at the declaration, so __CPROVER_initialize
assigned a code block to the object ("lhs and rhs of assignment must
have same type"). N5008 [stmt.dcl]/3, [basic.start.static]/2: the
object is zero-initialized and constructed at its declaration; the value
is now cleared.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The PR check runs cpplint on the changed lines since the merge base (71 findings): comment lines over 80 characters rewrapped; `&static_cast<const irept &>(x)' written as `&x' (runtime/casting); braces around multi-statement if/else bodies; `CPROVER_PREFIX' instead of literal `__CPROVER_'; an empty statement after a label replaced by an empty block; and `// NOLINT( readability/fn_size)' on the closing brace of the eight long functions (elaborate_class_template, typecheck_expr_main, prepare_deferred_method_body, guess_function_template_args, resolve_scope, disambiguate_template_classes, resolve, provide_stdlib_bodies), as the repository already does for typecheck_expr_main's sibling. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
- The layout tests (cbmc-cpp: alignas_pointer_member, cast_of_array_decays,
constexpr_nested_pack_in_multiarg, constexpr_zipped_pack_expansion,
derived_class_bit_field_layout, dynamic_class_vptr_at_offset_zero,
gnu_alignment_attribute_rules, primary_base_shared_vptr,
virtual_thunk_base_offset, cpp_base_subobject_layout, cpp_pragma_pack;
ansi-c: Struct_Padding10/11/12) assert LP64 x86_64 sizes and offsets:
`--64' / `-m64' so that the 32-bit CI build checks the same layout.
- pragma_pack5 (GNU attributes) guarded by `#ifdef __GNUC__' for Visual
Studio mode; the `__builtin_memchr/memcmp/assume_aligned' library tests
tagged gcc-only (MSVC has no such built-ins: implicit declaration).
- unit-proofs/strip_string is THOROUGH: 3.2 GB / 2 minutes, the CI runner's
SAT solver ran out of memory.
- cpp/regex_match_compile tagged gcc-only: Apple's libc++ <regex> (Xcode 16)
does not type-check.
- cpp11_sole_template_false_constraint gained the `^EXIT=6$' / `^SIGNAL=0$'
lines test.pl requires: their absence aborted the whole cbmc-cpp-libcxx
run ("Missing EXIT test").
- unit/count_tests.py reads sources as UTF-8 (the Windows runner's default
code page choked on an em dash in an existing unit test).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Reported by the PR's include-what-you-use job on files this branch adds or
changes (cpp_typecheck_conversions/expr/resolve/template.cpp,
elide_cpp_returned_temporaries.cpp, remove_exceptions_base.{h,cpp}).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…libstdc++ 11 use_facet
Two libstdc++ 11 (Ubuntu 22.04) shapes:
1. `std::string{string_view}': basic_string's converting constructor is
constrained by `_If_sv<_Tp>' = `__and_<is_convertible<const _Tp&,
basic_string_view>, ...>'; the 11 is_convertible is the SFINAE helper
`template<class F1, class T1, class = decltype(__test_aux<T1>(declval<
F1>()))> static true_type __test(int); template<class, class> static
false_type __test(...);'. Substituting the explicit `__test<_From, _To>'
arguments fills in the constrained default; when its call has no viable
function the resolver's silent `throw 0' escaped apply_template_args
and aborted the whole class body being instantiated (`type' undefined,
the base of is_convertible dropped). N5008 [temp.deduct.general]/5 +
[temp.deduct]/8: the failure removes that candidate only; the variadic
`__test(...)' must still be tried. The per-candidate loop now catches
the plain-int substitution failure as it does the kind mismatch. This
is what made the 22.04 unit-proofs (capitalize, trim_from_last_delimiter,
strip_string) fail to type-check strip_string.
2. `use_facet<ctype<char>>': libstdc++ 13 routes it through
__try_use_facet, which the stdlib model overrides to return the modelled
classic-"C" facet; libstdc++ 11's use_facet reads the invisible
`__loc->_M_impl->_M_facets' table itself. The override now applies to
both (cpp11_locale_ctype_facet on 22.04).
unit-proofs/capitalize becomes THOROUGH: with the 11 headers its SAT
instance exceeds the CI runner's memory.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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:
This branch will be split into smaller PRs for review. See CPP_SUPPORT_STATUS.md for a detailed feature matrix.