Bounded Model Checking Utilities. More...

#include "properties.h"

Include dependency graph for report_util.h:

This graph shows which files directly or indirectly include this file:

Functions
void	report_success (ui_message_handlert &)

void	report_failure (ui_message_handlert &)

void	report_inconclusive (ui_message_handlert &)

void	report_error (ui_message_handlert &)

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_properties_with_fault_localization (const propertiest &properties, const std::unordered_map< irep_idt, fault_location_infot > &, 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 > &, std::size_t iterations, ui_message_handlert &ui_message_handler)

void	output_error_trace_with_fault_localization (const goto_tracet &, const namespacet &, const trace_optionst &, const fault_location_infot &, ui_message_handlert &)

void	output_overall_result (resultt result, ui_message_handlert &ui_message_handler)

Detailed Description

Bounded Model Checking Utilities.

Definition in file report_util.h.

Function Documentation

◆ 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_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_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.

◆ 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.

Functions