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:

alphabetical ordering of file name
alphabetical ordering of function name
numerical ordering of line number
alphabetical ordering of goal ID
number ordering of the goal ID number
Parameters

property1 The first property.

property2 The 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.

property1	The first property.
property2	The second propery.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ propertyt

Function Documentation

◆ get_sorted_properties()

◆ is_property_less_than()

◆ json()

◆ max_fault_localization_score()

◆ output_error_trace_with_fault_localization()

◆ output_fault_localization_plain() [1/2]

◆ output_fault_localization_plain() [2/2]

◆ output_fault_localization_scores()

◆ output_fault_localization_xml()

◆ output_iterations()

◆ output_overall_result()

◆ output_properties()

◆ output_properties_plain()

◆ output_properties_with_fault_localization()

◆ output_properties_with_traces()

◆ output_properties_with_traces_and_fault_localization()

◆ output_single_property_plain()

◆ report_error()

◆ report_failure()

◆ report_inconclusive()

◆ report_success()

◆ xml()