Skip to content

Commit 7ff3d66

Browse files
committed
Make property numbering and show-properties fully deterministic
Use lexicographic ordering when iterating over goto functions to avoid property numbers (or the order in which they printed) to depend on hash values.
1 parent 413854f commit 7ff3d66

File tree

2 files changed

+12
-8
lines changed

2 files changed

+12
-8
lines changed

src/goto-programs/set_properties.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -131,9 +131,7 @@ void label_properties(goto_functionst &goto_functions)
131131
{
132132
std::map<irep_idt, std::size_t> property_counters;
133133

134-
for(goto_functionst::function_mapt::iterator
135-
it=goto_functions.function_map.begin();
136-
it!=goto_functions.function_map.end();
137-
it++)
134+
auto sorted = goto_functions.sorted();
135+
for(auto &it : sorted)
138136
label_properties(it->first, it->second.body, property_counters);
139137
}

src/goto-programs/show_properties.cpp

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,10 @@ void show_properties_json(
180180
messaget msg(message_handler);
181181
json_arrayt json_properties;
182182

183-
for(const auto &fct : goto_functions.function_map)
184-
convert_properties_json(json_properties, ns, fct.first, fct.second.body);
183+
// sort alphabetically
184+
const auto sorted = goto_functions.sorted();
185+
for(const auto &it : sorted)
186+
convert_properties_json(json_properties, ns, it->first, it->second.body);
185187

186188
json_objectt json_result{{"properties", json_properties}};
187189
msg.result() << json_result;
@@ -196,8 +198,12 @@ void show_properties(
196198
if(ui == ui_message_handlert::uit::JSON_UI)
197199
show_properties_json(ns, ui_message_handler, goto_functions);
198200
else
199-
for(const auto &fct : goto_functions.function_map)
200-
show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
201+
{
202+
// sort alphabetically
203+
const auto sorted = goto_functions.sorted();
204+
for(const auto &it : sorted)
205+
show_properties(ns, it->first, ui_message_handler, ui, it->second.body);
206+
}
201207
}
202208

203209
void show_properties(

0 commit comments

Comments
 (0)