Skip to content

Commit

Permalink
Remove dead method from recursive initialization
Browse files Browse the repository at this point in the history
The ::build_array_string_constructor method was originally intended to be used
for building C string constructors. Unfortunately as written the condition for
calling it was actually impossible to satisfy. This wasn’t noticed so far
because similar code is now generated in ::build_dynamic_array_constructor
instead.

Dead code is a maintenance burden so it’s removed here.
  • Loading branch information
hannes-steffenhagen-diffblue committed Jul 7, 2020
1 parent fda2b60 commit 8bc1772
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 38 deletions.
34 changes: 1 addition & 33 deletions src/goto-harness/recursive_initialization.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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<std::size_t>(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)
Expand Down
5 changes: 0 additions & 5 deletions src/goto-harness/recursive_initialization.h
Original file line number Diff line number Diff line change
Expand Up @@ -262,11 +262,6 @@ class recursive_initializationt
const exprt &size,
const optionalt<irep_idt> &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
Expand Down

0 comments on commit 8bc1772

Please sign in to comment.