From f616461cfae03a9ab5e9cc9ef3d9eba70e45715a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 28 Mar 2026 20:28:19 +0000 Subject: [PATCH] Remove deprecated add_axioms_for_copy method Fixes: #8018 --- .../strings/string_constraint_generator.h | 3 --- .../string_constraint_generator_main.cpp | 24 ------------------- 2 files changed, 27 deletions(-) diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index f439e5f28b3..f536b2bc1ab 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -151,9 +151,6 @@ class string_constraint_generatort final std::pair add_axioms_for_empty_string(const function_application_exprt &f); - 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( diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 81603410ed6..c02d18d134d 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -268,8 +268,6 @@ string_constraint_generatort::add_axioms_for_function_application( return add_axioms_for_trim(expr); else if(id == ID_cprover_string_empty_string_func) return add_axioms_for_empty_string(expr); - else if(id == ID_cprover_string_copy_func) - return add_axioms_for_copy(expr); else if(id == ID_cprover_string_of_int_hex_func) return add_axioms_from_int_hex(expr); else if(id == ID_cprover_string_of_float_func) @@ -300,28 +298,6 @@ string_constraint_generatort::add_axioms_for_function_application( UNREACHABLE; } -/// add axioms to say that the returned string expression is equal to the -/// argument of the function application -/// \deprecated should use substring instead -/// \param f: function application with one argument, which is a string, -/// or three arguments: string, integer offset and count -/// \return a new string expression -DEPRECATED(SINCE(2017, 10, 5, "should use substring instead")) -std::pair -string_constraint_generatort::add_axioms_for_copy( - const function_application_exprt &f) -{ - const auto &args = f.arguments(); - PRECONDITION(args.size() == 3 || args.size() == 5); - const array_string_exprt res = array_pool.find(args[1], args[0]); - const array_string_exprt str = get_string_expr(array_pool, args[2]); - const typet &index_type = str.length_type(); - const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3]; - const exprt count = - args.size() == 3 ? array_pool.get_or_create_length(str) : args[4]; - return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count)); -} - /// Length of a string /// /// Returns the length of the string argument of the given function application