diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index bca89aec733e..d9ae3643ebd9 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -265,9 +265,7 @@ code_blockt recursive_initializationt::build_constructor_body( } if(lhs_name.has_value()) { - if(should_be_treated_as_cstring(*lhs_name) && type == char_type()) - return build_array_string_constructor(result_symbol); - else if(should_be_treated_as_array(*lhs_name)) + if(should_be_treated_as_array(*lhs_name)) { CHECK_RETURN(size_symbol.has_value()); return build_dynamic_array_constructor( @@ -740,36 +738,6 @@ code_blockt recursive_initializationt::build_pointer_constructor( return body; } -code_blockt recursive_initializationt::build_array_string_constructor( - const symbol_exprt &result) const -{ - PRECONDITION(result.type().id() == ID_pointer); - const typet &type = result.type().subtype(); - PRECONDITION(type.id() == ID_array); - PRECONDITION(type.subtype() == char_type()); - const array_typet &array_type = to_array_type(type); - const auto array_size = - numeric_cast_v(to_constant_expr(array_type.size())); - code_blockt body{}; - - for(std::size_t index = 0; index < array_size - 1; index++) - { - index_exprt index_expr{dereference_exprt{result}, - from_integer(index, size_type())}; - auto const nondet_char = - get_fresh_local_typed_symexpr("nondet_char", char_type()); - body.add(code_declt{nondet_char}); - body.add(code_assignt{index_expr, nondet_char}); - body.add(code_assumet{ - notequal_exprt{index_expr, from_integer(0, array_type.subtype())}}); - } - body.add(code_assignt{index_exprt{dereference_exprt{result}, - from_integer(array_size - 1, size_type())}, - from_integer(0, array_type.subtype())}); - - return body; -} - code_blockt recursive_initializationt::build_array_constructor( const exprt &depth, const symbol_exprt &result) diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index e562388c3ea6..5a2b60878d44 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -262,11 +262,6 @@ class recursive_initializationt const exprt &size, const optionalt &lhs_name); - /// Constructor for strings: as array but the last element is zero. - /// \param result: symbol of the result parameter - /// \return the body of the constructor - code_blockt build_array_string_constructor(const symbol_exprt &result) const; - /// Select the specified struct-member to be non-deterministically /// initialized. /// \param lhs: symbol expression of the top structure