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

Include dependency graph for invariant.h:

Classes
struct	cbmc_invariants_should_throwt
	Helper to enable invariant throwing as above bounded to an object lifetime: More...

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_BECAUSE(REASON) INVARIANT(false, REASON)

#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	UNIMPLEMENTED_FEATURE(FEATURE) INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))

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

Variables
bool	cbmc_invariants_should_throw
	Set this to true to cause invariants to throw a C++ exception rather than abort the program. More...

Macro Definition Documentation

◆ CBMC_NORETURN

#define CBMC_NORETURN

Definition at line 178 of file invariant.h.

◆ CHECK_RETURN

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

Definition at line 495 of file invariant.h.

◆ CHECK_RETURN_STRUCTURED

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

Definition at line 499 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 496 of file invariant.h.

◆ CURRENT_FUNCTION_NAME

#define CURRENT_FUNCTION_NAME __func__

Definition at line 404 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 534 of file invariant.h.

◆ DATA_INVARIANT_STRUCTURED

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

Definition at line 538 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 535 of file invariant.h.

◆ EXPAND_MACRO

#define EXPAND_MACRO ( x ) x

Definition at line 396 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 423 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 407 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 437 of file invariant.h.

◆ POSTCONDITION

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

Definition at line 479 of file invariant.h.

◆ POSTCONDITION_STRUCTURED

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

Definition at line 483 of file invariant.h.

◆ POSTCONDITION_WITH_DIAGNOSTICS

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

Definition at line 480 of file invariant.h.

◆ PRECONDITION

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

Definition at line 463 of file invariant.h.

◆ PRECONDITION_STRUCTURED

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

Definition at line 467 of file invariant.h.

◆ PRECONDITION_WITH_DIAGNOSTICS

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

Definition at line 464 of file invariant.h.

◆ TODO

#define TODO INVARIANT(false, "Todo")

Definition at line 557 of file invariant.h.

◆ UNHANDLED_CASE

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

Definition at line 559 of file invariant.h.

◆ UNIMPLEMENTED

#define UNIMPLEMENTED INVARIANT(false, "Unimplemented")

Definition at line 558 of file invariant.h.

◆ UNIMPLEMENTED_FEATURE

#define UNIMPLEMENTED_FEATURE ( FEATURE ) INVARIANT(false, std::string{"Reached unimplemented "} + (FEATURE))

Definition at line 549 of file invariant.h.

◆ UNREACHABLE

#define UNREACHABLE INVARIANT(false, "Unreachable")

This should be used to mark dead code.

Definition at line 525 of file invariant.h.

◆ UNREACHABLE_BECAUSE

#define UNREACHABLE_BECAUSE ( REASON ) INVARIANT(false, REASON)

Definition at line 526 of file invariant.h.

◆ UNREACHABLE_STRUCTURED

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

Definition at line 527 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 141 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 275 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 239 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 88 of file invariant.cpp.

◆ report_exception_to_stderr()

void report_exception_to_stderr ( const invariant_failedt & reason )

Dump exception report to stderr.

Definition at line 149 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 379 of file invariant.h.

Variable Documentation

◆ cbmc_invariants_should_throw

bool cbmc_invariants_should_throw

extern

Set this to true to cause invariants to throw a C++ exception rather than abort the program.

This is currently untested behaviour, and may fail to clean up partly-completed CBMC operations or release resources. You should probably only use this to gather or report more information about the failure and then abort. Default off.

Definition at line 28 of file invariant.cpp.

Classes

Namespaces

Macros

Functions

Variables

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

◆ UNIMPLEMENTED_FEATURE

◆ UNREACHABLE

◆ UNREACHABLE_BECAUSE

◆ UNREACHABLE_STRUCTURED

Function Documentation

◆ get_backtrace()

◆ invariant_violated_string()

◆ invariant_violated_structured()

◆ print_backtrace()

◆ report_exception_to_stderr()

◆ report_invariant_failure()

Variable Documentation

◆ cbmc_invariants_should_throw