File tree 1 file changed +5
-10
lines changed
1 file changed +5
-10
lines changed Original file line number Diff line number Diff line change @@ -1185,25 +1185,20 @@ void linkingt::do_type_dependencies(
1185
1185
}
1186
1186
}
1187
1187
1188
- std::stack<irep_idt> queue;
1189
-
1190
- for (std::unordered_set<irep_idt>::const_iterator d_it =
1191
- needs_to_be_renamed.begin ();
1192
- d_it != needs_to_be_renamed.end ();
1193
- d_it++)
1194
- queue.push (*d_it);
1188
+ std::deque<irep_idt> queue (
1189
+ needs_to_be_renamed.begin (), needs_to_be_renamed.end ());
1195
1190
1196
1191
while (!queue.empty ())
1197
1192
{
1198
- irep_idt id = queue.top ();
1199
- queue.pop ();
1193
+ irep_idt id = queue.back ();
1194
+ queue.pop_back ();
1200
1195
1201
1196
const std::unordered_set<irep_idt> &u = used_by[id];
1202
1197
1203
1198
for (const auto &dep : u)
1204
1199
if (needs_to_be_renamed.insert (dep).second )
1205
1200
{
1206
- queue.push (dep);
1201
+ queue.push_back (dep);
1207
1202
#ifdef DEBUG
1208
1203
debug () << " LINKING: needs to be renamed (dependency): "
1209
1204
<< dep << eom;
You can’t perform that action at this time.
0 commit comments