Skip to content

Remove deprecated add_axioms_from_bool method#8919

Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-8022-add_axioms_from_bool
Open

Remove deprecated add_axioms_from_bool method#8919
tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig:fix-8022-add_axioms_from_bool

Conversation

@tautschnig
Copy link
Copy Markdown
Collaborator

@tautschnig tautschnig commented Mar 28, 2026

Removed the deprecated add_axioms_from_bool(array_string_exprt, exprt) method and inlined its logic at the call site in string_format_builtin_function.cpp

Fixes: #8022

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig self-assigned this Mar 28, 2026
@codecov
Copy link
Copy Markdown

codecov Bot commented Mar 29, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.46%. Comparing base (6df204e) to head (af83392).

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #8919      +/-   ##
===========================================
- Coverage    80.46%   80.46%   -0.01%     
===========================================
  Files         1704     1704              
  Lines       188665   188659       -6     
  Branches        73       73              
===========================================
- Hits        151805   151799       -6     
  Misses       36860    36860              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@tautschnig tautschnig marked this pull request as ready for review March 31, 2026 12:28
Copilot AI review requested due to automatic review settings March 31, 2026 12:28
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR removes the deprecated string_constraint_generatort::add_axioms_from_bool(array_string_exprt, exprt) helper and inlines its (String.format-related) boolean formatting constraints directly at the call site, aligning with Issue #8022’s deprecation cleanup.

Changes:

  • Removed the deprecated add_axioms_from_bool(const array_string_exprt &, const exprt &) declaration and definition.
  • Inlined the "true" / "false" constraint generation into string_format_builtin_function.cpp for the BOOLEAN format specifier.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File Description
src/solvers/strings/string_format_builtin_function.cpp Inlines the boolean-to-string axioms previously implemented by the deprecated helper.
src/solvers/strings/string_constraint_generator.h Removes the deprecated overload declaration from the generator interface.
src/solvers/strings/string_constraint_generator_valueof.cpp Removes the deprecated overload implementation.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread src/solvers/strings/string_format_builtin_function.cpp
Inline the body of the deprecated 2-argument add_axioms_from_bool
at its sole call site in string_format_builtin_function.cpp. Also
remove the orphaned 1-argument overload declaration which had no
definition or callers.

Fixes: diffblue#8022

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
@tautschnig tautschnig force-pushed the fix-8022-add_axioms_from_bool branch from c049a3d to af83392 Compare March 31, 2026 12:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

src/solvers/strings/string_constraint_generator_valueof.cpp - pair<exprt, string_constraints> string_constraint_generatort::add_axioms_from_bool

3 participants