37 switch(ui_message_handler.
get_ui())
65 switch(ui_message_handler.
get_ui())
93 switch(ui_message_handler.
get_ui())
101 xml.data =
"INCONCLUSIVE";
121 switch(ui_message_handler.
get_ui())
154 log.result() <<
"file " << l.get_file() <<
' ';
155 if(!l.get_line().empty())
156 log.result() <<
"line " << l.get_line() <<
' ';
196 const auto &
p1 =
property1.second.pc->source_location();
197 const auto &
p2 =
property2.second.pc->source_location();
198 if(
p1.get_file() !=
p2.get_file())
200 if(
p1.get_function() !=
p2.get_function())
203 !
p1.get_line().empty() && !
p2.get_line().empty() &&
204 p1.get_line() !=
p2.get_line())
209 [](
const irep_idt &property_id) -> std::pair<std::string, std::size_t> {
245static std::vector<propertiest::const_iterator>
249 for(
auto p_it = properties.begin();
p_it != properties.end();
p_it++)
255 [](propertiest::const_iterator
pit1, propertiest::const_iterator
pit2) {
256 return is_property_less_than(*pit1, *pit2);
274 const auto &l = p->second.pc->source_location();
278 log.result() <<
'\n';
285 if(!l.get_function().empty())
286 log.result() <<
"function " << l.get_function();
296 std::size_t iterations,
299 if(properties.empty())
302 log.status() <<
"\n** "
304 << properties.size() <<
" failed (" << iterations
310 std::size_t iterations,
314 switch(ui_message_handler.
get_ui())
350 std::size_t iterations,
354 switch(ui_message_handler.
get_ui())
425 log.conditional_output(
427 out <<
"Fault localization scores:" << messaget::eom;
428 for(auto &score_pair : fault_location.scores)
430 out << score_pair.first->source_location()
431 <<
"\n score: " << score_pair.second << messaget::eom;
441 return std::max_element(
445 fault_location_infot::score_mapt::value_type
score_pair1,
446 fault_location_infot::score_mapt::value_type
score_pair2) {
447 return score_pair1.second < score_pair2.second;
466 <<
"[" +
id2string(property_id) +
"]: \n "
472 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
494 xml_diagnosis.new_element(
"result").data =
"unable to localize fault";
508 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
511 xmlt dest(
"fault-localization");
518 log.result() << dest;
538 const std::unordered_map<irep_idt, fault_location_infot> &fault_locations,
539 std::size_t iterations,
543 switch(ui_message_handler.
get_ui())
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);
626 properties, traces,
trace_options, iterations, ui_message_handler);
641 switch(ui_message_handler.
get_ui())
668 "fault-localization",
671 log.result() << dest;
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_table_baset &symbol_table, message_handlert &message_handler)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
Provides methods for streaming JSON arrays.
Provides methods for streaming JSON objects.
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
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
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()
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.
@ 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)
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
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.
static std::vector< propertiest::const_iterator > get_sorted_properties(const propertiest &properties)
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)
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)
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)
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
std::optional< 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...
Options for printing the trace using show_goto_trace.