CBMC
|
Bounded Model Checking Utilities. More...
#include "report_util.h"
#include <algorithm>
#include <util/json.h>
#include <util/json_irep.h>
#include <util/json_stream.h>
#include <util/string2int.h>
#include <util/ui_message.h>
#include <util/xml.h>
#include <util/xml_irep.h>
#include <goto-programs/json_goto_trace.h>
#include <goto-programs/xml_goto_trace.h>
#include "fault_localization_provider.h"
#include "goto_trace_storage.h"
#include "bmc_util.h"
Go to the source code of this file.
Typedefs | |
using | propertyt = std::pair< irep_idt, property_infot > |
Bounded Model Checking Utilities.
Definition in file report_util.cpp.
using propertyt = std::pair<irep_idt, property_infot> |
Definition at line 183 of file report_util.cpp.
|
static |
Definition at line 246 of file report_util.cpp.
|
static |
Compare two properties according to the following sort:
property1 | The first property. |
property2 | The second propery. |
Definition at line 194 of file report_util.cpp.
|
static |
Definition at line 521 of file report_util.cpp.
|
static |
Definition at line 437 of file report_util.cpp.
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 | ||
) |
Definition at line 633 of file report_util.cpp.
|
static |
Definition at line 452 of file report_util.cpp.
|
static |
Definition at line 471 of file report_util.cpp.
void output_fault_localization_scores | ( | const fault_location_infot & | fault_location, |
messaget & | log | ||
) |
Definition at line 421 of file report_util.cpp.
|
static |
Definition at line 507 of file report_util.cpp.
|
static |
Definition at line 294 of file report_util.cpp.
void output_overall_result | ( | resultt | result, |
ui_message_handlert & | ui_message_handler | ||
) |
Definition at line 677 of file report_util.cpp.
void output_properties | ( | const propertiest & | properties, |
std::size_t | iterations, | ||
ui_message_handlert & | ui_message_handler | ||
) |
Definition at line 308 of file report_util.cpp.
|
static |
Definition at line 261 of file report_util.cpp.
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 | ||
) |
Definition at line 536 of file report_util.cpp.
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 | ||
) |
Definition at line 346 of file report_util.cpp.
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 | ||
) |
Definition at line 579 of file report_util.cpp.
|
static |
Definition at line 144 of file report_util.cpp.
void report_error | ( | ui_message_handlert & | ui_message_handler | ) |
Definition at line 116 of file report_util.cpp.
void report_failure | ( | ui_message_handlert & | ui_message_handler | ) |
Definition at line 60 of file report_util.cpp.
void report_inconclusive | ( | ui_message_handlert & | ui_message_handler | ) |
Definition at line 88 of file report_util.cpp.
void report_success | ( | ui_message_handlert & | ui_message_handler | ) |
Definition at line 32 of file report_util.cpp.
|
static |
Definition at line 483 of file report_util.cpp.