#include <cstdlib>
#include <sstream>
#include <stdexcept>
#include <string>
#include <type_traits>

Include dependency graph for invariant.h:

Classes
class	invariant_failedt
	A logic error, augmented with a distinguished field to hold a backtrace. More...

class	invariant_with_diagnostics_failedt
	A class that includes diagnostic information related to an invariant violation. More...

struct	detail::always_falset< T >

struct	diagnostics_helpert< T >
	Helper to give us some diagnostic in a usable form on assertion failure. More...

struct	diagnostics_helpert< char[N]>

struct	diagnostics_helpert< char * >

struct	diagnostics_helpert< std::string >

Namespaces
	detail

Macros
#define	CBMC_NORETURN

#define	EXPAND_MACRO(x) x

#define	CURRENT_FUNCTION_NAME __func__

#define	INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...)

#define	INVARIANT(CONDITION, REASON)
	This macro uses the wrapper function 'invariant_violated_string'. More...

#define	INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...)
	Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a specialisation for invariant_helpert This macro uses the wrapper function 'report_invariant_failure'. More...

#define	PRECONDITION(CONDITION) INVARIANT(CONDITION, "Precondition")

#define	PRECONDITION_WITH_DIAGNOSTICS(CONDITION, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)

#define	PRECONDITION_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

#define	POSTCONDITION(CONDITION) INVARIANT(CONDITION, "Postcondition")

#define	POSTCONDITION_WITH_DIAGNOSTICS(CONDITION, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)

#define	POSTCONDITION_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

#define	CHECK_RETURN(CONDITION) INVARIANT(CONDITION, "Check return value")

#define	CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)

#define	CHECK_RETURN_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

#define	UNREACHABLE INVARIANT(false, "Unreachable")
	This should be used to mark dead code. More...

#define	UNREACHABLE_STRUCTURED(TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))

#define	DATA_INVARIANT(CONDITION, REASON) INVARIANT(CONDITION, REASON)
	This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc. More...

#define	DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, ...) INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)

#define	DATA_INVARIANT_STRUCTURED(CONDITION, TYPENAME, ...) EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

#define	TODO INVARIANT(false, "Todo")

#define	UNIMPLEMENTED INVARIANT(false, "Unimplemented")

#define	UNHANDLED_CASE INVARIANT(false, "Unhandled case")

Functions
void	print_backtrace (std::ostream &out)
	Prints a back trace to 'out'. More...

std::string	get_backtrace ()
	Returns a backtrace. More...

void	report_exception_to_stderr (const invariant_failedt &)
	Dump exception report to stderr. More...

template<class ET , typename... Params>
std::enable_if< std::is_base_of< invariant_failedt, ET >::value >::type	invariant_violated_structured (const std::string &file, const std::string &function, const int line, const std::string &condition, Params &&... params)
	This function is the backbone of all the invariant types. More...

void	invariant_violated_string (const std::string &file, const std::string &function, const int line, const std::string &condition, const std::string &reason)
	This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'. More...

std::string	detail::assemble_diagnostics ()

template<typename T >
std::string	detail::diagnostic_as_string (T &&val)

void	detail::write_rest_diagnostics (std::ostream &)

template<typename T , typename... Ts>
void	detail::write_rest_diagnostics (std::ostream &out, T &&next, Ts &&... rest)

template<typename... Diagnostics>
std::string	detail::assemble_diagnostics (Diagnostics &&... args)

template<typename... Diagnostics>
void	report_invariant_failure (const std::string &file, const std::string &function, int line, std::string reason, std::string condition, Diagnostics &&... diagnostics)
	This is a wrapper function, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'. More...

Macro Definition Documentation

◆ CBMC_NORETURN

#define CBMC_NORETURN

Definition at line 157 of file invariant.h.

◆ CHECK_RETURN

#define CHECK_RETURN ( CONDITION ) INVARIANT(CONDITION, "Check return value")

Definition at line 470 of file invariant.h.

◆ CHECK_RETURN_STRUCTURED

#define CHECK_RETURN_STRUCTURED	(	CONDITION,
		TYPENAME,
		...
	)	EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

Definition at line 474 of file invariant.h.

◆ CHECK_RETURN_WITH_DIAGNOSTICS

#define CHECK_RETURN_WITH_DIAGNOSTICS	(	CONDITION,
		...
	)	INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Check return value", __VA_ARGS__)

Definition at line 471 of file invariant.h.

◆ CURRENT_FUNCTION_NAME

#define CURRENT_FUNCTION_NAME __func__

Definition at line 379 of file invariant.h.

◆ DATA_INVARIANT

#define DATA_INVARIANT	(	CONDITION,
		REASON
	)	INVARIANT(CONDITION, REASON)

This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.

being well formed. "The data structure is not corrupt or malformed"

Definition at line 485 of file invariant.h.

◆ DATA_INVARIANT_STRUCTURED

#define DATA_INVARIANT_STRUCTURED	(	CONDITION,
		TYPENAME,
		...
	)	EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

Definition at line 489 of file invariant.h.

◆ DATA_INVARIANT_WITH_DIAGNOSTICS

#define DATA_INVARIANT_WITH_DIAGNOSTICS	(	CONDITION,
		REASON,
		...
	)	INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON, __VA_ARGS__)

Definition at line 486 of file invariant.h.

◆ EXPAND_MACRO

#define EXPAND_MACRO ( x ) x

Definition at line 371 of file invariant.h.

◆ INVARIANT

#define INVARIANT	(	CONDITION,
		REASON
	)

Value:

do                                                                           \
  {                                                                            \
    if(!(CONDITION))                                                           \
    {                                                                          \
      invariant_violated_string(                                               \
        __FILE__, CURRENT_FUNCTION_NAME, __LINE__, #CONDITION, REASON);        \
    }                                                                          \
  } while(false)

This macro uses the wrapper function 'invariant_violated_string'.

Definition at line 400 of file invariant.h.

◆ INVARIANT_STRUCTURED

#define INVARIANT_STRUCTURED	(	CONDITION,
		TYPENAME,
		...
	)

Value:

do /* NOLINT */                                                              \
  {                                                                            \
    if(!(CONDITION))                                                           \
      invariant_violated_structured<TYPENAME>(                                 \
        __FILE__,                                                              \
        CURRENT_FUNCTION_NAME,                                                 \
        __LINE__,                                                              \
        #CONDITION,                                                            \
        __VA_ARGS__); /* NOLINT */                                             \
  } while(false)

Definition at line 382 of file invariant.h.

◆ INVARIANT_WITH_DIAGNOSTICS

#define INVARIANT_WITH_DIAGNOSTICS	(	CONDITION,
		REASON,
		...
	)

Value:

do                                                                           \
  {                                                                            \
    if(!(CONDITION))                                                           \
    {                                                                          \
      report_invariant_failure(                                                \
        __FILE__,                                                              \
        CURRENT_FUNCTION_NAME,                                                 \
        __LINE__,                                                              \
        REASON,                                                                \
        #CONDITION,                                                            \
        __VA_ARGS__);                                                          \
    }                                                                          \
  } while(false)

Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a specialisation for invariant_helpert This macro uses the wrapper function 'report_invariant_failure'.

Definition at line 414 of file invariant.h.

◆ POSTCONDITION

#define POSTCONDITION ( CONDITION ) INVARIANT(CONDITION, "Postcondition")

Definition at line 454 of file invariant.h.

◆ POSTCONDITION_STRUCTURED

#define POSTCONDITION_STRUCTURED	(	CONDITION,
		TYPENAME,
		...
	)	EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

Definition at line 458 of file invariant.h.

◆ POSTCONDITION_WITH_DIAGNOSTICS

#define POSTCONDITION_WITH_DIAGNOSTICS	(	CONDITION,
		...
	)	INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Postcondition", __VA_ARGS__)

Definition at line 455 of file invariant.h.

◆ PRECONDITION

#define PRECONDITION ( CONDITION ) INVARIANT(CONDITION, "Precondition")

Definition at line 438 of file invariant.h.

◆ PRECONDITION_STRUCTURED

#define PRECONDITION_STRUCTURED	(	CONDITION,
		TYPENAME,
		...
	)	EXPAND_MACRO(INVARIANT_STRUCTURED(CONDITION, TYPENAME, __VA_ARGS__))

Definition at line 442 of file invariant.h.

◆ PRECONDITION_WITH_DIAGNOSTICS

#define PRECONDITION_WITH_DIAGNOSTICS	(	CONDITION,
		...
	)	INVARIANT_WITH_DIAGNOSTICS(CONDITION, "Precondition", __VA_ARGS__)

Definition at line 439 of file invariant.h.

◆ TODO

#define TODO INVARIANT(false, "Todo")

Definition at line 496 of file invariant.h.

◆ UNHANDLED_CASE

#define UNHANDLED_CASE INVARIANT(false, "Unhandled case")

Definition at line 498 of file invariant.h.

◆ UNIMPLEMENTED

#define UNIMPLEMENTED INVARIANT(false, "Unimplemented")

Definition at line 497 of file invariant.h.

◆ UNREACHABLE

#define UNREACHABLE INVARIANT(false, "Unreachable")

This should be used to mark dead code.

Definition at line 478 of file invariant.h.

◆ UNREACHABLE_STRUCTURED

#define UNREACHABLE_STRUCTURED	(	TYPENAME,
		...
	)	EXPAND_MACRO(INVARIANT_STRUCTURED(false, TYPENAME, __VA_ARGS__))

Definition at line 479 of file invariant.h.

Function Documentation

◆ get_backtrace()

std::string get_backtrace ( )

Returns a backtrace.

Returns: backtrace with a file / function / line header.

Definition at line 102 of file invariant.cpp.

◆ invariant_violated_string()

void invariant_violated_string	(	const std::string &	file,
		const std::string &	function,
		const int	line,
		const std::string &	condition,
		const std::string &	reason
	)

inline

This is a wrapper function used by the macro 'INVARIANT(CONDITION, REASON)'.

It constructs an invariant_violatedt from reason and the backtrace, then aborts after printing the invariant's description. In future this may throw rather than aborting.

Parameters

file	: C string giving the name of the file.
function	: C string giving the name of the function.
line	: The line number of the invariant
reason	: brief description of the invariant violation.
condition	: the condition this invariant is checking.

Definition at line 250 of file invariant.h.

◆ invariant_violated_structured()

template<class ET , typename... Params>

std::enable_if<std::is_base_of<invariant_failedt, ET>::value>::type invariant_violated_structured	(	const std::string &	file,
		const std::string &	function,
		const int	line,
		const std::string &	condition,
		Params &&...	params
	)

This function is the backbone of all the invariant types.

Every instance of an invariant is ultimately generated by this function template, which is at times called via a wrapper function. Takes a backtrace, gives it to the reason structure, then aborts, printing reason.what() (which therefore includes the backtrace). In future this may throw reason instead of aborting. Template parameter ET: type of exception to construct

Parameters

file	: C string giving the name of the file.
function	: C string giving the name of the function.
line	: The line number of the invariant
condition	: the condition this invariant is checking.
params	: (variadic) parameters to forward to ET's constructor its backtrace member will be set before it is used.

Definition at line 218 of file invariant.h.

◆ print_backtrace()

void print_backtrace ( std::ostream & out )

Prints a back trace to 'out'.

Parameters

out	Stream to print backtrace

Definition at line 78 of file invariant.cpp.

◆ report_exception_to_stderr()

void report_exception_to_stderr ( const invariant_failedt & )

Dump exception report to stderr.

Definition at line 110 of file invariant.cpp.

◆ report_invariant_failure()

template<typename... Diagnostics>

void report_invariant_failure	(	const std::string &	file,
		const std::string &	function,
		int	line,
		std::string	reason,
		std::string	condition,
		Diagnostics &&...	diagnostics
	)

This is a wrapper function, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'.

Definition at line 354 of file invariant.h.

Classes

Namespaces

Macros

Functions

Macro Definition Documentation

◆ CBMC_NORETURN

◆ CHECK_RETURN

◆ CHECK_RETURN_STRUCTURED

◆ CHECK_RETURN_WITH_DIAGNOSTICS

◆ CURRENT_FUNCTION_NAME

◆ DATA_INVARIANT

◆ DATA_INVARIANT_STRUCTURED

◆ DATA_INVARIANT_WITH_DIAGNOSTICS

◆ EXPAND_MACRO

◆ INVARIANT

◆ INVARIANT_STRUCTURED

◆ INVARIANT_WITH_DIAGNOSTICS

◆ POSTCONDITION

◆ POSTCONDITION_STRUCTURED

◆ POSTCONDITION_WITH_DIAGNOSTICS

◆ PRECONDITION

◆ PRECONDITION_STRUCTURED

◆ PRECONDITION_WITH_DIAGNOSTICS

◆ TODO

◆ UNHANDLED_CASE

◆ UNIMPLEMENTED

◆ UNREACHABLE

◆ UNREACHABLE_STRUCTURED

Function Documentation

◆ get_backtrace()

◆ invariant_violated_string()

◆ invariant_violated_structured()

◆ print_backtrace()

◆ report_exception_to_stderr()

◆ report_invariant_failure()