Skip to content

Commit 228e765

Browse files
Rename current_count method to latest_index
current_count could sound related to count which has a different meaning from what this method returns.
1 parent b5ed1f8 commit 228e765

File tree

4 files changed

+5
-5
lines changed

4 files changed

+5
-5
lines changed

src/goto-symex/goto_symex_state.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -437,7 +437,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
437437
if(a_s_read.second.empty())
438438
{
439439
increase_generation(l1_identifier, ssa_l1);
440-
a_s_read.first=level2.current_count(l1_identifier);
440+
a_s_read.first = level2.latest_index(l1_identifier);
441441
}
442442
const renamedt<ssa_exprt, L2> l2_false_case = set_indices<L2>(ssa_l1, ns);
443443

src/goto-symex/renaming_level.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ operator()(renamedt<ssa_exprt, L1> l1_expr) const
112112
{
113113
if(!l1_expr.get().get_level_2().empty())
114114
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
115-
l1_expr.value().set_level_2(current_count(l1_expr.get().get_identifier()));
115+
l1_expr.value().set_level_2(latest_index(l1_expr.get().get_identifier()));
116116
return renamedt<ssa_exprt, L2>{std::move(l1_expr.value())};
117117
}
118118

@@ -137,7 +137,7 @@ void symex_level1t::restore_from(const symex_level1t &other)
137137
}
138138
}
139139

140-
unsigned symex_level2t::current_count(const irep_idt &identifier) const
140+
unsigned symex_level2t::latest_index(const irep_idt &identifier) const
141141
{
142142
const auto r_opt = current_names.find(identifier);
143143
return !r_opt ? 0 : r_opt->get().second;

src/goto-symex/renaming_level.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ struct symex_level2t
9292
renamedt<ssa_exprt, L2> operator()(renamedt<ssa_exprt, L1> l1_expr) const;
9393

9494
/// Counter corresponding to an identifier
95-
unsigned current_count(const irep_idt &identifier) const;
95+
unsigned latest_index(const irep_idt &identifier) const;
9696
};
9797

9898
/// Undo all levels of renaming

src/goto-symex/symex_atomic_section.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ void goto_symext::symex_atomic_end(statet &state)
7070
for(const auto &pair : state.written_in_atomic_section)
7171
{
7272
ssa_exprt w = pair.first;
73-
w.set_level_2(state.get_level2().current_count(w.get_identifier()));
73+
w.set_level_2(state.get_level2().latest_index(w.get_identifier()));
7474

7575
// guard is the disjunction over writes
7676
PRECONDITION(!pair.second.empty());

0 commit comments

Comments
 (0)