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