Skip to content

Commit f95df53

Browse files
committed
Fix based on review comments
will be squashed.
1 parent dcf0ea3 commit f95df53

File tree

2 files changed

+7
-9
lines changed

2 files changed

+7
-9
lines changed

src/goto-harness/recursive_initialization.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -321,10 +321,10 @@ bool recursive_initializationt::should_be_treated_as_array(
321321
initialization_config.pointers_to_treat_as_arrays.end();
322322
}
323323

324-
optionalt<std::size_t>
324+
optionalt<recursive_initializationt::equal_cluster_idt>
325325
recursive_initializationt::find_equal_cluster(const irep_idt &name) const
326326
{
327-
for(size_t index = 0;
327+
for(equal_cluster_idt index = 0;
328328
index != initialization_config.pointers_to_treat_equal.size();
329329
++index)
330330
{
@@ -820,10 +820,7 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
820820

821821
bool recursive_initializationt::needs_freeing(const exprt &expr) const
822822
{
823-
if(expr.type().id() != ID_pointer || expr.type().id() == ID_code)
824-
return false;
825-
else
826-
return true;
823+
return expr.type().id() == ID_pointer && expr.type().id() != ID_code;
827824
}
828825

829826
void recursive_initializationt::free_if_possible(
@@ -846,9 +843,9 @@ void recursive_initializationt::free_if_possible(
846843
.get_identifier() != expr_id &&
847844
initialization_config.arguments_may_be_equal)
848845
{
849-
// in equality cluster but not common origin -> free if equal to origin
846+
// in equality cluster but not common origin -> free if not equal to origin
850847
const auto condition =
851-
equal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
848+
notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
852849
body.add(code_ifthenelset{condition, call_free});
853850
}
854851
else

src/goto-harness/recursive_initialization.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ class recursive_initializationt
6060
public:
6161
using recursion_sett = std::set<irep_idt>;
6262
using type_constructor_namest = std::map<typet, irep_idt>;
63+
using equal_cluster_idt = std::size_t;
6364

6465
recursive_initializationt(
6566
recursive_initialization_configt initialization_config,
@@ -102,7 +103,7 @@ class recursive_initializationt
102103
symbol_exprt get_malloc_function();
103104

104105
bool should_be_treated_as_array(const irep_idt &pointer_name) const;
105-
optionalt<std::size_t> find_equal_cluster(const irep_idt &name) const;
106+
optionalt<equal_cluster_idt> find_equal_cluster(const irep_idt &name) const;
106107
bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
107108
optionalt<irep_idt>
108109
get_associated_size_variable(const irep_idt &array_name) const;

0 commit comments

Comments
 (0)