Repository navigation
Conversation
Require a successful array-size conversion before dereferencing its optional result. Build the generated index expressions without index_exprt, whose preconditions require operands to be typechecked already. Add Assignment_Array_Member to check both copied elements. The new test aborts before the fix and passes afterwards. Tested with GOTO/SSA validation: 17 related C++ regressions pass (4 additional cases skipped by the runner); mutating either expected copied value fails verification. Fixes diffblue#9239.
abcz-wang
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
October 27, 2026 07:21
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
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.
Implicit copy assignment of a class with an array member and a user-provided default constructor aborts in
default_assignop_value. Require the array-size conversion to succeed before dereferencing its optional result.Fixing that check exposes a second abort in
copy_array:index_exprtrequires already-typechecked array operands, but these expressions are generated before type checking. Construct the frontend index expressions withbinary_exprtso their operands and result types can be resolved by the subsequent type-checking pass.Adds a regression checking that both array elements are copied correctly.
Fixes #9239.
Validation on macOS arm64, Apple Clang 21, based on develop
5783f861:New regression aborts on the unmodified development build and passes with this fix.
17 C++ regressions pass with
--validate-goto-model --validate-ssa-equation(assignment, arrays, and constructors); 4 additional cases are skipped by the runner.Mutating either expected copied value correctly produces
VERIFICATION FAILED.clang-format 15 reports no changes on the PR diff;
git diff --checkpasses.Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures added are documented (none added).
User-visible behaviour is documented (restores existing C++ copy-assignment semantics; no new feature or option).
Regression tests are included in the same commit as the fix.
Performance claims include data points (no performance claims).
The PR is restricted to one bugfix.
No unrelated whitespace or formatting changes.