Remove deprecated add_axioms_for_copy method#8914
Open
tautschnig wants to merge 2 commits intodiffblue:developfrom
Open
Remove deprecated add_axioms_for_copy method#8914tautschnig wants to merge 2 commits intodiffblue:developfrom
tautschnig wants to merge 2 commits intodiffblue:developfrom
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8914 +/- ##
========================================
Coverage 80.47% 80.47%
========================================
Files 1704 1704
Lines 188694 188687 -7
Branches 73 73
========================================
+ Hits 151843 151850 +7
+ Misses 36851 36837 -14 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
There was a problem hiding this comment.
Pull request overview
Removes the long-deprecated string copy axiom generation path from the string solver, based on the claim that ID_cprover_string_copy_func calls are no longer generated (Fixes #8018).
Changes:
- Removed
string_constraint_generatort::add_axioms_for_copydeclaration and definition. - Removed dispatch handling for
ID_cprover_string_copy_funcinadd_axioms_for_function_application.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
src/solvers/strings/string_constraint_generator.h |
Drops the deprecated add_axioms_for_copy API from the generator interface. |
src/solvers/strings/string_constraint_generator_main.cpp |
Removes the ID_cprover_string_copy_func dispatch case and the deprecated implementation. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
force-pushed
the
fix-8018-add_axioms_for_copy
branch
from
f616461 to
702070d
Compare
tautschnig
force-pushed
the
fix-8018-add_axioms_for_copy
branch
3 times, most recently
from
5c5bce2 to
5b6f8a9
Compare
Sort function pointer candidates by identifier name before generating the dispatch code. This ensures the order of IF/GOTO branches in the resulting GOTO program is independent of internal hash table ordering, which can vary when irep IDs are added or removed. Without this fix, unrelated changes to irep_ids.def can cause different function pointer dispatch orderings, leading to different symbolic execution paths and dramatically different SAT solver performance. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The method was deprecated since 2017 in favour of substring, and no code generates ID_cprover_string_copy_func calls. Remove the method, its dispatch entry, the irep ID, and the README reference. Fixes: diffblue#8018 Co-authored-by: Kiro (autonomous agent) <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-8018-add_axioms_for_copy
branch
from
5b6f8a9 to
f4c2ce9
Compare
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.
The method was deprecated since 2017 in favour of substring, and no code generates ID_cprover_string_copy_func calls. Remove the method, its dispatch entry, the irep ID, and the README reference.
Fixes: #8018
Co-authored-by: Kiro kiro-agent@users.noreply.github.com