Skip to content

Commit 26e534c

Browse files
committed
Remove unneeded parameter from get_fresh_local_typed_symexpr.
1 parent 431df6a commit 26e534c

File tree

2 files changed

+7
-10
lines changed

2 files changed

+7
-10
lines changed

src/goto-harness/recursive_initialization.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -522,8 +522,7 @@ symbol_exprt recursive_initializationt::get_fresh_local_symexpr(
522522

523523
symbol_exprt recursive_initializationt::get_fresh_local_typed_symexpr(
524524
const std::string &symbol_name,
525-
const typet &type,
526-
const exprt &init_value) const
525+
const typet &type) const
527526
{
528527
symbolt &fresh_symbol = get_fresh_aux_symbol(
529528
type,
@@ -533,7 +532,6 @@ symbol_exprt recursive_initializationt::get_fresh_local_typed_symexpr(
533532
initialization_config.mode,
534533
goto_model.symbol_table);
535534
fresh_symbol.is_lvalue = true;
536-
fresh_symbol.value = init_value;
537535
return fresh_symbol.symbol_expr();
538536
}
539537

@@ -693,8 +691,9 @@ code_blockt recursive_initializationt::build_pointer_constructor(
693691
// we want to initialize the pointee as non-const even for pointer to const
694692
const typet non_const_pointer_type =
695693
pointer_type(remove_const(type.subtype()));
696-
const symbol_exprt &local_result = get_fresh_local_typed_symexpr(
697-
"local_result", non_const_pointer_type, nullptr_expr);
694+
const symbol_exprt &local_result =
695+
get_fresh_local_typed_symexpr("local_result", non_const_pointer_type);
696+
698697
then_case.add(code_declt{local_result});
699698
const namespacet ns{goto_model.symbol_table};
700699
then_case.add(
@@ -860,8 +859,8 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
860859
// we want the local result to be mutable so we can initialise it
861860
const typet mutable_dynamic_array_type =
862861
pointer_type(remove_const(element_type));
863-
const symbol_exprt &local_result = get_fresh_local_typed_symexpr(
864-
"local_result", mutable_dynamic_array_type, exprt{});
862+
const symbol_exprt &local_result =
863+
get_fresh_local_typed_symexpr("local_result", mutable_dynamic_array_type);
865864
body.add(code_declt{local_result});
866865
const namespacet ns{goto_model.symbol_table};
867866
for(auto array_size = min_array_size; array_size <= max_array_size;

src/goto-harness/recursive_initialization.h

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -157,12 +157,10 @@ class recursive_initializationt
157157
/// Construct a new local symbol of type \p type initialised to \p init_value.
158158
/// \param symbol_name: the base name for the new symbol
159159
/// \param type: type for the new symbol
160-
/// \param init_value: expression the symbol should be initialised with
161160
/// \return the symbol expression associated with the new symbol
162161
symbol_exprt get_fresh_local_typed_symexpr(
163162
const std::string &symbol_name,
164-
const typet &type,
165-
const exprt &init_value) const;
163+
const typet &type) const;
166164

167165
/// Construct a new function symbol of type \p fun_type.
168166
/// \param fun_name: the base name for the new symbol

0 commit comments

Comments
 (0)