cprover
invariant.h File Reference
#include <cstdlib>
#include <sstream>
#include <stdexcept>
#include <string>
#include <type_traits>
+ Include dependency graph for invariant.h:

Go to the source code of this file.

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)
#define CURRENT_FUNCTION_NAME
Definition: invariant.h:379

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__, \
__LINE__, \
__VA_ARGS__); /* NOLINT */ \
} while(false)
#define CURRENT_FUNCTION_NAME
Definition: invariant.h:379

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__, \
__LINE__, \
REASON, \
__VA_ARGS__); \
} \
} while(false)
#define CURRENT_FUNCTION_NAME
Definition: invariant.h:379

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