From 3f50573c2be9094a98cb4d01cc84650a7cc92d86 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 28 Mar 2026 23:54:57 +0000 Subject: [PATCH] Remove deprecated add_axioms_for_concat_code_point method Fixes: #8014 --- .../string_concatenation_builtin_function.cpp | 21 ------------------- .../strings/string_constraint_generator.h | 2 -- .../string_constraint_generator_main.cpp | 2 -- 3 files changed, 25 deletions(-) diff --git a/src/solvers/strings/string_concatenation_builtin_function.cpp b/src/solvers/strings/string_concatenation_builtin_function.cpp index 96de6af270c..9ab4fec5d6c 100644 --- a/src/solvers/strings/string_concatenation_builtin_function.cpp +++ b/src/solvers/strings/string_concatenation_builtin_function.cpp @@ -167,27 +167,6 @@ string_constraint_generatort::add_axioms_for_concat( res, s1, s2, index_zero, array_pool.get_or_create_length(s2)); } -/// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function -/// \deprecated java specific -/// \param f: function application with two arguments: a string and a code point -/// \return an expression -std::pair -string_constraint_generatort::add_axioms_for_concat_code_point( - const function_application_exprt &f) -{ - PRECONDITION(f.arguments().size() == 4); - const array_string_exprt res = - array_pool.find(f.arguments()[1], f.arguments()[0]); - const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]); - const typet &char_type = to_type_with_subtype(s1.content().type()).subtype(); - const typet &index_type = s1.length_type(); - const array_string_exprt code_point = - array_pool.fresh_string(index_type, char_type); - return combine_results( - add_axioms_for_code_point(code_point, f.arguments()[3]), - add_axioms_for_concat(res, s1, code_point)); -} - std::vector string_concatenation_builtin_functiont::eval( const std::vector &input1_value, const std::vector &input2_value, diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index f439e5f28b3..84dfa88baa9 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -154,8 +154,6 @@ class string_constraint_generatort final std::pair add_axioms_for_copy(const function_application_exprt &f); - std::pair - add_axioms_for_concat_code_point(const function_application_exprt &f); std::pair add_axioms_for_constant( const array_string_exprt &res, irep_idt sval, diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 81603410ed6..e1c3664a670 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -260,8 +260,6 @@ string_constraint_generatort::add_axioms_for_function_application( return add_axioms_for_compare_to(expr); else if(id == ID_cprover_string_literal_func) return add_axioms_from_literal(expr); - else if(id == ID_cprover_string_concat_code_point_func) - return add_axioms_for_concat_code_point(expr); else if(id == ID_cprover_string_substring_func) return add_axioms_for_substring(expr); else if(id == ID_cprover_string_trim_func)