Skip to content

Commit 8ddbbb7

Browse files
author
thk123
committed
Pull out the compare function
1 parent 13bae95 commit 8ddbbb7

File tree

1 file changed

+63
-53
lines changed

1 file changed

+63
-53
lines changed

src/goto-checker/report_util.cpp

Lines changed: 63 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -181,69 +181,79 @@ static void output_single_property_plain(
181181
<< messaget::eom;
182182
}
183183

184+
using propertyt = std::pair<irep_idt, property_infot>;
185+
/// Compare two properties according to the following sort:
186+
/// 1. alphabetical ordering of file name
187+
/// 2. alphabetical ordering of function name
188+
/// 3. numerical ordering of line number
189+
/// 4. alphabetical ordering of goal ID
190+
/// 5. number ordering of the goal ID number
191+
/// \param pit1: The first property.
192+
/// \param pit2: The second propery.
193+
/// \return True if the first property is less than the second property
194+
static bool is_property_less_than(const propertyt &pit1, const propertyt &pit2)
195+
{
196+
const auto &p1 = pit1.second.pc->source_location;
197+
const auto &p2 = pit2.second.pc->source_location;
198+
if(p1.get_file() != p2.get_file())
199+
return id2string(p1.get_file()) < id2string(p2.get_file());
200+
if(p1.get_function() != p2.get_function())
201+
return id2string(p1.get_function()) < id2string(p2.get_function());
202+
else if(
203+
!p1.get_line().empty() && !p2.get_line().empty() &&
204+
p1.get_line() != p2.get_line())
205+
return std::stoul(id2string(p1.get_line())) <
206+
std::stoul(id2string(p2.get_line()));
207+
208+
const auto split_property_id =
209+
[](const irep_idt &property_id) -> std::pair<std::string, std::size_t> {
210+
const auto property_string = id2string(property_id);
211+
const auto last_dot = property_string.rfind('.');
212+
std::string property_name;
213+
std::string property_number;
214+
if(last_dot == std::string::npos)
215+
{
216+
property_name = "";
217+
property_number = property_string;
218+
}
219+
else
220+
{
221+
property_name = property_string.substr(0, last_dot);
222+
property_number = property_string.substr(last_dot + 1);
223+
}
224+
const auto maybe_number = string2optional_size_t(property_number);
225+
if(maybe_number.has_value())
226+
return std::make_pair(property_name, *maybe_number);
227+
else
228+
return std::make_pair(property_name, 0);
229+
};
230+
231+
const auto left_split = split_property_id(pit1.first);
232+
const auto left_id_name = left_split.first;
233+
const auto left_id_number = left_split.second;
234+
235+
const auto right_split = split_property_id(pit2.first);
236+
const auto right_id_name = left_split.first;
237+
const auto right_id_number = left_split.second;
238+
239+
if(left_id_name != right_id_name)
240+
return left_id_name < right_id_name;
241+
else
242+
return left_id_number < right_id_number;
243+
}
244+
184245
static std::vector<propertiest::const_iterator>
185246
get_sorted_properties(const propertiest &properties)
186247
{
187248
std::vector<propertiest::const_iterator> sorted_properties;
188249
for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
189250
sorted_properties.push_back(p_it);
190-
// now determine an ordering for those goals:
191-
// 1. alphabetical ordering of file name
192-
// 2. alphabetical ordering of function name
193-
// 3. numerical ordering of line number
194-
// 4. alphabetical ordering of goal ID
195-
// 5. number ordering of the goal ID number
251+
196252
std::sort(
197253
sorted_properties.begin(),
198254
sorted_properties.end(),
199255
[](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
200-
const auto &p1 = pit1->second.pc->source_location;
201-
const auto &p2 = pit2->second.pc->source_location;
202-
if(p1.get_file() != p2.get_file())
203-
return id2string(p1.get_file()) < id2string(p2.get_file());
204-
if(p1.get_function() != p2.get_function())
205-
return id2string(p1.get_function()) < id2string(p2.get_function());
206-
else if(
207-
!p1.get_line().empty() && !p2.get_line().empty() &&
208-
p1.get_line() != p2.get_line())
209-
return std::stoul(id2string(p1.get_line())) <
210-
std::stoul(id2string(p2.get_line()));
211-
212-
const auto split_property_id =
213-
[](const irep_idt &property_id) -> std::pair<std::string, std::size_t> {
214-
const auto property_string = id2string(property_id);
215-
const auto last_dot = property_string.rfind('.');
216-
std::string property_name;
217-
std::string property_number;
218-
if(last_dot == std::string::npos)
219-
{
220-
property_name = "";
221-
property_number = property_string;
222-
}
223-
else
224-
{
225-
property_name = property_string.substr(0, last_dot);
226-
property_number = property_string.substr(last_dot + 1);
227-
}
228-
const auto maybe_number = string2optional_size_t(property_number);
229-
if(maybe_number.has_value())
230-
return std::make_pair(property_name, *maybe_number);
231-
else
232-
return std::make_pair(property_name, 0);
233-
};
234-
235-
const auto left_split = split_property_id(pit1->first);
236-
const auto left_id_name = left_split.first;
237-
const auto left_id_number = left_split.second;
238-
239-
const auto right_split = split_property_id(pit2->first);
240-
const auto right_id_name = left_split.first;
241-
const auto right_id_number = left_split.second;
242-
243-
if(left_id_name != right_id_name)
244-
return left_id_name < right_id_name;
245-
else
246-
return left_id_number < right_id_number;
256+
return is_property_less_than(*pit1, *pit2);
247257
});
248258
return sorted_properties;
249259
}

0 commit comments

Comments
 (0)