cprover
Loading...
Searching...
No Matches
report_util.cpp File Reference

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"
+ Include dependency graph for report_util.cpp:

Go to the source code of this file.

Typedefs

using propertyt = std::pair<irep_idt, property_infot>
 

Functions

void report_success (ui_message_handlert &ui_message_handler)
 
void report_failure (ui_message_handlert &ui_message_handler)
 
void report_inconclusive (ui_message_handlert &ui_message_handler)
 
void report_error (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())
 
static bool is_property_less_than (const propertyt &property1, const propertyt &property2)
 Compare two properties according to the following sort:
 
static std::vector< propertiest::const_iterator > get_sorted_properties (const propertiest &properties)
 
static void output_properties_plain (const std::vector< propertiest::const_iterator > &sorted_properties, messaget &log)
 
static void output_iterations (const propertiest &properties, std::size_t iterations, messaget &log)
 
void output_properties (const propertiest &properties, std::size_t iterations, 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 goto_programt::const_targett max_fault_localization_score (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)
 
static void output_fault_localization_plain (const std::unordered_map< irep_idt, fault_location_infot > &fault_locations, messaget &log)
 
static xmlt xml (const irep_idt &property_id, 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)
 
static json_objectt json (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)
 
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_overall_result (resultt result, ui_message_handlert &ui_message_handler)
 

Detailed Description

Bounded Model Checking Utilities.

Definition in file report_util.cpp.

Typedef Documentation

◆ propertyt

using propertyt = std::pair<irep_idt, property_infot>

Definition at line 183 of file report_util.cpp.

Function Documentation

◆ get_sorted_properties()

static std::vector< propertiest::const_iterator > get_sorted_properties ( const propertiest & properties)
static

Definition at line 246 of file report_util.cpp.

◆ is_property_less_than()

static bool is_property_less_than ( const propertyt & property1,
const propertyt & property2 )
static

Compare two properties according to the following sort:

  1. alphabetical ordering of file name
  2. alphabetical ordering of function name
  3. numerical ordering of line number
  4. alphabetical ordering of goal ID
  5. number ordering of the goal ID number
    Parameters
    property1The first property.
    property2The second propery.
    Returns
    True if the first property is less than the second property

Definition at line 194 of file report_util.cpp.

◆ json()

static json_objectt json ( const fault_location_infot & fault_location)
static

Definition at line 521 of file report_util.cpp.

◆ max_fault_localization_score()

static goto_programt::const_targett max_fault_localization_score ( const fault_location_infot & fault_location)
static

Definition at line 437 of file report_util.cpp.

◆ output_error_trace_with_fault_localization()

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.

◆ output_fault_localization_plain() [1/2]

static void output_fault_localization_plain ( const irep_idt & property_id,
const fault_location_infot & fault_location,
messaget & log )
static

Definition at line 452 of file report_util.cpp.

◆ output_fault_localization_plain() [2/2]

static void output_fault_localization_plain ( const std::unordered_map< irep_idt, fault_location_infot > & fault_locations,
messaget & log )
static

Definition at line 471 of file report_util.cpp.

◆ output_fault_localization_scores()

void output_fault_localization_scores ( const fault_location_infot & fault_location,
messaget & log )

Definition at line 421 of file report_util.cpp.

◆ output_fault_localization_xml()

static void output_fault_localization_xml ( const std::unordered_map< irep_idt, fault_location_infot > & fault_locations,
messaget & log )
static

Definition at line 507 of file report_util.cpp.

◆ output_iterations()

static void output_iterations ( const propertiest & properties,
std::size_t iterations,
messaget & log )
static

Definition at line 294 of file report_util.cpp.

◆ output_overall_result()

void output_overall_result ( resultt result,
ui_message_handlert & ui_message_handler )

Definition at line 677 of file report_util.cpp.

◆ output_properties()

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.

◆ output_properties_plain()

static void output_properties_plain ( const std::vector< propertiest::const_iterator > & sorted_properties,
messaget & log )
static

Definition at line 261 of file report_util.cpp.

◆ output_properties_with_fault_localization()

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.

◆ output_properties_with_traces()

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.

◆ output_properties_with_traces_and_fault_localization()

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.

◆ output_single_property_plain()

static void output_single_property_plain ( const irep_idt & property_id,
const property_infot & property_info,
messaget & log,
irep_idt current_file = irep_idt() )
static

Definition at line 144 of file report_util.cpp.

◆ report_error()

void report_error ( ui_message_handlert & ui_message_handler)

Definition at line 116 of file report_util.cpp.

◆ report_failure()

void report_failure ( ui_message_handlert & ui_message_handler)

Definition at line 60 of file report_util.cpp.

◆ report_inconclusive()

void report_inconclusive ( ui_message_handlert & ui_message_handler)

Definition at line 88 of file report_util.cpp.

◆ report_success()

void report_success ( ui_message_handlert & ui_message_handler)

Definition at line 32 of file report_util.cpp.

◆ xml()

static xmlt xml ( const irep_idt & property_id,
const fault_location_infot & fault_location,
messaget & log )
static

Definition at line 483 of file report_util.cpp.