Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions src/solvers/strings/string_constraint_generator.h
Original file line number Diff line number Diff line change
Expand Up @@ -187,8 +187,6 @@ class string_constraint_generatort final
std::pair<exprt, string_constraintst>
add_axioms_from_int_hex(const function_application_exprt &f);
std::pair<exprt, string_constraintst>
add_axioms_from_long(const function_application_exprt &f);
std::pair<exprt, string_constraintst>
add_axioms_from_bool(const function_application_exprt &f);
std::pair<exprt, string_constraintst>
add_axioms_from_bool(const array_string_exprt &res, const exprt &b);
Expand Down
12 changes: 11 additions & 1 deletion src/solvers/strings/string_constraint_generator_main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,17 @@ string_constraint_generatort::add_axioms_for_function_application(
else if(id == ID_cprover_string_of_double_func)
return add_axioms_from_double(expr);
else if(id == ID_cprover_string_of_long_func)
return add_axioms_from_long(expr);
{
// Inline implementation of the deprecated add_axioms_from_long
PRECONDITION(expr.arguments().size() == 3 || expr.arguments().size() == 4);
const array_string_exprt res =
array_pool.find(expr.arguments()[1], expr.arguments()[0]);
if(expr.arguments().size() == 4)
return add_axioms_for_string_of_int_with_radix(
res, expr.arguments()[2], expr.arguments()[3], 0);
else
return add_axioms_for_string_of_int(res, expr.arguments()[2], 0);
}
else if(id == ID_cprover_string_set_length_func)
return add_axioms_for_set_length(expr);
else if(id == ID_cprover_string_delete_func)
Expand Down
19 changes: 0 additions & 19 deletions src/solvers/strings/string_constraint_generator_valueof.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,25 +35,6 @@ static unsigned long to_integer_or_default(
return def;
}

/// Add axioms corresponding to the String.valueOf(J) java function.
/// \deprecated should use add_axioms_from_int instead
/// \param f: function application with one long argument
/// \return a new string expression
DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int instead"))
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_from_long(
const function_application_exprt &f)
{
PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
const array_string_exprt res =
array_pool.find(f.arguments()[1], f.arguments()[0]);
if(f.arguments().size() == 4)
return add_axioms_for_string_of_int_with_radix(
res, f.arguments()[2], f.arguments()[3], 0);
else
return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
}

/// Add axioms stating that the returned string equals "true" when the Boolean
/// expression is true and "false" when it is false.
/// \deprecated This is Java specific and should be implemented in Java instead
Expand Down
Loading