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",
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
Bounded Model Checking Utilities.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
instructionst::const_iterator const_targett
Step of the trace of a GOTO program.
const namespacet & get_namespace() const
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Provides methods for streaming JSON arrays.
void push_back(const jsont &json)
Push back a JSON element into the current array stream.
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Provides methods for streaming JSON objects.
void push_back(const std::string &key, const jsont &json)
Push back a JSON element into the current object stream.
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
bool first
Is the current element the first element in the object or array? This is required to know whether a d...
Class that provides messages with a built-in verbosity 'level'.
static const commandt yellow
render text with yellow foreground color
static const commandt magenta
render text with magenta foreground color
static const commandt reset
return to default formatting, as defined by the terminal
mstreamt & status() const
static const commandt green
render text with green foreground color
static const commandt faint
render text with faint font
static const commandt bright_red
render text with bright red foreground color
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
mstreamt & result() const
static const commandt red
render text with red foreground color
static const commandt bright_green
render text with bright green foreground color
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual uit get_ui() const
virtual json_stream_arrayt & get_json_stream()
void set_attribute(const std::string &attribute, unsigned value)
xmlt & new_element(const std::string &key)
Interface for Goto Checkers to provide Fault Localization.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
const std::string & id2string(const irep_idt &d)
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
std::string as_string(resultt result)
@ UNKNOWN
The checker was unable to determine the status of the property.
@ NOT_REACHABLE
The property was proven to be unreachable.
@ PASS
The property was not violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
resultt
The result of goto verifying.
@ UNKNOWN
No property was violated, neither was there an error.
@ PASS
No properties were violated.
@ ERROR
An error occurred during goto checking.
@ FAIL
Some properties were violated.
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
void output_properties(const propertiest &properties, std::size_t iterations, ui_message_handlert &ui_message_handler)
static void output_properties_plain(const std::vector< propertiest::const_iterator > &sorted_properties, messaget &log)
std::pair< irep_idt, property_infot > propertyt
static goto_programt::const_targett max_fault_localization_score(const fault_location_infot &fault_location)
void output_properties_with_fault_localization(const propertiest &properties, const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, std::size_t iterations, ui_message_handlert &ui_message_handler)
void output_properties_with_traces_and_fault_localization(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, std::size_t iterations, ui_message_handlert &ui_message_handler)
static json_objectt json(const fault_location_infot &fault_location)
static void output_fault_localization_plain(const irep_idt &property_id, const fault_location_infot &fault_location, messaget &log)
void report_success(ui_message_handlert &ui_message_handler)
static bool is_property_less_than(const propertyt &property1, const propertyt &property2)
Compare two properties according to the following sort:
static xmlt xml(const irep_idt &property_id, const fault_location_infot &fault_location, messaget &log)
void report_inconclusive(ui_message_handlert &ui_message_handler)
void output_overall_result(resultt result, ui_message_handlert &ui_message_handler)
void output_properties_with_traces(const propertiest &properties, const goto_trace_storaget &traces, const trace_optionst &trace_options, std::size_t iterations, ui_message_handlert &ui_message_handler)
static std::vector< propertiest::const_iterator > get_sorted_properties(const propertiest &properties)
void output_fault_localization_scores(const fault_location_infot &fault_location, messaget &log)
static void output_fault_localization_xml(const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, messaget &log)
void output_error_trace_with_fault_localization(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, const fault_location_infot &fault_location_info, ui_message_handlert &ui_message_handler)
static void output_iterations(const propertiest &properties, std::size_t iterations, messaget &log)
void report_error(ui_message_handlert &ui_message_handler)
void report_failure(ui_message_handlert &ui_message_handler)
static void output_single_property_plain(const irep_idt &property_id, const property_infot &property_info, messaget &log, irep_idt current_file=irep_idt())
Bounded Model Checking Utilities.
#define PRECONDITION(CONDITION)
optionalt< std::size_t > string2optional_size_t(const std::string &str, int base)
Convert string to size_t similar to the stoul or stoull functions, return nullopt when the conversion...
property_statust status
The status of the property.
std::string description
A description (usually derived from the assertion's comment)
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Options for printing the trace using show_goto_trace.