#include <esbmc/property_report.h>
#include <goto-programs/goto_functions.h>
#include <util/base/cwe_mapping.h>
#include <algorithm>
#include <tuple>
#include <unordered_map>

Include dependency graph for property_report.cpp:

Functions
const char *	verdict_label (property_verdictt verdict)
	Fixed-width label for a verdict, e.g. "PASSED", "NOT CHECKED".
property_countst	count_properties (const std::vector< property_rowt > &rows)
std::set< std::string >	collect_library_assertion_files (const goto_functionst &goto_functions)
	Source files whose assertions come from a hidden function body, i.e.
static bool	same_position_and_text (const property_rowt &a, const property_rowt &b)
static void	label_by_condition (std::vector< property_rowt >::iterator first, std::vector< property_rowt >::iterator last, const std::function< std::string(const expr2tc &)> &render)
std::vector< property_rowt >	build_property_rows (const std::map< std::string, property_resultt > &verdicts, const std::set< std::string > &library_files, const std::function< std::string(const expr2tc &)> &render_condition)
	Orders `verdicts` by source position – the table itself is keyed on the property description, which sorts alphabetically – and gives each row a stable id of the form <function>.

Variables
const char *const	unreached_claim_note = "never reached"
	The last enumerator falls out to the return below rather than returning in its own arm, so the function needs no unreachable trailing statement to satisfy -Wreturn-type.

Function Documentation

◆ build_property_rows()

std::vector< property_rowt > build_property_rows	(	const std::map< std::string, property_resultt > &	verdicts,
		const std::set< std::string > &	library_files,
		const std::function< std::string(const expr2tc &)> &	render_condition = {} )

Orders verdicts by source position – the table itself is keyed on the property description, which sorts alphabetically – and gives each row a stable id of the form <function>.

<class>.<n>, numbered per function and property class in source order.

Files in library_files sort last, so ESBMC's own operational models do not push the user's code to the bottom of the report; their absolute paths would otherwise sort ahead of a relative one.

The id is a handle for reading and diffing reports. It is deliberately not the number –claim takes: that one counts GOTO assert instructions in function_map order (goto-programs/set_claims.cpp), which is a different sequence from the source order used here. render_condition prints the condition of an assertion whose row would otherwise read the same as another's; without it such rows stay identical.

◆ collect_library_assertion_files()

std::set< std::string > collect_library_assertion_files ( const goto_functionst & goto_functions )

Source files whose assertions come from a hidden function body, i.e.

from one of ESBMC's own operational models rather than the user's code.

◆ count_properties()

property_countst count_properties ( const std::vector< property_rowt > & rows )

◆ label_by_condition()

void label_by_condition	(	std::vector< property_rowt >::iterator	first,
		std::vector< property_rowt >::iterator	last,
		const std::function< std::string(const expr2tc &)> &	render )

static

◆ same_position_and_text()

bool same_position_and_text	(	const property_rowt &	a,
		const property_rowt &	b )

static

◆ verdict_label()

const char * verdict_label ( property_verdictt verdict )

Fixed-width label for a verdict, e.g. "PASSED", "NOT CHECKED".

Variable Documentation

◆ unreached_claim_note

const char* const unreached_claim_note = "never reached"

The last enumerator falls out to the return below rather than returning in its own arm, so the function needs no unreachable trailing statement to satisfy -Wreturn-type.

The note on a claim no path reached within the bound.

Functions

Variables