Decorator for a message_handlert used during function inlining that collect names of GOTO functions creating warnings and allows to turn inlining warnings into hard errors. More...

#include <inlining_decorator.h>

Inheritance diagram for inlining_decoratort:

Collaboration diagram for inlining_decoratort:

Public Member Functions
	inlining_decoratort (message_handlert &_wrapped)

void	throw_on_no_body (messaget &log, const int error_code)
	Throws the given error code if `no body for function` warnings happend during inlining. More...

void	throw_on_recursive_calls (messaget &log, const int error_code)
	Throws the given error code if `recursive call` warnings happend during inlining. More...

void	throw_on_missing_function (messaget &log, const int error_code)
	Throws the given error code if `missing function` warnings happend during inlining. More...

void	throw_on_not_enough_arguments (messaget &log, const int error_code)
	Throws the given error code if `not enough arguments` warnings happend during inlining. More...

const std::set< irep_idt > &	get_no_body_set () const

const std::set< irep_idt > &	get_missing_function_set () const

const std::set< irep_idt > &	get_recursive_call_set () const

const std::set< irep_idt > &	get_not_enough_arguments_set () const

void	print (unsigned level, const std::string &message) override

void	print (unsigned level, const xmlt &xml) override

void	print (unsigned level, const jsont &json) override

void	print (unsigned level, const structured_datat &data) override

void	print (unsigned level, const std::string &message, const source_locationt &location) override

void	flush (unsigned i) override

void	set_verbosity (unsigned _verbosity)

unsigned	get_verbosity () const

std::size_t	get_message_count (unsigned level) const

std::string	command (unsigned i) const override
	Create an ECMA-48 SGR (Select Graphic Rendition) command. More...

Public Member Functions inherited from message_handlert
	message_handlert ()

virtual	~message_handlert ()

void	set_verbosity (unsigned _verbosity)

unsigned	get_verbosity () const

std::size_t	get_message_count (unsigned level) const

Private Member Functions
void	match_no_body_warning (const std::string &message)

void	match_missing_function_warning (const std::string &message)

void	match_recursive_call_warning (const std::string &message)

void	match_not_enough_arguments_warning (const std::string &message)

void	parse_message (const std::string &message)

Private Attributes
message_handlert &	wrapped

std::regex	no_body_regex

std::set< irep_idt >	no_body_set

std::regex	missing_function_regex

std::set< irep_idt >	missing_function_set

std::regex	recursive_call_regex

std::set< irep_idt >	recursive_call_set

std::regex	not_enough_arguments_regex

std::set< irep_idt >	not_enough_arguments_set

Additional Inherited Members
Protected Attributes inherited from message_handlert
unsigned	verbosity

std::vector< std::size_t >	message_count

Detailed Description

Decorator for a message_handlert used during function inlining that collect names of GOTO functions creating warnings and allows to turn inlining warnings into hard errors.

The decorator intercepts and parses messages sent to the decorated message handler and collects the names of GOTO functions involved in these 4 types warnings:

recursive call warnings,
missing function warnings,
not enough arguments warnings,
no body for function warnings.

For each warning type, the decorator offers:

a method that returns the set of function names that caused the warnings
a method that throws an error in case that set is not empty

So this decorator allows to inspect the sets of functions involved in warnings to check if the warnings are expected or not, and to turn warnings into hard errors if desired.

Decorator pattern info: https://en.wikipedia.org/wiki/Decorator_pattern

Definition at line 42 of file inlining_decorator.h.

Constructor & Destructor Documentation

◆ inlining_decoratort()

inlining_decoratort::inlining_decoratort ( message_handlert & _wrapped )

explicit

Definition at line 13 of file inlining_decorator.cpp.

Member Function Documentation

◆ command()

std::string inlining_decoratort::command ( unsigned ) const

inlineoverridevirtual

Create an ECMA-48 SGR (Select Graphic Rendition) command.

The default behavior is no action.

Reimplemented from message_handlert.

Definition at line 159 of file inlining_decorator.h.

◆ flush()

void inlining_decoratort::flush ( unsigned i )

inlineoverridevirtual

Implements message_handlert.

Definition at line 139 of file inlining_decorator.h.

◆ get_message_count()

std::size_t inlining_decoratort::get_message_count ( unsigned level ) const

inline

Definition at line 154 of file inlining_decorator.h.

◆ get_missing_function_set()

const std::set<irep_idt>& inlining_decoratort::get_missing_function_set ( ) const

inline

Definition at line 93 of file inlining_decorator.h.

◆ get_no_body_set()

const std::set<irep_idt>& inlining_decoratort::get_no_body_set ( ) const

inline

Definition at line 88 of file inlining_decorator.h.

◆ get_not_enough_arguments_set()

const std::set<irep_idt>& inlining_decoratort::get_not_enough_arguments_set ( ) const

inline

Definition at line 103 of file inlining_decorator.h.

◆ get_recursive_call_set()

const std::set<irep_idt>& inlining_decoratort::get_recursive_call_set ( ) const

inline

Definition at line 98 of file inlining_decorator.h.

◆ get_verbosity()

unsigned inlining_decoratort::get_verbosity ( ) const

inline

Definition at line 149 of file inlining_decorator.h.

◆ match_missing_function_warning()

void inlining_decoratort::match_missing_function_warning ( const std::string & message )

private

Definition at line 33 of file inlining_decorator.cpp.

◆ match_no_body_warning()

void inlining_decoratort::match_no_body_warning ( const std::string & message )

private

Definition at line 25 of file inlining_decorator.cpp.

◆ match_not_enough_arguments_warning()

void inlining_decoratort::match_not_enough_arguments_warning ( const std::string & message )

private

Definition at line 51 of file inlining_decorator.cpp.

◆ match_recursive_call_warning()

void inlining_decoratort::match_recursive_call_warning ( const std::string & message )

private

Definition at line 42 of file inlining_decorator.cpp.

◆ parse_message()

void inlining_decoratort::parse_message ( const std::string & message )

private

Definition at line 60 of file inlining_decorator.cpp.

◆ print() [1/5]

void inlining_decoratort::print	(	unsigned	level,
		const jsont &	json
	)

inlineoverridevirtual

Implements message_handlert.

Definition at line 119 of file inlining_decorator.h.

◆ print() [2/5]

void inlining_decoratort::print	(	unsigned	level,
		const std::string &	message
	)

inlineoverridevirtual

Implements message_handlert.

Definition at line 108 of file inlining_decorator.h.

◆ print() [3/5]

void inlining_decoratort::print	(	unsigned	level,
		const std::string &	message,
		const source_locationt &	location
	)

inlineoverridevirtual

Reimplemented from message_handlert.

Definition at line 129 of file inlining_decorator.h.

◆ print() [4/5]

void inlining_decoratort::print	(	unsigned	level,
		const structured_datat &	data
	)

inlineoverridevirtual

Reimplemented from message_handlert.

Definition at line 124 of file inlining_decorator.h.

◆ print() [5/5]

void inlining_decoratort::print	(	unsigned	level,
		const xmlt &	xml
	)

inlineoverridevirtual

Implements message_handlert.

Definition at line 114 of file inlining_decorator.h.

◆ set_verbosity()

void inlining_decoratort::set_verbosity ( unsigned _verbosity )

inline

Definition at line 144 of file inlining_decorator.h.

◆ throw_on_missing_function()

void inlining_decoratort::throw_on_missing_function	(	messaget &	log,
		const int	error_code
	)

Throws the given error code if missing function warnings happend during inlining.

Definition at line 96 of file inlining_decorator.cpp.

◆ throw_on_no_body()

void inlining_decoratort::throw_on_no_body	(	messaget &	log,
		const int	error_code
	)

Throws the given error code if no body for function warnings happend during inlining.

Definition at line 68 of file inlining_decorator.cpp.

◆ throw_on_not_enough_arguments()

void inlining_decoratort::throw_on_not_enough_arguments	(	messaget &	log,
		const int	error_code
	)

Throws the given error code if not enough arguments warnings happend during inlining.

Definition at line 111 of file inlining_decorator.cpp.

◆ throw_on_recursive_calls()

void inlining_decoratort::throw_on_recursive_calls	(	messaget &	log,
		const int	error_code
	)

Throws the given error code if recursive call warnings happend during inlining.

Definition at line 81 of file inlining_decorator.cpp.

Member Data Documentation

◆ missing_function_regex

std::regex inlining_decoratort::missing_function_regex

private

Definition at line 52 of file inlining_decorator.h.

◆ missing_function_set

std::set<irep_idt> inlining_decoratort::missing_function_set

private

Definition at line 53 of file inlining_decorator.h.

◆ no_body_regex

std::regex inlining_decoratort::no_body_regex

private

Definition at line 47 of file inlining_decorator.h.

◆ no_body_set

std::set<irep_idt> inlining_decoratort::no_body_set

private

Definition at line 48 of file inlining_decorator.h.

◆ not_enough_arguments_regex

std::regex inlining_decoratort::not_enough_arguments_regex

private

Definition at line 62 of file inlining_decorator.h.

◆ not_enough_arguments_set

std::set<irep_idt> inlining_decoratort::not_enough_arguments_set

private

Definition at line 63 of file inlining_decorator.h.

◆ recursive_call_regex

std::regex inlining_decoratort::recursive_call_regex

private

Definition at line 57 of file inlining_decorator.h.

◆ recursive_call_set

std::set<irep_idt> inlining_decoratort::recursive_call_set

private

Definition at line 58 of file inlining_decorator.h.

◆ wrapped

message_handlert& inlining_decoratort::wrapped

private

Definition at line 45 of file inlining_decorator.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/contracts/inlining_decorator.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-instrument/contracts/inlining_decorator.cpp

Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ inlining_decoratort()

Member Function Documentation

◆ command()

◆ flush()

◆ get_message_count()

◆ get_missing_function_set()

◆ get_no_body_set()

◆ get_not_enough_arguments_set()

◆ get_recursive_call_set()

◆ get_verbosity()

◆ match_missing_function_warning()

◆ match_no_body_warning()

◆ match_not_enough_arguments_warning()

◆ match_recursive_call_warning()

◆ parse_message()

◆ print() [1/5]

◆ print() [2/5]

◆ print() [3/5]

◆ print() [4/5]

◆ print() [5/5]

◆ set_verbosity()

◆ throw_on_missing_function()

◆ throw_on_no_body()

◆ throw_on_not_enough_arguments()

◆ throw_on_recursive_calls()

Member Data Documentation

◆ missing_function_regex

◆ missing_function_set

◆ no_body_regex

◆ no_body_set

◆ not_enough_arguments_regex

◆ not_enough_arguments_set

◆ recursive_call_regex

◆ recursive_call_set

◆ wrapped