#include <goto-programs/property_verdict.h>
#include <functional>
#include <map>
#include <set>
#include <string>
#include <vector>

Include dependency graph for property_report.h:

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

Classes
struct	property_rowt
	One line of the property report: a verdict together with everything needed to order and print it. More...
struct	property_countst
	How many properties reached each verdict, and how wide the id and line columns must be to line the rows up. More...

Functions
property_countst	count_properties (const std::vector< property_rowt > &rows)
const char *	verdict_label (property_verdictt)
	Fixed-width label for a verdict, e.g. "PASSED", "NOT CHECKED".
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.
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
	The note on a claim no path reached within the bound.

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 )

◆ 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

extern

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

It holds vacuously, so it is recorded as passed, but the run never tested it (#7503).