38 switch(ui_message_handler.
get_ui())
55 msg.
result() << json_result;
66 switch(ui_message_handler.
get_ui())
83 msg.
result() << json_result;
94 switch(ui_message_handler.
get_ui())
110 json_result[
"cProverStatus"] =
json_stringt(
"inconclusive");
111 msg.
result() << json_result;
122 switch(ui_message_handler.
get_ui())
139 msg.
result() << json_result;
151 const auto &l = property_info.
pc->source_location;
154 if(l.get_file() != current_file)
155 log.
result() <<
"file " << l.get_file() <<
' ';
156 if(!l.get_line().empty())
157 log.
result() <<
"line " << l.get_line() <<
' ';
159 switch(property_info.
status)
197 const auto &p1 = property1.second.pc->source_location;
198 const auto &p2 = property2.second.pc->source_location;
199 if(p1.get_file() != p2.get_file())
201 if(p1.get_function() != p2.get_function())
204 !p1.get_line().empty() && !p2.get_line().empty() &&
205 p1.get_line() != p2.get_line())
206 return std::stoul(
id2string(p1.get_line())) <
209 const auto split_property_id =
210 [](
const irep_idt &property_id) -> std::pair<std::string, std::size_t> {
211 const auto property_string =
id2string(property_id);
212 const auto last_dot = property_string.rfind(
'.');
213 std::string property_name;
214 std::string property_number;
215 if(last_dot == std::string::npos)
218 property_number = property_string;
222 property_name = property_string.substr(0, last_dot);
223 property_number = property_string.substr(last_dot + 1);
226 if(maybe_number.has_value())
227 return std::make_pair(property_name, *maybe_number);
229 return std::make_pair(property_name, 0);
232 const auto left_split = split_property_id(property1.first);
233 const auto left_id_name = left_split.first;
234 const auto left_id_number = left_split.second;
236 const auto right_split = split_property_id(property2.first);
237 const auto right_id_name = right_split.first;
238 const auto right_id_number = right_split.second;
240 if(left_id_name != right_id_name)
241 return left_id_name < right_id_name;
243 return left_id_number < right_id_number;
246 static std::vector<propertiest::const_iterator>
249 std::vector<propertiest::const_iterator> sorted_properties;
250 for(
auto p_it = properties.begin(); p_it != properties.end(); p_it++)
251 sorted_properties.push_back(p_it);
254 sorted_properties.begin(),
255 sorted_properties.end(),
256 [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
257 return is_property_less_than(*pit1, *pit2);
259 return sorted_properties;
263 const std::vector<propertiest::const_iterator> &sorted_properties,
266 if(sorted_properties.empty())
273 for(
const auto &p : sorted_properties)
275 const auto &l = p->second.pc->source_location;
276 if(l.get_function() != previous_function)
278 if(!previous_function.
empty())
280 previous_function = l.get_function();
281 if(!previous_function.
empty())
283 current_file = l.get_file();
284 if(!current_file.
empty())
285 log.
result() << current_file <<
' ';
286 if(!l.get_function().empty())
287 log.
result() <<
"function " << l.get_function();
297 std::size_t iterations,
300 if(properties.empty())
305 << properties.size() <<
" failed (" << iterations
311 std::size_t iterations,
315 switch(ui_message_handler.
get_ui())
326 for(
const auto &property_pair : properties)
328 log.
result() <<
xml(property_pair.first, property_pair.second);
338 for(
const auto &property_pair : properties)
340 result_array.
push_back(
json(property_pair.first, property_pair.second));
351 std::size_t iterations,
355 switch(ui_message_handler.
get_ui())
361 for(
const auto &property_it : sorted_properties)
366 <<
"Trace for " << property_it->first <<
":"
371 traces[property_it->first],
381 for(
const auto &property_pair : properties)
383 xmlt xml_result =
xml(property_pair.first, property_pair.second);
388 traces[property_pair.first],
391 log.
result() << xml_result;
401 for(
const auto &property_pair : properties)
405 json(json_property, property_pair.
first, property_pair.second);
410 convert<json_stream_arrayt>(
412 traces[property_pair.first],
428 out <<
"Fault localization scores:" << messaget::eom;
429 for(auto &score_pair : fault_location.scores)
431 out << score_pair.first->source_location
432 <<
"\n score: " << score_pair.second << messaget::eom;
442 return std::max_element(
443 fault_location.
scores.begin(),
444 fault_location.
scores.end(),
446 fault_location_infot::score_mapt::value_type score_pair1,
447 fault_location_infot::score_mapt::value_type score_pair2) {
448 return score_pair1.second < score_pair2.second;
458 if(fault_location.
scores.empty())
472 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
476 for(
const auto fault_location_pair : fault_locations)
479 fault_location_pair.first, fault_location_pair.second, log);
488 xmlt xml_diagnosis(
"diagnosis");
492 if(fault_location.
scores.empty())
495 return xml_diagnosis;
504 return xml_diagnosis;
508 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
511 xmlt dest(
"fault-localization");
512 for(
const auto fault_location_pair : fault_locations)
515 xml(fault_location_pair.first, fault_location_pair.second, log);
524 if(fault_location.
scores.empty())
526 json_result[
"result"] =
json_stringt(
"unable to localize fault");
530 json_result[
"result"] =
538 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
539 std::size_t iterations,
543 switch(ui_message_handler.
get_ui())
557 for(
const auto &property_pair : properties)
561 json(json_property, property_pair.
first, property_pair.second);
565 "diagnosis",
json(fault_locations.at(property_pair.first)));
583 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
584 std::size_t iterations,
588 switch(ui_message_handler.
get_ui())
593 properties, traces, trace_options, iterations, ui_message_handler);
603 for(
const auto &property_pair : properties)
607 json(json_property, property_pair.
first, property_pair.second);
612 convert<json_stream_arrayt>(
614 traces[property_pair.first],
618 "diagnosis",
json(fault_locations.at(property_pair.first)));
626 properties, traces, trace_options, iterations, ui_message_handler);
641 switch(ui_message_handler.
get_ui())
659 convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
660 json_result.
push_back(
"diagnosis",
json(fault_location_info));
668 "fault-localization",